Back-and-Forth Equivalence

This file defines the back-and-forth equivalence relation between tuples in structures, indexed by ordinals. This is the semantic predicate that corresponds to Scott formulas.

Main Definitions

• BFEquiv: The α-back-and-forth equivalence between tuples, indexed by ordinal α.

Main Results

• BFEquiv.zero_iff_sameAtomicType: At level 0, BF-equivalence is atomic type equivalence.
• BFEquiv.monotone: BF-equivalence at higher ordinals implies equivalence at lower ordinals.
• BFEquiv.forth/BFEquiv.back: Extension properties at successor ordinals.
• BFEquiv.symm: BF-equivalence is symmetric.

Implementation Notes

We use Ordinal.limitRecOn for the definition, which requires handling three cases:

• Zero: same atomic type
• Successor Order.succ α: equivalence at α plus forth and back conditions
• Limit (with Order.IsSuccLimit): equivalence at all smaller ordinals

Known Limitation: ω-Level Coherence and Quantifier Swap

A natural approach to proving BFEquiv_omega_implies_equiv (BF-equivalence at ω implies isomorphism) is to define a "strategy" type that carries explicit witnesses instead of just existence claims. The inductive definition:

inductive BFStrategy : (k : ℕ) → ... → Type
  | zero : SameAtomicType a b → BFStrategy 0 n a b
  | succ : BFStrategy k n a b →
           (forth : (m : M) → Σ n', BFStrategy k (n+1) ...) → ...

fails Lean's nested-inductive check. However, we CAN define BFStrategy by recursion on k (this compiles and avoids the kernel restriction). See BFStrategy below.

We then define BFStrategyOmega n a b := ∀ k, BFStrategy k n a b, a coherent family of strategies at all finite levels. This is the "winning strategy in the ω-round EF game."

The real mathematical issue: Even with these definitions, we have:

• BFStrategyOmega → isomorphism is provable (the strategy gives coherent witnesses)
• BFEquiv ω → BFStrategyOmega is the open problem (possibly false without extra assumptions)

This is the standard model-theory distinction: "BFEquiv holds at all finite levels" (∀ k, Duplicator wins the k-round game) does NOT imply "Duplicator has a winning strategy in the ω-round game," even for countable structures.

The obstruction is the quantifier swap:

From BFEquiv ω: ∀ k, ∃ n'_k, BFEquiv k (snoc a m) (snoc b n'_k)
Need:          ∃ n', ∀ k, BFEquiv k (snoc a m) (snoc b n')

Concrete counterexample to such swaps: Let S_k = {n ∈ ℕ | n ≥ k}. Each S_k is non-empty, and S_0 ⊇ S_1 ⊇ S_2 ⊇ ..., but ⋂_k S_k = ∅. The witnesses keep shifting as k grows.

In our setting, S_k = {n' ∈ N | BFEquiv k (snoc a m) (snoc b n')}. By monotonicity of BFEquiv, these sets are decreasing. But without a stabilization property, their intersection may be empty.

Note on alternative approaches:

• Dependent choice does NOT help: even with full AC, ∀ k, ∃ n'_k doesn't yield ∃ n', ∀ k when the sets strictly decrease to empty intersection.
• König's lemma would require finite branching or compactness; not available here since the "tree" of valid witnesses lacks the necessary finiteness properties.
• A game-theoretic formulation (strategy as function on finite plays) might help but still requires proving a winning strategy exists from BFEquiv ω.

Resolution (in Sentence.lean): We use the stabilization approach:

1. StabilizesForTuples M α n: BFEquiv α ↔ BFEquiv (succ α) for n-tuples from M
2. StabilizesCompletely M α: All tuple sizes stabilize at α
3. exists_complete_stabilization: For countable M, such α < ω₁ exists
4. BFEquiv_stabilization_implies_equiv: At stabilization, BFEquiv → isomorphism

At a complete stabilization ordinal, forth/back witnesses stay at the same level, so the standard back-and-forth closes without quantifier swap issues.

