The game on bare sets

The duplicator's strategy on structures over the empty vocabulary – bare finite sets, the simplest structures there are. A position is legal there as soon as the two tuples have the same equality pattern (DescriptiveComplexity.partialIso_bare: there is no relation to check), and the strategy is the obvious one: answer a repetition by the matching repetition, a fresh element by a fresh element. Fresh elements last as long as the sets do, so DescriptiveComplexity.efEquiv_bare – two bare sets with at least n elements each are n-round equivalent, whatever their sizes.

By the methodology lemma (DescriptiveComplexity.realize_sentence_of_efEquiv) first-order logic therefore cannot compare the sizes of two bare sets beyond its quantifier rank: it counts up to a constant and no further. That is the whole content of the inexpressibility of DescriptiveComplexity.EVEN (DescriptiveComplexity.Problems.Even), and the reason the same problem must be attacked with a much finer game once a linear order is available.

Fresh elements

theorem DescriptiveComplexity.exists_notMem_range {N : Type} [Finite N] {j : ℕ} (b : Fin j → N) (h : j < Nat.card N) : ∃ (d : N), ∀ (i : Fin j), b i ≠ d

A tuple shorter than the finite set it lives in misses an element.

Extending a position

theorem DescriptiveComplexity.snoc_pattern {M N : Type} {j : ℕ} {a : Fin j → M} {b : Fin j → N} {c : M} {d : N} (hpat : ∀ (i i' : Fin j), a i = a i' ↔ b i = b i') (hc : ∀ (i : Fin j), a i = c ↔ b i = d) (i i' : Fin (j + 1)) : Fin.snoc a c i = Fin.snoc a c i' ↔ Fin.snoc b d i = Fin.snoc b d i'

Extending two tuples with the same equality pattern by a matching pair of elements – matching in the sense that each coordinate hits the new element on the left exactly when it does on the right – preserves the pattern.

The strategy

theorem DescriptiveComplexity.partialIso_bare {M N : Type} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] {j : ℕ} {a : Fin j → M} {b : Fin j → N} (hpat : ∀ (i i' : Fin j), a i = a i' ↔ b i = b i') : PartialIso FirstOrder.Language.empty a b

Over the empty vocabulary a position is legal as soon as the two tuples have the same equality pattern: there is no relation to check.

theorem DescriptiveComplexity.efStage_bare {M N : Type} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] [Finite M] [Finite N] (n : ℕ) {j : ℕ} (a : Fin j → M) (b : Fin j → N) : (∀ (i i' : Fin j), a i = a i' ↔ b i = b i') → n + j ≤ Nat.card M → n + j ≤ Nat.card N → efStage FirstOrder.Language.empty n a b

The duplicator's strategy on bare sets: from a position whose tuples have the same equality pattern, the duplicator survives as many rounds as either set has elements to spare. A repetition is answered by the matching repetition, a fresh element by a fresh element (DescriptiveComplexity.exists_notMem_range), which is where the budget is spent.

theorem DescriptiveComplexity.efEquiv_bare {M N : Type} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] [Finite M] [Finite N] (n : ℕ) (hM : n ≤ Nat.card M) (hN : n ≤ Nat.card N) : EFEquiv FirstOrder.Language.empty M N n

Two bare sets with at least n elements each are n-round equivalent – however different their sizes.

What first-order logic can say about a bare set

theorem DescriptiveComplexity.exists_card_bound_of_foDefinableFree {P : DecisionProblem FirstOrder.Language.empty} (h : FODefinableFree P) : ∃ (N : ℕ), ∀ (A B : Type) [inst : FirstOrder.Language.empty.Structure A] [inst_1 : FirstOrder.Language.empty.Structure B] [Finite A] [Finite B] [Nonempty A] [Nonempty B], N ≤ Nat.card A → N ≤ Nat.card B → (P.Holds A ↔ P.Holds B)

First-order logic counts up to a constant: an order-free first-order definable property of bare sets has a threshold beyond which it no longer depends on the size of the set. The threshold is the quantifier rank of a defining sentence – one round of the game per quantifier (DescriptiveComplexity.efEquiv_bare, DescriptiveComplexity.realize_sentence_of_efEquiv).

Every inexpressibility result over the empty vocabulary is an instance: exhibit two large sets of different sizes the problem separates.