Back-and-forth successor levels via extension spectra

For a class C of coded models of a sentence φ and an ordinal α, the depth-α back-and-forth relation on n-tuples of C-models is an equivalence relation (bfTupleSetoid). By BFEquiv.succ, two tuples are (α+1)-equivalent iff they are α-equivalent and have the same set of depth-α classes of one-point extensions — their depth-α extension spectrum (bfExtensionSpectrum). So the (α+1)-classes over n-tuples are counted by the α-classes together with the realized extension spectra.

Main results

• bfTupleSetoid_succ_iff — (α+1)-equivalence is α-equivalence together with equality of extension spectra, for every arity and every class of models.
• bfExtensionSpectra — the realized extension spectra, the range of bfExtensionSpectrum.
• countable_bfTupleQuotient_succ — countably many α-classes over n-tuples and countably many realized extension spectra give countably many (α+1)-classes over n-tuples.
• mk_bfTupleQuotient_succ_le_aleph_one — the same transfer with ≤ ℵ₁ on both inputs.
• bfTupleSetoid_zero_eq_comap — at arity 0 the setoid is the pullback of bfEquivSetoid along the forgetful map to the underlying coded model (the tuple is trivial, and the class membership is forgotten); bfTupleSetoid_zero_iff is the pointwise form.

The hypothesis on the extension spectra is the whole content: a subset of a countable class space can a priori take continuum many values, so nothing here bounds the spectra themselves. Nothing is said about limit levels.

@[reducible, inline]

abbrev FirstOrder.Language.CodedModelTuple {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (n : ℕ) : Type v

Coded models of φ in a class C, each with an n-tuple.

Equations

• FirstOrder.Language.CodedModelTuple φ C n = (↑C × (Fin n → ℕ))

def FirstOrder.Language.bfTupleSetoid {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) : Setoid (CodedModelTuple φ C n)

The depth-α back-and-forth setoid on n-tuples of C-models.

Equations

• FirstOrder.Language.bfTupleSetoid φ C α n = { r := fun (x y : FirstOrder.Language.CodedModelTuple φ C n) => FirstOrder.Language.BFEquiv α n x.2 y.2, iseqv := ⋯ }

theorem FirstOrder.Language.bfTupleSetoid_zero_eq_comap {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) : bfTupleSetoid φ C α 0 = Setoid.comap (fun (x : CodedModelTuple φ C 0) => ↑x.1) (bfEquivSetoid φ α)

At arity 0 the tuple is trivial, and the setoid is the pullback of bfEquivSetoid along the map forgetting the class membership and the empty tuple.

theorem FirstOrder.Language.bfTupleSetoid_zero_iff {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (x y : CodedModelTuple φ C 0) : (bfTupleSetoid φ C α 0) x y ↔ (bfEquivSetoid φ α) ↑x.1 ↑y.1

The pointwise form of bfTupleSetoid_zero_eq_comap.

def FirstOrder.Language.bfExtensionSpectrum {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) (x : CodedModelTuple φ C n) : Set (Quotient (bfTupleSetoid φ C α (n + 1)))

The depth-α extension spectrum of a tuple: the depth-α classes of its one-point extensions.

Equations

• FirstOrder.Language.bfExtensionSpectrum φ C α n x = Set.range fun (m : ℕ) => ⟦(x.1, Fin.snoc x.2 m)⟧

def FirstOrder.Language.bfExtensionSpectra {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) : Set (Set (Quotient (bfTupleSetoid φ C α (n + 1))))

The realized extension spectra of n-tuples of C-models at depth α.

Equations

• FirstOrder.Language.bfExtensionSpectra φ C α n = Set.range (FirstOrder.Language.bfExtensionSpectrum φ C α n)

theorem FirstOrder.Language.bfTupleSetoid_succ_iff {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) (x y : CodedModelTuple φ C n) : (bfTupleSetoid φ C (Order.succ α) n) x y ↔ (bfTupleSetoid φ C α n) x y ∧ bfExtensionSpectrum φ C α n x = bfExtensionSpectrum φ C α n y

The successor characterization: (α+1)-equivalence is α-equivalence with equal depth-α extension spectra.

theorem FirstOrder.Language.exists_injective_bfTupleQuotient_succ {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) : ∃ (f : Quotient (bfTupleSetoid φ C (Order.succ α) n) → Quotient (bfTupleSetoid φ C α n) × ↑(bfExtensionSpectra φ C α n)), Function.Injective f

The (α+1)-classes over n-tuples inject into pairs (an α-class, a realized extension spectrum).

theorem FirstOrder.Language.countable_bfTupleQuotient_succ {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) (hα : Countable (Quotient (bfTupleSetoid φ C α n))) (hspec : Countable ↑(bfExtensionSpectra φ C α n)) : Countable (Quotient (bfTupleSetoid φ C (Order.succ α) n))

Countability transfer: countably many α-classes over n-tuples and countably many realized extension spectra give countably many (α+1)-classes over n-tuples.

theorem FirstOrder.Language.mk_bfTupleQuotient_succ_le_aleph_one {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) (hα : Cardinal.mk (Quotient (bfTupleSetoid φ C α n)) ≤ Cardinal.aleph 1) (hspec : Cardinal.mk ↑(bfExtensionSpectra φ C α n) ≤ Cardinal.aleph 1) : Cardinal.mk (Quotient (bfTupleSetoid φ C (Order.succ α) n)) ≤ Cardinal.aleph 1

Countability transfer at ≤ ℵ₁: if the α-classes over n-tuples and the realized extension spectra both number at most ℵ₁, so do the (α+1)-classes over n-tuples.