Consistency properties

A consistency property over a language L is a family of sets of L_{ω₁ω} sentences of the Henkin expansion L[[ℕ]] that contains no outright contradiction and is closed under the decomposition of every connective and quantifier: whenever a member contains a compound sentence, the family also contains the member enlarged by a suitable component of that sentence (one chosen component for a disjunctive sentence, every component for a conjunctive one). The quantifier clauses instantiate only the Henkin constants L.con c, and the equality clauses make every closed term equal to some Henkin constant, so that a model built from a member can be one in which every element is the interpretation of a Henkin constant.

The syntax has only implication and falsum as propositional primitives, with ¬φ the formula φ.imp ⊥. A negated compound sentence is therefore decomposed by its own clause, and double negation is the negated-implication clause at ψ = ⊥ (ConsistencyProperty.not_not).

Two clauses common in finitary presentations are absent. Closure under unions of increasing chains is absent because L_{ω₁ω} is not compact, so the satisfiable sets of sentences are not closed under unions of chains. A decision clause, adding φ or ¬φ to every member, is absent because model existence can be proved by a fair enumeration of decomposition requests that never needs it. Substitution of equals is required only into atomic formulas.

The basic example is semantic: in an L[[ℕ]]-structure in which every element is the interpretation of a Henkin constant, the sets of sentences true in the structure form a consistency property (ConsistencyProperty.ofModel). The model existence theorem is the converse: a countable member of a consistency property over a countable language has a countable model of exactly this kind.

A second instance, the one behind the omitting types theorem, is built from satisfiability rather than from one model. For a formation-closed fragment A and a theory T of sentences of A, the satisfiable theories made of T and finitely many instances of members of A at tuples of Henkin constants form a consistency property (ConsistencyProperty.ofSatisfiable). Only finitely many Henkin constants occur in such a theory, so the witness clauses are met by reinterpreting a fresh constant in a model; formation closure supplies the negations and the atomic sentences that the clauses add.

Main definitions

• FirstOrder.Language.ConsistencyProperty: consistency properties over L[[ℕ]].
• FirstOrder.Language.ConsistencyProperty.ofModel: the sets of sentences true in a structure whose elements are all named by Henkin constants.
• FirstOrder.Language.ConsistencyProperty.ofSatisfiable: the satisfiable theories made of a theory of sentences of a formation-closed fragment and finitely many instances of its members.

Main results

• FirstOrder.Language.ConsistencyProperty.not_not: double negation elimination.
• FirstOrder.Language.ConsistencyProperty.mem_ofModel_iff: the members of ofModel are the theories modelled by the structure.
• FirstOrder.Language.ConsistencyProperty.onTheoryω_mem_ofSatisfiable: a satisfiable theory of sentences of the fragment is a member of ofSatisfiable.
• FirstOrder.Language.ConsistencyProperty.exists_model_of_mem_ofSatisfiable and FirstOrder.Language.ConsistencyProperty.insert_mem_ofSatisfiable: a member of ofSatisfiable has a model expanding an L-structure by an interpretation of the Henkin constants, and adding an instance keeps a satisfiable theory a member.

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/ConsistencyProperty.lean and InfinitaryLogic/Methods/Henkin/SatisfiableConsistencyProperty.lean, which formalize consistency properties and the true-in-a-model instance. Divergences from that source: the clauses are stated over the Henkin expansion L[[ℕ]], with the quantifier clauses instantiating Henkin constants through bound substitution and an explicit naming clause for closed terms; the chain-closure and decision clauses are dropped; and the true-in-a-model instance names elements by Henkin constants rather than by a naming function into closed terms.

structure FirstOrder.Language.ConsistencyProperty (L : Language) : Type (max u v)

A consistency property over L: a family of sets of L_{ω₁ω} sentences of the Henkin expansion L[[ℕ]] containing neither ⊥ nor a sentence together with its negation, and closed under the decomposition of each connective and quantifier, with the Henkin constants as witnesses and as names for closed terms.

• sets : Set (L.withConstants ℕ).Theoryω

  The family of consistent sets of sentences.

