Model existence for consistency properties

A countable member of a consistency property over a countable language has a countable, nonempty model in every universe, with every element named by a Henkin constant. The fair enumeration supplies a Henkin-complete superset without contradictions; its quotient term model satisfies the starting set by the two-polarity truth lemma. Moving this model to another universe preserves both satisfaction and the surjectivity of the interpretations of the constants.

The limit need not itself belong to the consistency property. No decision clause or closure under unions of increasing chains is used.

The model can moreover be made to omit countably many countable partial types p i (ConsistencyProperty.model_existence_omitting), provided the consistency property lets each of them be refuted at every tuple of Henkin constants: for every member t and every tuple c, some ψ ∈ p i has t + ¬ψ[c] in the property.

Main results

• FirstOrder.Language.ConsistencyProperty.henkinComplete_limit: the limit of a surjective request schedule, starting from an enumerated member, is Henkin complete.
• FirstOrder.Language.ConsistencyProperty.model_existence: a countable member has a countable nonempty model, in any universe, whose elements are all named by Henkin constants.
• FirstOrder.Language.ConsistencyProperty.model_existence_omitting: the model can also be made to omit countably many countable partial types that the consistency property refutes at every tuple.

Implementation notes

Omission is obtained without changing the enumeration: every member of C, and in particular s, is enlarged by the countable disjunctions ⋁_{ψ ∈ p i} ¬ψ[c]. The enlarged sets again form a consistency property, since every member can decide each adjoined disjunction by the hypothesis, and none contains the negation of one: adding the chosen refutation ¬ψ[c] and then the negated disjunct ¬¬ψ[c] would produce a contradiction. A model of the enlarged starting set in which every element is named refutes some member of p i at every tuple.

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.

This assembles the fair enumeration and quotient truth lemma of the imported modules; their module docstrings record the relationship to Cameron Freer's cameronfreer/infinitary-logic.

theorem FirstOrder.Language.ConsistencyProperty.henkinComplete_limit {L : Language} (C : L.ConsistencyProperty) {s : (L.withConstants ℕ).Theoryω} (hs : s ∈ C.sets) {e : ℕ → (L.withConstants ℕ).Sentenceω} (he : s ⊆ Set.range e) {q : ℕ → Request L} (hq : Function.Surjective q) : HenkinComplete (C.limit s e q)

The limit of a fair enumeration starting from a member of a consistency property is Henkin complete. The enumeration of the starting set may include sentences outside it.

theorem FirstOrder.Language.ConsistencyProperty.model_existence {L : Language} [Countable ((n : ℕ) × L.Functions n)] [Countable ((n : ℕ) × L.Relations n)] (C : L.ConsistencyProperty) {s : (L.withConstants ℕ).Theoryω} (hs : s ∈ C.sets) (hsc : Set.Countable s) : ∃ (M : Type w) (x : (L.withConstants ℕ).Structure M), Countable M ∧ Nonempty M ∧ s.Model M ∧ Function.Surjective fun (c : ℕ) => ↑(L.con c)

Model existence. Every countable member of a consistency property over a language with countably many function and relation symbols has a countable nonempty model in any universe. Every element of the model is the interpretation of a Henkin constant.

Omitting types

theorem FirstOrder.Language.ConsistencyProperty.model_existence_omitting {L : Language} [Countable ((n : ℕ) × L.Functions n)] [Countable ((n : ℕ) × L.Relations n)] (C : L.ConsistencyProperty) {ι : Type u_1} [Countable ι] {n : ι → ℕ} (p : (i : ι) → Set ((L.withConstants ℕ).BoundedFormulaω Empty (n i))) (hp : ∀ (i : ι), (p i).Countable) (hC : ∀ (i : ι), ∀ t ∈ C.sets, ∀ (c : Fin (n i) → ℕ), ∃ ψ ∈ p i, insert (BoundedFormulaInf.substBounds (fun (j : Fin (n i)) => (L.con (c j)).term) ψ).not t ∈ C.sets) {s : (L.withConstants ℕ).Theoryω} (hs : s ∈ C.sets) (hsc : Set.Countable s) : ∃ (M : Type w) (x : (L.withConstants ℕ).Structure M), Countable M ∧ Nonempty M ∧ s.Model M ∧ (Function.Surjective fun (c : ℕ) => ↑(L.con c)) ∧ ∀ (i : ι), OmitsType M (p i)

The model existence theorem with omitted types. Over a language with countably many function and relation symbols, let p i be countably many countable partial types such that every member t of the consistency property C and every tuple c of Henkin constants admit some ψ ∈ p i for which t together with the refutation ¬ψ[c] is again a member. Then every countable member s of C has a countable nonempty model, in any universe w, in which every element is the interpretation of a Henkin constant and which omits every p i.