Satisfiability and entailment of L_{ω₁ω} theories

An L_{ω₁ω} theory is satisfiable when it has a nonempty model, and it entails a sentence when every nonempty model of the theory satisfies the sentence. As in Mathlib's first-order Theory.IsSatisfiable and Theory.ModelsBoundedFormula, both notions quantify over models in the fixed universe max u v of a language L : Language.{u, v}. Any nonempty model that is small in that universe, in particular any countable model, witnesses satisfiability and satisfies every entailed sentence.

Entailment is reflexive, monotone and transitive, admits cut, and is refutation of the negated conclusion. An entailed ¬ ∀ x, φ x yields the entailed ∃ x, ¬ φ x. A countable theory entails exactly what the conjunction of its sentences entails, so the entailments of a countable theory are entailments between two sentences. For first-order theories and sentences, embedded into L_{ω₁ω} by BoundedFormula.toOmega, satisfiability and entailment agree with Mathlib's first-order notions.

Main definitions

• FirstOrder.Language.Theoryω.IsSatisfiable: a theory has a nonempty model.
• FirstOrder.Language.Theoryω.Entails: every nonempty model of a theory satisfies a sentence.
• FirstOrder.Language.Sentenceω.Entails: entailment between two sentences.

Main results

• FirstOrder.Language.Theoryω.Model.isSatisfiable: a nonempty small model witnesses satisfiability.
• FirstOrder.Language.Theoryω.Entails.realize_of_small: an entailed sentence holds in every nonempty small model.
• FirstOrder.Language.Theoryω.entails_iff_not_isSatisfiable: a theory entails a sentence exactly when the theory together with the negation of the sentence is unsatisfiable.
• FirstOrder.Language.Theoryω.Entails.trans, FirstOrder.Language.Theoryω.Entails.cut: the transitivity and cut rules.
• FirstOrder.Language.Theoryω.entails_iff_conjunction_entails: a countable theory entails what its conjunction entails.
• FirstOrder.Language.Theoryω.isSatisfiable_image_toOmega_iff, FirstOrder.Language.Theoryω.entails_image_toOmega_iff and FirstOrder.Language.Sentenceω.entails_toOmega_iff: agreement with Mathlib's Theory.IsSatisfiable and Theory.ModelsBoundedFormula on first-order theories.

References

• The definitions and the refutation characterisation follow Mathlib's first-order Theory.IsSatisfiable, Theory.ModelsBoundedFormula and Theory.models_iff_not_satisfiable in Mathlib/ModelTheory/Satisfiability.lean (Aaron Anderson).
• Divergences from Mathlib: a model of an L_{ω₁ω} theory is an unbundled structure together with a proof of Theoryω.Model, so no bundled model type is introduced; a model in another universe is moved into the universe max u v through Small, whereas Mathlib's first-order Theory.Model.isSatisfiable uses downward Löwenheim–Skolem, which for L_{ω₁ω} holds only relative to countable fragments.

def FirstOrder.Language.Theoryω.IsSatisfiable {L : Language} (T : L.Theoryω) : Prop

A theory is satisfiable when it has a nonempty model in the universe max u v, the model universe of Mathlib's first-order Theory.IsSatisfiable.

def FirstOrder.Language.Theoryω.Entails {L : Language} (T : L.Theoryω) (φ : L.Sentenceω) : Prop

A theory entails a sentence when every nonempty model of the theory in the universe max u v satisfies the sentence, as in Mathlib's first-order Theory.ModelsBoundedFormula.

theorem FirstOrder.Language.Theoryω.isSatisfiable_iff {L : Language} {T : L.Theoryω} : T.IsSatisfiable ↔ ∃ (M : Type (max u v)) (x : L.Structure M), Nonempty M ∧ T.Model M

Unfolding lemma for Theoryω.IsSatisfiable.

theorem FirstOrder.Language.Theoryω.entails_iff {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} : T.Entails φ ↔ ∀ (M : Type (max u v)) [inst : L.Structure M] [Nonempty M], T.Model M → SentenceInf.Realize φ M

Unfolding lemma for Theoryω.Entails.

Satisfiability

theorem FirstOrder.Language.Theoryω.Model.isSatisfiable {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] [Nonempty M] [Small.{max u v, w} M] (h : T.Model M) : T.IsSatisfiable

A nonempty model of a theory that is small in the universe max u v, for instance a countable model in any universe, witnesses the satisfiability of the theory.

