Ehrenfeucht–Fraïssé: n-equivalence and first-order inexpressibility

[UPSTREAM] candidate. M ≡ₙ N (NEquiv n M N) holds when M and N agree on every sentence of quantifier rank ≤ n — the finite-rank refinement of mathlib's ElementarilyEquivalent (= ∀ n, NEquiv n). On it rests the Ehrenfeucht–Fraïssé inexpressibility corollary: a property of structures that can be ≡ₙ-fooled for every n is not first-order definable. This is the abstract engine behind most ∉ FO (Studies.BarwiseCooper1981), parity, connectivity, etc.

mathlib has the ∞-rank apparatus (ElementarilyEquivalent, the unbounded back-and-forth IsExtensionPair) but not this finite-rank layer; quantifier rank itself is BoundedFormula.qr (this directory).

Main definitions / results

• FirstOrder.Language.NEquiv — n-equivalence of structures.
• FirstOrder.Language.FODefinable — a structure property captured by a sentence.
• FirstOrder.Language.not_foDefinable_of_nEquiv — the EF inexpressibility corollary.

def FirstOrder.Language.NEquiv {L : Language} (n : ℕ) (M N : CategoryTheory.Bundled L.Structure) : Prop

n-equivalence: M and N satisfy the same sentences of quantifier rank ≤ n. The finite-rank refinement of ElementarilyEquivalent (≅[L]), which is the n = ∞ case (elementarilyEquivalent_iff_forall_nEquiv).

Equations

• FirstOrder.Language.NEquiv n M N = ∀ (φ : L.Sentence), FirstOrder.Language.BoundedFormula.qr φ ≤ n → (↑M ⊨ φ ↔ ↑N ⊨ φ)

theorem FirstOrder.Language.NEquiv.refl {L : Language} (n : ℕ) (M : CategoryTheory.Bundled L.Structure) : NEquiv n M M

theorem FirstOrder.Language.NEquiv.symm {L : Language} {n : ℕ} {M N : CategoryTheory.Bundled L.Structure} (h : NEquiv n M N) : NEquiv n N M

theorem FirstOrder.Language.NEquiv.trans {L : Language} {n : ℕ} {M N P : CategoryTheory.Bundled L.Structure} (h₁ : NEquiv n M N) (h₂ : NEquiv n N P) : NEquiv n M P

theorem FirstOrder.Language.NEquiv.mono {L : Language} {n m : ℕ} {M N : CategoryTheory.Bundled L.Structure} (hnm : n ≤ m) (h : NEquiv m M N) : NEquiv n M N

n-equivalence is antitone in the rank: agreeing up to rank m implies agreeing up to any smaller rank n.

theorem FirstOrder.Language.elementarilyEquivalent_iff_forall_nEquiv {L : Language} (M N : CategoryTheory.Bundled L.Structure) : L.ElementarilyEquivalent ↑M ↑N ↔ ∀ (n : ℕ), NEquiv n M N

ElementarilyEquivalent is exactly n-equivalence at every rank.

def FirstOrder.Language.FODefinable {L : Language} (P : CategoryTheory.Bundled L.Structure → Prop) : Prop

A property of structures is first-order definable when some sentence captures exactly the structures with the property.

Equations

• FirstOrder.Language.FODefinable P = ∃ (φ : L.Sentence), ∀ (M : CategoryTheory.Bundled L.Structure), ↑M ⊨ φ ↔ P M

theorem FirstOrder.Language.not_foDefinable_of_nEquiv {L : Language} {P : CategoryTheory.Bundled L.Structure → Prop} (h : ∀ (n : ℕ), ∃ (M : CategoryTheory.Bundled L.Structure) (N : CategoryTheory.Bundled L.Structure), NEquiv n M N ∧ ¬(P M ↔ P N)) : ¬FODefinable P

Ehrenfeucht–Fraïssé inexpressibility. If for every rank n there are structures that are n-equivalent yet separated by P (one has it, the other does not), then P is not first-order definable. The standard route to FO-inexpressibility: the sentence's own quantifier rank is the n at which the witnesses fool it.