Important: BFEquiv ω is equivalent to elementary equivalence (winning all finite EF games), which does NOT imply isomorphism. Potential counterexamples in relational languages include equivalence relations with matching finite-class structure but different arrangements of infinite classes.

noncomputable def FirstOrder.Language.BFEquiv {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (α : Ordinal.{u_1}) (n : ℕ) (a : Fin n → M) (b : Fin n → N) : Prop

Back-and-forth equivalence at ordinal α between tuples a in M and b in N.

At level 0: same atomic type. At successor α + 1: same atomic type, plus:

• (forth) for every m in M, there exists n in N with BFEquiv α (snoc a m) (snoc b n)
• (back) for every n in N, there exists m in M with BFEquiv α (snoc a m) (snoc b n) At limit λ: BFEquiv β for all β < λ.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.BFEquiv.zero {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) : BFEquiv 0 n a b ↔ SameAtomicType a b

theorem FirstOrder.Language.BFEquiv.zero_iff_sameAtomicType {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) : BFEquiv 0 n a b ↔ SameAtomicType a b

theorem FirstOrder.Language.BFEquiv.succ {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} (α : Ordinal.{u_1}) (a : Fin n → M) (b : Fin n → N) : BFEquiv (Order.succ α) n a b ↔ BFEquiv α n a b ∧ (∀ (m : M), ∃ (n' : N), BFEquiv α (n + 1) (Fin.snoc a m) (Fin.snoc b n')) ∧ ∀ (n' : N), ∃ (m : M), BFEquiv α (n + 1) (Fin.snoc a m) (Fin.snoc b n')

theorem FirstOrder.Language.BFEquiv.limit {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} (α : Ordinal.{u_1}) (hα : Order.IsSuccLimit α) (a : Fin n → M) (b : Fin n → N) : BFEquiv α n a b ↔ ∀ β < α, BFEquiv β n a b

theorem FirstOrder.Language.BFEquiv.of_succ {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {α : Ordinal.{u_1}} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv (Order.succ α) n a b) : BFEquiv α n a b

BF-equivalence at level α + 1 implies BF-equivalence at level α.

theorem FirstOrder.Language.BFEquiv.monotone {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {α β : Ordinal.{u_1}} (hαβ : α ≤ β) {a : Fin n → M} {b : Fin n → N} (h : BFEquiv β n a b) : BFEquiv α n a b

BF-equivalence is monotone: higher ordinals imply lower ordinals.

theorem FirstOrder.Language.BFEquiv.forth {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {α : Ordinal.{u_1}} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv (Order.succ α) n a b) (m : M) : ∃ (n' : N), BFEquiv α (n + 1) (Fin.snoc a m) (Fin.snoc b n')

The "forth" property at a successor level.

theorem FirstOrder.Language.BFEquiv.back {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {α : Ordinal.{u_1}} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv (Order.succ α) n a b) (n' : N) : ∃ (m : M), BFEquiv α (n + 1) (Fin.snoc a m) (Fin.snoc b n')

The "back" property at a successor level.

theorem FirstOrder.Language.BFEquiv.refl_zero {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : BFEquiv 0 n a a

BF-equivalence at level 0 is reflexive.

theorem FirstOrder.Language.BFEquiv.refl {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (α : Ordinal.{u_1}) (a : Fin n → M) : BFEquiv α n a a

BF-equivalence is reflexive at all levels.

theorem FirstOrder.Language.BFEquiv.symm {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {α : Ordinal.{u_1}} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv α n a b) : BFEquiv α n b a

BF-equivalence is symmetric at all levels.

theorem FirstOrder.Language.BFEquiv.trans {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {P : Type u_1} [L.Structure P] {α : Ordinal.{u_2}} {a : Fin n → M} {b : Fin n → N} {c : Fin n → P} (hab : BFEquiv α n a b) (hbc : BFEquiv α n b c) : BFEquiv α n a c

BF-equivalence is transitive at all levels. If a and b are BF-equivalent, and b and c are BF-equivalent, then a and c are BF-equivalent. Note that a, b, c may be tuples in different structures.

BFStrategy: Explicit Witness Strategies

A back-and-forth strategy at level k provides explicit witnesses for extensions. Unlike BFEquiv which only asserts existence, a strategy carries the actual witnesses.

The key insight is that BFStrategy can be defined by recursion on k (not as an inductive type), avoiding Lean's nested-inductive check that blocks inductive definitions.

The open problem is BFEquiv ω → BFStrategyOmega: this is the quantifier swap obstruction. Having a strategy implies BFEquiv, but the converse requires choosing coherent witnesses.

Important: BFEquiv ω (winning all finite games) does NOT imply isomorphism in general. Winning all finite back-and-forth games does not give an ω-round strategy. The Type-valued BFStrategyT below is genuinely stronger than BFEquiv ω because it carries witnesses.

def FirstOrder.Language.BFStrategyT (L : Language) [L.IsRelational] (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : ℕ → (n : ℕ) → (Fin n → M) → (Fin n → N) → Type (max w w')

Type-valued back-and-forth strategy at level k. Carries actual witnesses for extensions.

At level 0: a proof that tuples have the same atomic type (as a subtype of Unit). At level k+1: strategy at level k, plus witness FUNCTIONS (not just existence) for forth/back.

This is STRONGER than BFEquiv k because it provides computational witnesses, not just existence proofs. The converse BFEquiv k → BFStrategyT k requires Choice and loses coherence.

We use a recursive def (not inductive) to avoid Lean's nested-inductive restrictions. The base case uses { _ : Unit // SameAtomicType a b } to lift Prop to Type in a universe- polymorphic way (Subtype lives in the same universe as the carrier type).

Equations

• One or more equations did not get rendered due to their size.
• L.BFStrategyT M N 0 = fun (_n : ℕ) (a : Fin _n → M) (b : Fin _n → N) => { x : PUnit.{(max ?u.187 ?u.186) + 1} // FirstOrder.Language.SameAtomicType a b }

def FirstOrder.Language.BFStrategyOmegaT {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (n : ℕ) (a : Fin n → M) (b : Fin n → N) : Type (max w w')

A coherent family of Type-valued strategies at all finite levels. This is the "winning strategy in the ω-round EF game" with actual witnesses.

This is STRONGER than BFEquiv ω. The existence of BFStrategyOmegaT implies isomorphism (provable by standard back-and-forth), but BFEquiv ω alone does not.

Equations

• FirstOrder.Language.BFStrategyOmegaT n a b = ((k : ℕ) → L.BFStrategyT M N k n a b)

theorem FirstOrder.Language.BFStrategyT_implies_BFEquiv {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} (k : ℕ) (strat : L.BFStrategyT M N k n a b) : BFEquiv (↑k) n a b

A Type-valued strategy at level k implies BF-equivalence at level k. This direction is straightforward: just forget the witnesses.

theorem FirstOrder.Language.BFStrategyOmegaT_implies_BFEquiv_omega {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hstrat : BFStrategyOmegaT n a b) : BFEquiv Ordinal.omega0 n a b

A coherent ω-strategy implies BF-equivalence at level ω.

Universe Lifting for BFEquiv

BFEquiv is defined by Ordinal.limitRecOn, which is universe-specific. These lemmas transport BFEquiv between ordinal universes via Ordinal.lift.

theorem FirstOrder.Language.BFEquiv.ofOrdinalLift {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {β : Ordinal.{0}} {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv β n a b) : BFEquiv (Ordinal.lift.{w, 0} β) n a b

Lift BFEquiv from Ordinal.{0} to Ordinal.{w} at a specific ordinal. If BFEquiv β n a b holds at β : Ordinal.{0}, then it holds at Ordinal.lift β : Ordinal.{w}.

theorem FirstOrder.Language.BFEquiv.toOrdinalLift {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {β : Ordinal.{0}} {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv (Ordinal.lift.{w, 0} β) n a b) : BFEquiv β n a b

Lower BFEquiv from Ordinal.{w} back to Ordinal.{0} at a specific ordinal. If BFEquiv (Ordinal.lift β) n a b holds at the lifted ordinal, then BFEquiv β n a b holds at the original.