theorem FirstOrder.Language.Theoryω.IsSatisfiable.mono {L : Language} {T T' : L.Theoryω} (h : T'.IsSatisfiable) (hT : T ⊆ T') : T.IsSatisfiable

A subtheory of a satisfiable theory is satisfiable.

@[simp]

theorem FirstOrder.Language.Theoryω.isSatisfiable_empty {L : Language} : ∅.IsSatisfiable

The empty theory is satisfiable.

Entailment

theorem FirstOrder.Language.Theoryω.entails_of_mem {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} (h : φ ∈ T) : T.Entails φ

A theory entails each of its sentences.

theorem FirstOrder.Language.Theoryω.Entails.mono {L : Language} {T T' : L.Theoryω} {φ : L.Sentenceω} (h : T.Entails φ) (hT : T ⊆ T') : T'.Entails φ

Entailment is monotone in the theory.

theorem FirstOrder.Language.Theoryω.Model.of_entails {L : Language} {T T' : L.Theoryω} {M : Type (max u v)} [L.Structure M] [Nonempty M] (hM : T.Model M) (hT : ∀ ψ ∈ T', T.Entails ψ) : T'.Model M

A nonempty model of T in the universe max u v is a model of every theory whose sentences T entails.

theorem FirstOrder.Language.Theoryω.Entails.trans {L : Language} {T T' : L.Theoryω} {φ : L.Sentenceω} (h : T'.Entails φ) (hT : ∀ ψ ∈ T', T.Entails ψ) : T.Entails φ

Transitivity of entailment. If T entails every sentence of T', then T entails every sentence that T' entails.

theorem FirstOrder.Language.Theoryω.Entails.cut {L : Language} {T : L.Theoryω} {φ ψ : L.Sentenceω} (hψ : T.Entails ψ) (h : (insert ψ T).Entails φ) : T.Entails φ

Cut. A sentence entailed by a theory may be used as an additional hypothesis.

theorem FirstOrder.Language.Theoryω.Entails.ex_not_of_not_all {L : Language} {T : L.Theoryω} {φ : L.BoundedFormulaω Empty 1} (h : T.Entails (BoundedFormulaInf.all φ).not) : T.Entails (BoundedFormulaInf.not φ).ex

A theory entailing ¬ ∀ x, φ x entails ∃ x, ¬ φ x.

theorem FirstOrder.Language.Theoryω.entails_iff_not_isSatisfiable {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} : T.Entails φ ↔ ¬(insert (BoundedFormulaInf.not φ) T).IsSatisfiable

Entailment is refutation. A theory entails a sentence exactly when the theory together with the negation of the sentence is unsatisfiable. This is the L_{ω₁ω} form of Mathlib's Theory.models_iff_not_satisfiable.

theorem FirstOrder.Language.Theoryω.Entails.realize_of_small {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} (h : T.Entails φ) (M : Type w) [L.Structure M] [Nonempty M] [Small.{max u v, w} M] (hM : T.Model M) : SentenceInf.Realize φ M

A sentence entailed by a theory holds in every nonempty model of the theory that is small in the universe max u v, for instance in every countable model in any universe.

theorem FirstOrder.Language.Theoryω.isSatisfiable_iff_not_entails_bot {L : Language} {T : L.Theoryω} : T.IsSatisfiable ↔ ¬T.Entails ⊥

A theory is satisfiable exactly when it does not entail the false sentence.

@[simp]

theorem FirstOrder.Language.Theoryω.entails_conjunction_iff {L : Language} {T T' : L.Theoryω} (hT' : Set.Countable T') : T.Entails (T'.conjunction hT') ↔ ∀ ψ ∈ T', T.Entails ψ

A theory entails the conjunction of a countable theory exactly when it entails each of its sentences.

Entailment between sentences

def FirstOrder.Language.Sentenceω.Entails {L : Language} (φ ψ : L.Sentenceω) : Prop

A sentence entails another when the theory consisting of the first sentence entails the second: every nonempty model of φ in the universe max u v satisfies ψ.

theorem FirstOrder.Language.Sentenceω.entails_def {L : Language} {φ ψ : L.Sentenceω} : φ.Entails ψ ↔ {φ}.Entails ψ

Entailment between sentences is entailment by the singleton theory.

theorem FirstOrder.Language.Sentenceω.entails_iff {L : Language} {φ ψ : L.Sentenceω} : φ.Entails ψ ↔ ∀ (M : Type (max u v)) [inst : L.Structure M] [Nonempty M], SentenceInf.Realize φ M → SentenceInf.Realize ψ M

A sentence entails another when every nonempty model of the first in the universe max u v satisfies the second.

theorem FirstOrder.Language.Sentenceω.Entails.refl {L : Language} (φ : L.Sentenceω) : φ.Entails φ

Every sentence entails itself.

theorem FirstOrder.Language.Sentenceω.Entails.trans {L : Language} {φ ψ χ : L.Sentenceω} (h₁ : φ.Entails ψ) (h₂ : ψ.Entails χ) : φ.Entails χ

Entailment between sentences is transitive.

theorem FirstOrder.Language.Theoryω.entails_iff_conjunction_entails {L : Language} {T : L.Theoryω} {φ : L.Sentenceω} (hT : Set.Countable T) : T.Entails φ ↔ (T.conjunction hT).Entails φ

A countable theory entails what its conjunction entails. This reduces the entailments of a countable theory to entailments between two sentences.

Agreement with first-order satisfiability and entailment

@[simp]

theorem FirstOrder.Language.Theoryω.isSatisfiable_image_toOmega_iff {L : Language} {T : L.Theory} : IsSatisfiable (BoundedFormula.toOmega '' T) ↔ T.IsSatisfiable

The image of a first-order theory in L_{ω₁ω} is satisfiable exactly when the first-order theory is satisfiable in the sense of Mathlib's Theory.IsSatisfiable.

@[simp]

theorem FirstOrder.Language.Theoryω.entails_image_toOmega_iff {L : Language} {T : L.Theory} {φ : L.Sentence} : Entails (BoundedFormula.toOmega '' T) (BoundedFormula.toOmega φ) ↔ T ⊨ᵇ φ

The image of a first-order theory in L_{ω₁ω} entails the image of a first-order sentence exactly when the first-order theory models the sentence in the sense of Mathlib's Theory.ModelsBoundedFormula.

@[simp]

theorem FirstOrder.Language.Sentenceω.entails_toOmega_iff {L : Language} {φ ψ : L.Sentence} : Entails (BoundedFormula.toOmega φ) (BoundedFormula.toOmega ψ) ↔ {φ} ⊨ᵇ ψ

Entailment between the images of two first-order sentences in L_{ω₁ω} is first-order entailment in the sense of Mathlib's Theory.ModelsBoundedFormula.