The finite-rank Ehrenfeucht–Fraïssé back-and-forth relation

[UPSTREAM] candidate. The rank-k back-and-forth relation BackForth k v w on structures-with-tuples (M, v), (N, w) is the syntax-free combinatorial characterization of k-equivalence: BackForth 0 is agreement on quantifier-free formulas, and BackForth (k+1) is the forth (every a : M is matched by some b : N) and back (dually) conditions, recursing at rank k. This is the rank-bounded refinement of mathlib's unbounded IsExtensionPair / FGEquiv-based back-and-forth.

The soundness direction — BackForth k v w implies the two tuples satisfy the same formulas of quantifier rank ≤ k (BackForth.agree), hence the structures are ≡ₖ (nEquiv_of_backForth, feeding not_foDefinable_of_nEquiv) — is the tractable half and is proved here in full (under the finite-model-theory convention that the domains are [Nonempty], used to extract quantifier-free agreement of a tuple from the higher-rank forth/back data). The converse (Libkin "1 ⟹ 3", via rank-k Hintikka formulas / k-types) is left as future work.

Construction: Libkin, Elements of Finite Model Theory, Thm 3.18; Hodges, Model Theory, §3.2 (general back-and-forth systems).

Main definitions / results

• FirstOrder.Language.BackForth — the rank-k back-and-forth relation.
• FirstOrder.Language.BackForth.agree — soundness: back-and-forth ⟹ agreement on rank-≤ k formulas.
• FirstOrder.Language.nEquiv_of_backForth — back-and-forth on the empty tuples ⟹ ≡ₖ.

def FirstOrder.Language.BackForth {L : Language} (M N : Type w) [L.Structure M] [L.Structure N] (k : ℕ) {m : ℕ} : (Fin m → M) → (Fin m → N) → Prop

The rank-k Ehrenfeucht–Fraïssé back-and-forth relation between a structure M with an m-tuple v and a structure N with an m-tuple w.

• At rank 0: v and w satisfy the same quantifier-free formulas (here phrased as all formulas of quantifier rank 0).
• At rank k + 1: the forth condition (every a : M extends v to a pair still related at rank k by some b : N) and the dual back condition.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BackForth M N 0 x✝¹ x✝ = ∀ (φ : L.BoundedFormula (Fin x✝²) 0), φ.qr = 0 → (φ.Realize x✝¹ default ↔ φ.Realize x✝ default)

theorem FirstOrder.Language.BackForth.mono {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] [Nonempty M] {k m : ℕ} {v : Fin m → M} {w : Fin m → N} : BackForth M N (k + 1) v w → BackForth M N k v w

Monotonicity: a rank-k+1 back-and-forth pair is also a rank-k one. The base step (rank 1 → 0) recovers quantifier-free agreement of the tuple (v, w) itself by extending along the forth clause at an arbitrary element (whence [Nonempty M]) and discarding the new last variable via liftLast.

theorem FirstOrder.Language.BackForth.mono_zero {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] [Nonempty M] [Nonempty N] {k m : ℕ} {v : Fin m → M} {w : Fin m → N} : BackForth M N k v w → BackForth M N 0 v w

A rank-k back-and-forth pair is also a rank-0 one (quantifier-free agreement).

theorem FirstOrder.Language.BackForth.agree {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] {m : ℕ} [Nonempty M] [Nonempty N] {k : ℕ} {v : Fin m → M} {w : Fin m → N} (h : BackForth M N k v w) (φ : L.BoundedFormula (Fin m) 0) : φ.qr ≤ k → (φ.Realize v default ↔ φ.Realize w default)

Soundness of back-and-forth (Libkin Thm 3.18, "3 ⟹ 1"). If (M, v) and (N, w) are related by the rank-k back-and-forth relation, then they satisfy the same formulas of quantifier rank ≤ k. Proof: the all case uses the forth clause and the rank-k recursion, the dual ex case the back clause; atomic agreement descends to the quantifier-free base case via mono_zero.

theorem FirstOrder.Language.nEquiv_of_backForth {L : Language} {k : ℕ} (M N : CategoryTheory.Bundled L.Structure) [Nonempty ↑M] [Nonempty ↑N] (h : BackForth (↑M) (↑N) k default default) : NEquiv k M N

A rank-k back-and-forth relation between the structures themselves (on the empty tuples) witnesses k-equivalence — and so feeds not_foDefinable_of_nEquiv.