• no_falsum (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ⊥ ∉ s

  No consistent set contains ⊥.

• no_contradiction (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ φ ∈ s, BoundedFormulaInf.not φ ∉ s

  No consistent set contains a sentence together with its negation.

• imp (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (φ ψ : (L.withConstants ℕ).Sentenceω), BoundedFormulaInf.imp φ ψ ∈ s → insert (BoundedFormulaInf.not φ) s ∈ self.sets ∨ insert ψ s ∈ self.sets

  An implication can be decomposed into the negation of its hypothesis or its conclusion.

• not_imp (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (φ ψ : (L.withConstants ℕ).Sentenceω), (BoundedFormulaInf.imp φ ψ).not ∈ s → insert φ s ∈ self.sets ∧ insert (BoundedFormulaInf.not ψ) s ∈ self.sets

  A negated implication can be decomposed into its hypothesis and the negation of its conclusion.

• iInf (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (φs : ℕ → (L.withConstants ℕ).Sentenceω), BoundedFormulaInf.iInf φs ∈ s → ∀ (k : ℕ), insert (φs k) s ∈ self.sets

  A countable conjunction can be decomposed into each of its conjuncts.

• not_iInf (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (φs : ℕ → (L.withConstants ℕ).Sentenceω), (BoundedFormulaInf.iInf φs).not ∈ s → ∃ (k : ℕ), insert (BoundedFormulaInf.not (φs k)) s ∈ self.sets

  A negated countable conjunction can be decomposed into the negation of some conjunct.

• iSup (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (φs : ℕ → (L.withConstants ℕ).Sentenceω), BoundedFormulaInf.iSup φs ∈ s → ∃ (k : ℕ), insert (φs k) s ∈ self.sets

  A countable disjunction can be decomposed into some disjunct.

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

  A negated countable disjunction can be decomposed into the negation of each disjunct.

• all (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1), BoundedFormulaInf.all φ ∈ s → ∀ (c : ℕ), insert (BoundedFormulaInf.inst φ (L.con c).term) s ∈ self.sets

  A universal sentence can be instantiated at every Henkin constant.

• not_all (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1), (BoundedFormulaInf.all φ).not ∈ s → ∃ (c : ℕ), insert (BoundedFormulaInf.not (BoundedFormulaInf.inst φ (L.con c).term)) s ∈ self.sets

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

• eq_refl (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)), insert (BoundedFormulaInf.equal t t) s ∈ self.sets

  Every closed term equals itself.

• eq_subst (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (t t' : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1), BoundedFormulaInf.IsAtomic φ → BoundedFormulaInf.equal t t' ∈ s → BoundedFormulaInf.inst φ t ∈ s → insert (BoundedFormulaInf.inst φ t') s ∈ self.sets

  Equals can be substituted for equals in an atomic formula.

• eq_name (s : (L.withConstants ℕ).Theoryω) : s ∈ self.sets → ∀ (t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)), ∃ (c : ℕ), insert (BoundedFormulaInf.equal (L.con c).term t) s ∈ self.sets

  Every closed term equals some Henkin constant.

theorem FirstOrder.Language.ConsistencyProperty.ext {L : Language} {x y : L.ConsistencyProperty} (sets : x.sets = y.sets) : x = y

theorem FirstOrder.Language.ConsistencyProperty.ext_iff {L : Language} {x y : L.ConsistencyProperty} : x = y ↔ x.sets = y.sets

theorem FirstOrder.Language.ConsistencyProperty.not_not {L : Language} (C : L.ConsistencyProperty) {s : (L.withConstants ℕ).Theoryω} (hs : s ∈ C.sets) {φ : (L.withConstants ℕ).Sentenceω} (h : (BoundedFormulaInf.not φ).not ∈ s) : insert φ s ∈ C.sets

Double negation elimination: a doubly negated sentence can be replaced by the sentence.

def FirstOrder.Language.ConsistencyProperty.ofModel {L : Language} (M : Type w) [(L.withConstants ℕ).Structure M] (hM : Function.Surjective fun (c : ℕ) => ↑(L.con c)) : L.ConsistencyProperty

The satisfaction instance: in an L[[ℕ]]-structure in which every element is the interpretation of a Henkin constant, the sets of sentences true in the structure form a consistency property. For an L-structure M and a surjection e : ℕ → M, the expansion constantsOn.structure e interpreting L.con c as e c is such a structure.

@[simp]

theorem FirstOrder.Language.ConsistencyProperty.mem_ofModel_iff {L : Language} {M : Type w} [(L.withConstants ℕ).Structure M] {hM : Function.Surjective fun (c : ℕ) => ↑(L.con c)} {s : (L.withConstants ℕ).Theoryω} : s ∈ (ofModel M hM).sets ↔ s.Model M

The members of ofModel M hM are the theories of which M is a model.

def FirstOrder.Language.ConsistencyProperty.ofSatisfiable {L : Language} (T : L.Theoryω) (A : L.Fragment) (hA : A.FormationClosed) (hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A) : L.ConsistencyProperty

The consistency property of satisfiable instances. For a formation-closed fragment A and a theory T of sentences of A, the satisfiable theories of L[[ℕ]] made of the image of T and a finite set of instances of members of A at tuples of Henkin constants form a consistency property.

@[simp]

theorem FirstOrder.Language.ConsistencyProperty.mem_ofSatisfiable_iff {L : Language} {A : L.Fragment} {T : L.Theoryω} {hA : A.FormationClosed} {hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A} {s : (L.withConstants ℕ).Theoryω} : s ∈ (ofSatisfiable T A hA hT).sets ↔ (∃ (σ : (L.withConstants ℕ).Theoryω), Set.Finite σ ∧ σ ⊆ A.instances ℕ ∧ s = (L.lhomWithConstants ℕ).onTheoryω T ∪ σ) ∧ s.IsSatisfiable

The members of ofSatisfiable T A hA hT are the satisfiable theories made of the sentences of T, mapped to L[[ℕ]], and finitely many instances of members of A.

theorem FirstOrder.Language.ConsistencyProperty.onTheoryω_mem_ofSatisfiable {L : Language} {A : L.Fragment} {T : L.Theoryω} {hA : A.FormationClosed} {hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A} (h : T.IsSatisfiable) : (L.lhomWithConstants ℕ).onTheoryω T ∈ (ofSatisfiable T A hA hT).sets

A satisfiable theory of sentences of A, mapped to L[[ℕ]], is a member of ofSatisfiable.

theorem FirstOrder.Language.ConsistencyProperty.exists_model_of_mem_ofSatisfiable {L : Language} {A : L.Fragment} {T : L.Theoryω} {hA : A.FormationClosed} {hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A} {s : (L.withConstants ℕ).Theoryω} (hs : s ∈ (ofSatisfiable T A hA hT).sets) : ∃ (M : Type (max u v)) (x : L.Structure M) (_ : Nonempty M) (e : ℕ → M) (F : Set ℕ), F.Finite ∧ (∀ φ ∈ s, ∃ (n : ℕ) (χ : L.BoundedFormulaω Empty n) (d : Fin n → ℕ), BoundedFormulaInf.instConstants χ d = φ ∧ ∀ (i : Fin n), d i ∈ F) ∧ s.Model M

Members of ofSatisfiable have expansion models: a member has a nonempty model that is the expansion of an L-structure by an interpretation e of the Henkin constants, and its sentences are instances at tuples of constants from one finite set F.

theorem FirstOrder.Language.ConsistencyProperty.insert_mem_ofSatisfiable {L : Language} {A : L.Fragment} {T : L.Theoryω} {hA : A.FormationClosed} {hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A} {s : (L.withConstants ℕ).Theoryω} {X : (L.withConstants ℕ).Sentenceω} (hs : s ∈ (ofSatisfiable T A hA hT).sets) (hX : X ∈ A.instances ℕ) (hsat : (insert X s).IsSatisfiable) : insert X s ∈ (ofSatisfiable T A hA hT).sets

Adding an instance to a member of ofSatisfiable gives a member, provided the enlarged theory is satisfiable.