Henkin-complete sets and their term models

A set S of L_{ω₁ω} sentences of the Henkin expansion L[[ℕ]] is Henkin complete when it contains the target of every clause of a consistency property: an implication in S brings the negation of its hypothesis or its conclusion into S, a universal sentence in S brings all of its instances at Henkin constants, a negated universal sentence brings a counterexample at some Henkin constant, equality is reflexive and substitutive into atomic formulas, every closed term is equal to some Henkin constant, and so on. The model existence theorem produces such a set as the union of a fair enumeration of members of a consistency property.

A Henkin-complete set has a term model: the Henkin constants modulo the equalities asserted in S. A function symbol applied to classes is the class of a constant that S asserts to be equal to the corresponding closed term, and a relation holds of classes when S contains the corresponding relational sentence. Every element of the term model is the interpretation of a Henkin constant, and the term model is countable.

Suppose in addition that S contains neither ⊥ nor a sentence together with its negation. The truth lemma then consists of two forward implications, for every formula φ with n bound positions and every tuple c of n Henkin constants: if S contains the instance φ[c] then φ holds of the constants c in the term model, and if S contains ¬φ[c] then it does not. No maximality of S and no decision between φ and ¬φ is needed. Under the same hypotheses the term model is a model of S (ConsistencyProperty.HenkinComplete.model).

Main definitions

• FirstOrder.Language.ConsistencyProperty.HenkinComplete: sets of L[[ℕ]] sentences that contain the target of every clause of a consistency property.
• FirstOrder.Language.ConsistencyProperty.HenkinComplete.TermModel: the Henkin constants modulo the equalities asserted in a Henkin-complete set, with its L[[ℕ]]-structure.

Main results

• FirstOrder.Language.ConsistencyProperty.HenkinComplete.eq_congr: substitution of equals into atomic formulas at any number of bound positions, with eq_symm and eq_trans.
• FirstOrder.Language.ConsistencyProperty.HenkinComplete.con_surjective: every element of the term model is named by a Henkin constant.
• FirstOrder.Language.ConsistencyProperty.HenkinComplete.realize_eq_con_of_mem: a closed term denotes the class of any Henkin constant that S asserts to be equal to it.
• FirstOrder.Language.ConsistencyProperty.HenkinComplete.realize_iff_mem_of_isAtomic: an atomic sentence holds in the term model exactly when it belongs to S.
• FirstOrder.Language.ConsistencyProperty.HenkinComplete.truth_pos and FirstOrder.Language.ConsistencyProperty.HenkinComplete.truth_neg: the truth lemma.
• FirstOrder.Language.ConsistencyProperty.HenkinComplete.model: the term model of a Henkin-complete set containing no contradiction is a model of it.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, §4.1.
• H. J. Keisler, Model Theory for Infinitary Logic, North-Holland, 1971.
• cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Methods/Henkin/CountableCompletion/ConsistencyPropertyEqOn.lean, QuotientTermModel.lean and QuotientTruthLemma.lean, which formalize a Henkin-completeness predicate, a quotient term model and the two-polarity forward truth lemma. Divergences from that source: the clauses are those of FirstOrder.Language.ConsistencyProperty, with function symbols, substitution of equals into all atomic formulas and a naming clause for closed terms; the absence of ⊥ and of contradictions is kept out of the predicate; the term model is a quotient of the Henkin constants rather than of the closed terms; and the truth lemma is a structural induction over formulas with bound positions instantiated by tuples of constants.

structure FirstOrder.Language.ConsistencyProperty.HenkinComplete {L : Language} (S : (L.withConstants ℕ).Theoryω) : Prop

A set S of L[[ℕ]] sentences is Henkin complete when it contains the target of every clause of a consistency property: one chosen component of each disjunctive sentence in S, every component of each conjunctive one, every instance at a Henkin constant of each universal sentence, a counterexample at some Henkin constant to each negated universal sentence, every reflexive equation of closed terms, the result of substituting equals into each atomic sentence, and an equation naming each closed term by a Henkin constant.

