Model classes of infinitary sentences

For a relational language L, a carrier V and an infinitary sentence φ, the model class TauCeti.RelationalConfiguration.modelsOf φ is the set of configurations on V whose decoded structures satisfy φ. Model classes are the basic objects of the descriptive set theory of countable models: counting the countable models of φ is counting the isomorphism classes met by its model classes on ℕ and on each Fin n.

On a countable carrier, every infinitary formula with countable branching defines a Borel set of configurations at each valuation of its variables. In a relational language every term is a variable, so atomic formulas are cylinders or constant conditions; implication, countable conjunction and disjunction, and quantification over the countable carrier preserve Borelness. In particular model classes of L_{ω₁ω} sentences are Borel, hence standard Borel subspaces when the language has countably many relation symbols. Model classes are closed under isomorphism of the decoded structures, across carriers, and by Equiv.realize_encodeVia a structure transported to any bijective carrier lies in the model class of each sentence it satisfies.

This is the easy direction of the López–Escobar theorem, which conversely presents every isomorphism-invariant Borel set of configurations on ℕ as a model class; see Gao, Invariant Descriptive Set Theory, and Kechris, Classical Descriptive Set Theory.

Main definitions

• TauCeti.RelationalConfiguration.modelsOf: the configurations on V decoding to models of a sentence.

Main results

• TauCeti.RelationalConfiguration.modelsOf_inf, modelsOf_sup, modelsOf_iInf, modelsOf_iSup, modelsOf_not, modelsOf_imp, modelsOf_top and modelsOf_bot: model classes turn the connectives into the Boolean set operations.
• TauCeti.RelationalConfiguration.measurableSet_setOf_realize: on a countable carrier, the configurations realizing an infinitary formula with countable branching at a fixed valuation form a measurable set.
• TauCeti.RelationalConfiguration.measurableSet_modelsOf: model classes of such sentences are measurable, and TauCeti.RelationalConfiguration.standardBorelSpace_modelsOf makes them standard Borel.
• FirstOrder.Language.Equiv.mem_modelsOf_iff: model classes are invariant under isomorphism of the decoded structures.

def TauCeti.RelationalConfiguration.modelsOf {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} (φ : L.SentenceInf ι) : Set (RelationalConfiguration L V)

The model class of an infinitary sentence: the configurations on V whose decoded structures satisfy it.

@[simp]

theorem TauCeti.RelationalConfiguration.mem_modelsOf {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} {φ : L.SentenceInf ι} {c : RelationalConfiguration L V} : c ∈ modelsOf φ ↔ φ.Realize V

A configuration lies in the model class of φ exactly when its decoded structure satisfies φ.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_bot {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} : modelsOf ⊥ = ∅

The false sentence has no models.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_top {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} : modelsOf ⊤ = Set.univ

The true sentence holds in every structure.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_infiniteSentence_of_infinite {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [Infinite V] : modelsOf L.infiniteSentence = Set.univ

On an infinite carrier every configuration satisfies the infinitude sentence.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_infiniteSentence_of_finite {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [Finite V] : modelsOf L.infiniteSentence = ∅

On a finite carrier no configuration satisfies the infinitude sentence, including on the empty carrier.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_imp {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} (φ ψ : L.SentenceInf ι) : modelsOf (FirstOrder.Language.BoundedFormulaInf.imp φ ψ) = (modelsOf φ)ᶜ ∪ modelsOf ψ

The model class of an implication is the complement of the model class of its hypothesis, joined with the model class of its conclusion.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_not {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} (φ : L.SentenceInf ι) : modelsOf (FirstOrder.Language.BoundedFormulaInf.not φ) = (modelsOf φ)ᶜ

The model class of a negation is the complement of the model class.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_inf {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} (φ ψ : L.SentenceInf ι) : modelsOf (φ ⊓ ψ) = modelsOf φ ∩ modelsOf ψ

The model class of a conjunction is the intersection of the model classes.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_sup {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} (φ ψ : L.SentenceInf ι) : modelsOf (φ ⊔ ψ) = modelsOf φ ∪ modelsOf ψ

The model class of a disjunction is the union of the model classes.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_iInf {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} (φs : ι → L.SentenceInf ι) : modelsOf (FirstOrder.Language.BoundedFormulaInf.iInf φs) = ⋂ (i : ι), modelsOf (φs i)

The model class of an infinitary conjunction is the intersection of the model classes.

@[simp]

theorem TauCeti.RelationalConfiguration.modelsOf_iSup {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} (φs : ι → L.SentenceInf ι) : modelsOf (FirstOrder.Language.BoundedFormulaInf.iSup φs) = ⋃ (i : ι), modelsOf (φs i)

The model class of an infinitary disjunction is the union of the model classes.

theorem TauCeti.RelationalConfiguration.measurableSet_setOf_realize {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} [Countable ι] [Countable V] {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (v : α → V) (xs : Fin n → V) : MeasurableSet {c : RelationalConfiguration L V | φ.Realize v xs}

On a countable carrier, the configurations realizing an infinitary formula with countable branching, at fixed valuations of its free and bound variables, form a measurable set. Neither the language nor its relation symbols need be countable.

theorem TauCeti.RelationalConfiguration.measurableSet_modelsOf {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} [Countable ι] [Countable V] (φ : L.SentenceInf ι) : MeasurableSet (modelsOf φ)

On a countable carrier, the model class of an infinitary sentence with countable branching, in particular of every L_{ω₁ω} sentence, is measurable.

instance TauCeti.RelationalConfiguration.standardBorelSpace_modelsOf {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {ι : Type uι} [∀ (n : ℕ), Countable (L.Relations n)] [Countable ι] [Countable V] (φ : L.SentenceInf ι) : StandardBorelSpace ↑(modelsOf φ)

In a language with countably many relation symbols of each arity, a model class on a countable carrier is a standard Borel space.

theorem FirstOrder.Language.Equiv.mem_modelsOf_iff {L : Language} [L.IsRelational] {V : Type w} {W : Type w'} {ι : Type uι} {c : TauCeti.RelationalConfiguration L V} {d : TauCeti.RelationalConfiguration L W} (e : L.Equiv V W) (φ : L.SentenceInf ι) : c ∈ TauCeti.RelationalConfiguration.modelsOf φ ↔ d ∈ TauCeti.RelationalConfiguration.modelsOf φ

Model classes are invariant under isomorphism: configurations on possibly different carriers with isomorphic decoded structures lie in the same model classes.