Documentation

TauCeti.ModelTheory.ModelExistence.CountableModel

Countable models of countable L_{ω₁ω} theories #

A nonempty model of a countable L_{ω₁ω} theory T, of any cardinality and in any universe, gives a countable nonempty model of T in every universe. The language may have any number of symbols. The proof passes to the sublanguage of the function symbols occurring in T, of which there are countably many, takes a countable substructure containing a chosen element that is elementary for the fragment generated by T, moves it into the target universe, and expands it back to L on its nonempty carrier. The chosen element matters: without it the substructure can be empty, for instance for T = {⊤} over a language without constants.

Consequently satisfiability and entailment of countable theories can be tested on countable models in any one universe. The universe max u v fixed in Theoryω.IsSatisfiable and Theoryω.Entails is a normalization, not a restriction: a sentence entailed by a countable theory holds in every nonempty model of the theory, whatever its cardinality and universe. This is what lets entailment move between languages in different universes. A language map preserves entailment by countable theories, and an injective one also reflects it.

Main results #

References #

source
theorem FirstOrder.Language.Theoryω.Model.exists_countable_model {L : Language} {T : L.Theoryω} (hT : Set.Countable T) {M : Type w} [L.Structure M] [Nonempty M] (h : T.Model M) :
∃ (N : Type w') (x : L.Structure N), Countable N ∧ Nonempty N ∧ T.Model N

Downward Löwenheim–Skolem for countable theories. A nonempty model of a countable theory, of any cardinality and in any universe, gives a countable nonempty model of the theory in every universe w'. The language may have any number of symbols.

source
theorem FirstOrder.Language.Theoryω.exists_countable_model {L : Language} {T : L.Theoryω} (hT : Set.Countable T) (h : T.IsSatisfiable) :
∃ (M : Type w) (x : L.Structure M), Countable M ∧ Nonempty M ∧ T.Model M

Countable models of satisfiable countable theories. A satisfiable countable theory has a countable nonempty model in every universe w.

source
theorem FirstOrder.Language.Theoryω.Entails.realize {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} (hT : Set.Countable T) (h : T.Entails φ) (M : Type w) [L.Structure M] [Nonempty M] (hM : T.Model M) :
SentenceInf.Realize φ M

Universe invariance of entailment. A sentence entailed by a countable theory holds in every nonempty model of the theory, of any cardinality and in any universe.

source
theorem FirstOrder.Language.Theoryω.entails_iff_countable {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} (hT : Set.Countable T) :
T.Entails φ ↔ ∀ (M : Type w) [inst : L.Structure M] [Countable M] [Nonempty M], T.Model M → SentenceInf.Realize φ M

Entailment is tested on countable models. A countable theory entails a sentence exactly when every countable nonempty model of the theory in the universe w satisfies it.

source
theorem FirstOrder.Language.Theoryω.Entails.onTheoryω {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} {L' : Language} (hT : Set.Countable T) (h : T.Entails φ) (g : L →ᴸ L') :
(g.onTheoryω T).Entails (g.onBoundedFormulaInf φ)

Language maps preserve entailment. If a countable theory T entails φ, the image of T under any language map g entails the image of φ. The two languages may live in different universes.

source
theorem FirstOrder.Language.Theoryω.entails_onTheoryω_iff {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} {L' : Language} {g : L →ᴸ L'} (hg : g.Injective) (hT : Set.Countable T) :
(g.onTheoryω T).Entails (g.onBoundedFormulaInf φ) ↔ T.Entails φ

Injective language maps reflect entailment. For an injective language map g, the image of a countable theory T entails the image of φ exactly when T entails φ. This is the entailment form of Mathlib's Theory.isSatisfiable_onTheory_iff.

source
theorem FirstOrder.Language.Sentenceω.Entails.realize {L : Language} {φ ψ : L.Sentenceω} (h : φ.Entails ψ) (M : Type w) [L.Structure M] [Nonempty M] (hφ : SentenceInf.Realize φ M) :
SentenceInf.Realize ψ M

Universe invariance of entailment between sentences. If φ entails ψ, then ψ holds in every nonempty model of φ, of any cardinality and in any universe.

source
theorem FirstOrder.Language.Sentenceω.entails_iff_countable {L : Language} {φ ψ : L.Sentenceω} :
φ.Entails ψ ↔ ∀ (M : Type w) [inst : L.Structure M] [Countable M] [Nonempty M], SentenceInf.Realize φ M → SentenceInf.Realize ψ M

Entailment between sentences is tested on countable models. A sentence φ entails ψ exactly when ψ holds in every countable nonempty model of φ in the universe w.

source
theorem FirstOrder.Language.Sentenceω.Entails.onBoundedFormulaInf {L : Language} {φ ψ : L.Sentenceω} {L' : Language} (h : φ.Entails ψ) (g : L →ᴸ L') :
Entails (g.onBoundedFormulaInf φ) (g.onBoundedFormulaInf ψ)

Language maps preserve entailment between sentences. If φ entails ψ, the image of φ under any language map g entails the image of ψ.

source
theorem FirstOrder.Language.Sentenceω.entails_onBoundedFormulaInf_iff {L : Language} {φ ψ : L.Sentenceω} {L' : Language} {g : L →ᴸ L'} (hg : g.Injective) :
Entails (g.onBoundedFormulaInf φ) (g.onBoundedFormulaInf ψ) ↔ φ.Entails ψ

Injective language maps reflect entailment between sentences. For an injective language map g, the image of φ entails the image of ψ exactly when φ entails ψ.