Ordinal back-and-forth equivalence

BFEquiv α n a b compares finite tuples at ordinal depth α. At zero it is atomic-type agreement; a successor retains the previous level and requires matching one-element extensions in both directions; a limit requires every earlier level. Keeping the previous level prevents empty structures with different nullary relations from becoming equivalent at a successor.

The equivalence laws and lowering of the ordinal are the basic tools for internal stabilization and for the characteristic formulas of tuples. No countability or nonemptiness is assumed. As with SameAtomicType, the language is required to be relational, so the initial level compares all atomic formulas.

The recursion follows Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Scott/BackAndForth.lean. Here the ordinal universe is independent of the universes of the structures.

For a family of structures M i, i : ι, bfTupleSetoid L M α n packages equivalence at depth α as an equivalence relation on the pointed tuples ⟨i, a⟩ with a : Fin n → M i, comparing tuples across all members of the family.

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

Ordinal back-and-forth equivalence of tuples. At successors the previous level is retained, in addition to the forth and back requirements. The language is relational.

@[simp]

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

Level zero is precisely atomic-type agreement.

@[simp]

theorem TauCeti.BFEquiv.add_one {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} (α : Ordinal.{o}) (a : Fin n → M) (b : Fin n → N) : BFEquiv (α + 1) n a b ↔ BFEquiv α n a b ∧ (∀ (x : M), ∃ (y : N), BFEquiv α (n + 1) (Fin.snoc a x) (Fin.snoc b y)) ∧ ∀ (y : N), ∃ (x : M), BFEquiv α (n + 1) (Fin.snoc a x) (Fin.snoc b y)

The successor step consists of the previous level and the two extension requirements.

@[simp]

theorem TauCeti.BFEquiv.one {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) : BFEquiv 1 n a b ↔ SameAtomicType a b ∧ (∀ (x : M), ∃ (y : N), SameAtomicType (Fin.snoc a x) (Fin.snoc b y)) ∧ ∀ (y : N), ∃ (x : M), SameAtomicType (Fin.snoc a x) (Fin.snoc b y)

Level one consists of atomic-type agreement and atomic-type matching of one-element extensions in both directions.

@[simp]

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

At a limit ordinal, equivalence means equivalence at every smaller ordinal.

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

Equivalence at a level implies equivalence at every lower level.

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

Atomic type is preserved at every back-and-forth level.

@[simp]

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

Every tuple is back-and-forth equivalent to itself.

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

Back-and-forth equivalence is symmetric, including between different structure universes.

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

Back-and-forth equivalence is transitive across three structures.

theorem TauCeti.BFEquiv.comp {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} {α : Ordinal.{o}} (h : BFEquiv α n a b) {m : ℕ} (g : Fin m → Fin n) : BFEquiv α m (a ∘ g) (b ∘ g)

Back-and-forth equivalence is preserved when the two tuples are reindexed in the same way.

theorem TauCeti.BFEquiv.symm_iff {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} (α : Ordinal.{o}) (a : Fin n → M) (b : Fin n → N) : BFEquiv α n a b ↔ BFEquiv α n b a

Swapping the two tuples does not change back-and-forth equivalence.

theorem TauCeti.BFEquiv.exists_bfEquiv_append {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {β : Ordinal.{o}} {m : ℕ} {a : Fin m → M} {b : Fin m → N} (k : ℕ) (h : BFEquiv (β + ↑k) m a b) (x : Fin k → M) : ∃ (y : Fin k → N), BFEquiv β (m + k) (Fin.append a x) (Fin.append b y)

Equivalence at depth β + k extends along any k further elements of the first structure to equivalence at depth β: k forth steps match them with elements of the second structure.

@[simp]

theorem TauCeti.BFEquiv.lift {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} (α : Ordinal.{o}) (a : Fin n → M) (b : Fin n → N) : BFEquiv (Ordinal.lift.{o', o} α) n a b ↔ BFEquiv α n a b

Back-and-forth equivalence is invariant under lifting the ordinal depth across universes.

theorem FirstOrder.Language.Equiv.bfEquiv {L : Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (α : Ordinal.{o}) {n : ℕ} (a : Fin n → M) : TauCeti.BFEquiv α n a (⇑e ∘ a)

An isomorphism carries every tuple to a tuple back-and-forth equivalent to it at every level. In particular, tuples in one automorphism orbit are equivalent at every level.

Equivalence of pointed tuples of a family

def TauCeti.bfTupleSetoid (L : FirstOrder.Language) [L.IsRelational] {ι : Type x} (M : ι → Type w) [(i : ι) → L.Structure (M i)] (α : Ordinal.{o}) (n : ℕ) : Setoid ((i : ι) × (Fin n → M i))

Back-and-forth equivalence at depth α of pointed n-tuples of the family M: the pointed tuples ⟨i, a⟩ and ⟨j, b⟩ are related when a in M i and b in M j are back-and-forth equivalent at depth α.

@[simp]

theorem TauCeti.bfTupleSetoid_apply {L : FirstOrder.Language} [L.IsRelational] {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] {α : Ordinal.{o}} {n : ℕ} {x y : (i : ι) × (Fin n → M i)} : (bfTupleSetoid L M α n) x y ↔ BFEquiv α n x.snd y.snd

Two pointed tuples are related at depth α exactly when their tuples are back-and-forth equivalent at depth α.

theorem TauCeti.bfTupleSetoid_anti {L : FirstOrder.Language} [L.IsRelational] {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] (n : ℕ) : Antitone fun (x : Ordinal.{o}) => bfTupleSetoid L M x n

The levels decrease as the depth grows.

@[simp]

theorem TauCeti.bfTupleSetoid_lift {L : FirstOrder.Language} [L.IsRelational] {ι : Type x} {M : ι → Type w} [(i : ι) → L.Structure (M i)] (α : Ordinal.{o}) (n : ℕ) : bfTupleSetoid L M (Ordinal.lift.{o', o} α) n = bfTupleSetoid L M α n

Lifting the ordinal depth across universes does not change bfTupleSetoid.

Empty-structure regression examples