• imp (φ ψ : (L.withConstants ℕ).Sentenceω) : BoundedFormulaInf.imp φ ψ ∈ S → BoundedFormulaInf.not φ ∈ S ∨ ψ ∈ S

  An implication brings the negation of its hypothesis or its conclusion.

• not_imp (φ ψ : (L.withConstants ℕ).Sentenceω) : (BoundedFormulaInf.imp φ ψ).not ∈ S → φ ∈ S ∧ BoundedFormulaInf.not ψ ∈ S

  A negated implication brings its hypothesis and the negation of its conclusion.

• iInf (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaInf.iInf φs ∈ S → ∀ (k : ℕ), φs k ∈ S

  A countable conjunction brings each of its conjuncts.

• not_iInf (φs : ℕ → (L.withConstants ℕ).Sentenceω) : (BoundedFormulaInf.iInf φs).not ∈ S → ∃ (k : ℕ), BoundedFormulaInf.not (φs k) ∈ S

  A negated countable conjunction brings the negation of some conjunct.

• iSup (φs : ℕ → (L.withConstants ℕ).Sentenceω) : BoundedFormulaInf.iSup φs ∈ S → ∃ (k : ℕ), φs k ∈ S

  A countable disjunction brings some disjunct.

• not_iSup (φs : ℕ → (L.withConstants ℕ).Sentenceω) : (BoundedFormulaInf.iSup φs).not ∈ S → ∀ (k : ℕ), BoundedFormulaInf.not (φs k) ∈ S

  A negated countable disjunction brings the negation of each disjunct.

• all (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : BoundedFormulaInf.all φ ∈ S → ∀ (c : ℕ), BoundedFormulaInf.inst φ (L.con c).term ∈ S

  A universal sentence brings its instance at every Henkin constant.

• not_all (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : (BoundedFormulaInf.all φ).not ∈ S → ∃ (c : ℕ), BoundedFormulaInf.not (BoundedFormulaInf.inst φ (L.con c).term) ∈ S

  A negated universal sentence brings a counterexample at some Henkin constant.

• eq_refl (t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)) : BoundedFormulaInf.equal t t ∈ S

  Every closed term equals itself.

• eq_subst (t t' : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : BoundedFormulaInf.IsAtomic φ → BoundedFormulaInf.equal t t' ∈ S → BoundedFormulaInf.inst φ t ∈ S → BoundedFormulaInf.inst φ t' ∈ S

  Equals can be substituted for equals in an atomic formula.

• eq_name (t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)) : ∃ (c : ℕ), BoundedFormulaInf.equal (L.con c).term t ∈ S

  Every closed term equals some Henkin constant.

Equality

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.eq_congr {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) {n : ℕ} {φ : (L.withConstants ℕ).BoundedFormulaω Empty n} (hφ : BoundedFormulaInf.IsAtomic φ) {s t : Fin n → (L.withConstants ℕ).Term (Empty ⊕ Fin 0)} (hst : ∀ (i : Fin n), BoundedFormulaInf.equal (s i) (t i) ∈ S) (hs : BoundedFormulaInf.substBounds s φ ∈ S) : BoundedFormulaInf.substBounds t φ ∈ S

Substitution of equals into an atomic formula at any number of bound positions: if S contains sᵢ = tᵢ for every bound position i of the atomic formula φ, then S contains φ[t] as soon as it contains φ[s].

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.eq_symm {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) {t t' : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)} (h : BoundedFormulaInf.equal t t' ∈ S) : BoundedFormulaInf.equal t' t ∈ S

Equality of closed terms in a Henkin-complete set is symmetric.

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.eq_trans {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) {t t' t'' : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)} (h : BoundedFormulaInf.equal t t' ∈ S) (h' : BoundedFormulaInf.equal t' t'' ∈ S) : BoundedFormulaInf.equal t t'' ∈ S

Equality of closed terms in a Henkin-complete set is transitive.

The term model

def FirstOrder.Language.ConsistencyProperty.HenkinComplete.TermModel {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) : Type

The term model of a Henkin-complete set S: the Henkin constants modulo the equalities asserted in S. A function symbol applied to classes is the class of a constant that S asserts to be equal to the corresponding closed term, and a relation holds of classes when S contains the corresponding relational sentence.

@[instance_reducible]

noncomputable def FirstOrder.Language.ConsistencyProperty.HenkinComplete.termModelStructure {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) : (L.withConstants ℕ).Structure hS.TermModel

The L[[ℕ]]-structure of the term model: a function symbol applied to classes of constants is the class of the constant naming the corresponding closed term, and a relation holds of classes of constants when S contains the corresponding relational sentence.

@[instance_reducible]

noncomputable instance FirstOrder.Language.ConsistencyProperty.HenkinComplete.instStructureWithConstantsNatTermModel {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) : (L.withConstants ℕ).Structure hS.TermModel

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.con_surjective {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) : Function.Surjective fun (c : ℕ) => ↑(L.con c)

Every element of the term model is named by a Henkin constant.

instance FirstOrder.Language.ConsistencyProperty.HenkinComplete.instCountableTermModel {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) : Countable hS.TermModel

instance FirstOrder.Language.ConsistencyProperty.HenkinComplete.instNonemptyTermModel {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) : Nonempty hS.TermModel

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.con_eq_con_iff {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) {c d : ℕ} : ↑(L.con c) = ↑(L.con d) ↔ BoundedFormulaInf.equal (L.con c).term (L.con d).term ∈ S

Two Henkin constants denote the same element of the term model exactly when S asserts that they are equal.

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.realize_eq_con_of_mem {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) {t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)} {c : ℕ} (h : BoundedFormulaInf.equal (L.con c).term t ∈ S) (v : Empty ⊕ Fin 0 → hS.TermModel) : Term.realize v t = ↑(L.con c)

Evaluation in the term model: a closed term denotes the interpretation of any Henkin constant that S asserts to be equal to it.

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.realize_iff_mem_of_isAtomic {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) {φ : (L.withConstants ℕ).Sentenceω} (hφ : BoundedFormulaInf.IsAtomic φ) : SentenceInf.Realize φ hS.TermModel ↔ φ ∈ S

Atomic semantics of the term model: an atomic sentence holds in the term model exactly when it belongs to S.

The truth lemma

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.truth_pos {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) (hbot : ⊥ ∉ S) (hcon : ∀ φ ∈ S, BoundedFormulaInf.not φ ∉ S) {n : ℕ} {φ : (L.withConstants ℕ).BoundedFormulaω Empty n} {c : Fin n → ℕ} (h : BoundedFormulaInf.substBounds (fun (i : Fin n) => (L.con (c i)).term) φ ∈ S) : BoundedFormulaInf.Realize φ Empty.elim fun (i : Fin n) => ↑(L.con (c i))

Truth lemma, positive half: if a Henkin-complete set S containing neither ⊥ nor a sentence together with its negation contains the instance of φ at the Henkin constants c, then φ holds of the interpretations of c in the term model.

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.truth_neg {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) (hbot : ⊥ ∉ S) (hcon : ∀ φ ∈ S, BoundedFormulaInf.not φ ∉ S) {n : ℕ} {φ : (L.withConstants ℕ).BoundedFormulaω Empty n} {c : Fin n → ℕ} (h : (BoundedFormulaInf.substBounds (fun (i : Fin n) => (L.con (c i)).term) φ).not ∈ S) : ¬BoundedFormulaInf.Realize φ Empty.elim fun (i : Fin n) => ↑(L.con (c i))

Truth lemma, negative half: if a Henkin-complete set S containing neither ⊥ nor a sentence together with its negation contains the negated instance of φ at the Henkin constants c, then φ fails of the interpretations of c in the term model.

theorem FirstOrder.Language.ConsistencyProperty.HenkinComplete.model {L : Language} {S : (L.withConstants ℕ).Theoryω} (hS : HenkinComplete S) (hbot : ⊥ ∉ S) (hcon : ∀ φ ∈ S, BoundedFormulaInf.not φ ∉ S) : S.Model hS.TermModel

The term model is a model: a Henkin-complete set containing neither ⊥ nor a sentence together with its negation is satisfied by its term model.