Henkin Construction

This file provides the infrastructure for the Henkin-style proof of the model existence theorem for Lω₁ω. The construction proceeds in several stages:

1. Maximal consistent extension: Extend a consistent set of sentences to a maximal one within the consistency property (using Zorn's lemma or sequential enumeration for countable languages).
2. Term model: Build a model from equivalence classes of closed terms.
3. Truth lemma: Show that truth in the term model corresponds to membership in the maximal consistent set.

Main Results

• ConsistencyProperty.exists_maximal: Every consistent set extends to a maximal consistent set (requires chain-closure of C.sets).
• ConsistencyProperty.MaximalConsistent: Predicate for maximal consistency.
• Properties of maximal consistent sets (closure under connectives).

References

• [Mar16], §4.1
• [Kei71]

Maximal Consistent Sets

def FirstOrder.Language.ConsistencyProperty.MaximalConsistent {L : Language} (C : L.ConsistencyProperty) (S : Set L.Sentenceω) : Prop

A set is maximal consistent in a consistency property if it is consistent and no proper superset is consistent. Uses Mathlib's Maximal predicate: Maximal (· ∈ C.sets) S means S ∈ C.sets ∧ ∀ S', S' ∈ C.sets → S ⊆ S' → S = S'.

Equations

• C.MaximalConsistent S = Maximal (fun (x : Set L.Sentenceω) => x ∈ C.sets) S

theorem FirstOrder.Language.ConsistencyProperty.exists_maximal {L : Language} (C : L.ConsistencyProperty) (S : Set L.Sentenceω) (hS : S ∈ C.sets) : ∃ (S' : Set L.Sentenceω), S ⊆ S' ∧ C.MaximalConsistent S'

Every consistent set in a consistency property can be extended to a maximal consistent set, by Zorn's lemma.

The chain-closure axiom of ConsistencyProperty ensures that the union of any nonempty chain of consistent sets remains consistent, providing the upper bound required by Zorn's lemma.

Properties of Maximal Consistent Sets

These properties follow from maximality: if adding a sentence preserves consistency, then it must already be in the maximal set.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.consistent {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) : S ∈ C.sets

A maximal consistent set is consistent.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.mem_of_union_consistent {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ : L.Sentenceω} (h : S ∪ {φ} ∈ C.sets) : φ ∈ S

If S ∪ {φ} is consistent and S is maximal, then φ ∈ S.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.imp_mem {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ ψ : L.Sentenceω} (h : BoundedFormulaω.imp φ ψ ∈ S) : BoundedFormulaω.not φ ∈ S ∨ ψ ∈ S

In a maximal consistent set, for every implication φ → ψ in S, either ¬φ ∈ S or ψ ∈ S.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.neg_imp_mem {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ ψ : L.Sentenceω} (h : (BoundedFormulaω.imp φ ψ).not ∈ S) : φ ∈ S ∧ BoundedFormulaω.not ψ ∈ S

In a maximal consistent set, negated implication gives both components: if ¬(φ → ψ) ∈ S, then φ ∈ S and ¬ψ ∈ S.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.not_not_mem {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ : L.Sentenceω} (h : (BoundedFormulaω.not φ).not ∈ S) : φ ∈ S

In a maximal consistent set, double negation elimination holds.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.iInf_mem {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φs : ℕ → L.Sentenceω} (h : BoundedFormulaω.iInf φs ∈ S) (k : ℕ) : φs k ∈ S

In a maximal consistent set, if ⋀ᵢ φᵢ ∈ S, then φₖ ∈ S for all k.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.neg_iInf_mem {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φs : ℕ → L.Sentenceω} (h : (BoundedFormulaω.iInf φs).not ∈ S) : ∃ (k : ℕ), BoundedFormulaω.not (φs k) ∈ S

In a maximal consistent set, if ¬(⋀ᵢ φᵢ) ∈ S, then ¬φₖ ∈ S for some k.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.iSup_mem {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φs : ℕ → L.Sentenceω} (h : BoundedFormulaω.iSup φs ∈ S) : ∃ (k : ℕ), φs k ∈ S

In a maximal consistent set, if ⋁ᵢ φᵢ ∈ S, then φₖ ∈ S for some k.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.neg_iSup_mem {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φs : ℕ → L.Sentenceω} (h : (BoundedFormulaω.iSup φs).not ∈ S) (k : ℕ) : BoundedFormulaω.not (φs k) ∈ S

In a maximal consistent set, if ¬(⋁ᵢ φᵢ) ∈ S, then ¬φₖ ∈ S for all k.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.decide {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) (φ : L.Sentenceω) : φ ∈ S ∨ BoundedFormulaω.not φ ∈ S

A maximal consistent set decides every sentence: either φ ∈ S* or ¬φ ∈ S*.

theorem FirstOrder.Language.ConsistencyProperty.MaximalConsistent.not_mem_iff {L : Language} {C : L.ConsistencyProperty} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) (φ : L.Sentenceω) : BoundedFormulaω.not φ ∈ S ↔ φ ∉ S

In a maximal consistent set, ¬φ ∈ S ↔ φ ∉ S.

theorem FirstOrder.Language.ConsistencyPropertyEq.MaximalConsistent.all_mem {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ : L.Formulaω (Fin 1)} (h : (BoundedFormulaω.relabel Sum.inr φ).all ∈ S) (t : L.Term Empty) : (BoundedFormulaω.subst φ fun (x : Fin 1) => t) ∈ S

In a maximal consistent set with ConsistencyPropertyEq, universal quantification: (∀x.φ) ∈ S* iff for all closed terms t, φ[x/t] ∈ S*.

theorem FirstOrder.Language.ConsistencyPropertyEq.MaximalConsistent.ex_mem {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ : L.Formulaω (Fin 1)} (h : (BoundedFormulaω.relabel Sum.inr φ).ex ∈ S) : ∃ (t : L.Term Empty), (BoundedFormulaω.subst φ fun (x : Fin 1) => t) ∈ S

In a maximal consistent set with ConsistencyPropertyEq, existential quantification: if (∃x.φ) ∈ S* then there exists a closed term t with φ[x/t] ∈ S*.

theorem FirstOrder.Language.ConsistencyPropertyEq.MaximalConsistent.neg_all_mem {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ : L.Formulaω (Fin 1)} (h : (BoundedFormulaω.relabel Sum.inr φ).all.not ∈ S) : ∃ (t : L.Term Empty), (BoundedFormulaω.subst φ fun (x : Fin 1) => t).not ∈ S

In a maximal consistent set, if ¬(∀x.φ(x)) ∈ S, then ∃t, ¬φ(t) ∈ S.

theorem FirstOrder.Language.ConsistencyPropertyEq.MaximalConsistent.all_bound_mem {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ : L.BoundedFormulaω Empty 1} (h : φ.all ∈ S) (t : L.Term Empty) : (BoundedFormulaω.subst φ.openBounds fun (x : Fin 1) => t) ∈ S

Direct universal instantiation: if ∀x.φ ∈ S*, then φ(t) ∈ S* for all closed terms t. Uses openBounds to convert the bound variable to a free variable for substitution.

theorem FirstOrder.Language.ConsistencyPropertyEq.MaximalConsistent.neg_all_bound_mem {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} (hmax : C.MaximalConsistent S) {φ : L.BoundedFormulaω Empty 1} (h : φ.all.not ∈ S) : ∃ (t : L.Term Empty), (BoundedFormulaω.subst φ.openBounds fun (x : Fin 1) => t).not ∈ S

Direct negated universal: if ¬(∀x.φ) ∈ S*, then ∃t, ¬φ(t) ∈ S*.

Term Model Construction

The term model for the Henkin construction is built from closed terms of language L. Two terms are equivalent if the maximal consistent set contains the equation t₁ = t₂. The quotient model satisfies all sentences in S.

def FirstOrder.Language.termEquiv {L : Language} (C : L.ConsistencyPropertyEq) (S : Set L.Sentenceω) (_hmax : C.MaximalConsistent S) : L.Term Empty → L.Term Empty → Prop

Equivalence relation on closed terms induced by a maximal consistent set.

Equations

• FirstOrder.Language.termEquiv C S _hmax t₁ t₂ = (FirstOrder.Language.BoundedFormulaω.equal (FirstOrder.Language.Term.relabel Sum.inl t₁) (FirstOrder.Language.Term.relabel Sum.inl t₂) ∈ S)

theorem FirstOrder.Language.termEquiv_equivalence {L : Language} (C : L.ConsistencyPropertyEq) (S : Set L.Sentenceω) (hmax : C.MaximalConsistent S) : Equivalence (termEquiv C S hmax)

The term equivalence is an equivalence relation.

Term Setoid and Quotient

def FirstOrder.Language.termSetoid {L : Language} (C : L.ConsistencyPropertyEq) (S : Set L.Sentenceω) (hmax : C.MaximalConsistent S) : Setoid (L.Term Empty)

The Setoid on closed terms induced by the equivalence relation from S*.

Equations

• FirstOrder.Language.termSetoid C S hmax = { r := FirstOrder.Language.termEquiv C S hmax, iseqv := ⋯ }

def FirstOrder.Language.TermModel {L : Language} (C : L.ConsistencyPropertyEq) (S : Set L.Sentenceω) (hmax : C.MaximalConsistent S) : Type u

The carrier of the term model: closed terms quotiented by the equivalence relation t₁ ~ t₂ ↔ (t₁ = t₂) ∈ S*.

Equations

• FirstOrder.Language.TermModel C S hmax = Quotient (FirstOrder.Language.termSetoid C S hmax)

instance FirstOrder.Language.instCountableTermModelOfSigmaNatFunctions {L : Language} (C : L.ConsistencyPropertyEq) (S : Set L.Sentenceω) (hmax : C.MaximalConsistent S) [Countable ((l : ℕ) × L.Functions l)] : Countable (TermModel C S hmax)

Language Structure on the Term Model

The structure interprets function symbols by applying them to representative terms, and relation symbols by checking membership in the maximal consistent set S*.

def FirstOrder.Language.TermModel.mk {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} {hmax : C.MaximalConsistent S} (t : L.Term Empty) : TermModel C S hmax

Embed a closed term into the term model as its equivalence class.

Equations

• FirstOrder.Language.TermModel.mk t = ⟦t⟧

noncomputable instance FirstOrder.Language.termModelStructure {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} {hmax : C.MaximalConsistent S} : L.Structure (TermModel C S hmax)

The language structure on the term model.

Function interpretation: funMap f [⟦t₁⟧,...,⟦tₙ⟧] = ⟦f(t₁,...,tₙ)⟧. Relation interpretation: RelMap R [⟦t₁⟧,...,⟦tₙ⟧] ↔ rel R [t₁,...,tₙ] ∈ S*.

Equations

• One or more equations did not get rendered due to their size.

Truth Lemma Infrastructure

theorem FirstOrder.Language.term_realize_eq_mk {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} {hmax : C.MaximalConsistent S} (t : L.Term Empty) : Term.realize Empty.elim t = TermModel.mk t

In the term model, evaluating a closed term gives its equivalence class.

theorem FirstOrder.Language.TermModel.exists_rep {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} {hmax : C.MaximalConsistent S} (x : TermModel C S hmax) : ∃ (t : L.Term Empty), mk t = x

Every element of the term model is the equivalence class of some term.

Term Conversion for Empty Variable Types

Since Empty ⊕ Fin 0 has no inhabitants, terms of type Term (Empty ⊕ Fin 0) are ground terms (built from function symbols only). We provide a conversion to Term Empty and show it preserves semantics and set membership.

Opening Bound Variables

BoundedFormulaω.openBounds is defined in Operations.lean and converts bound variables to free variables. The truth lemma uses the semantic roundtrip (realize_openBounds) rather than the syntactic roundtrip.

Semantic Roundtrip for openBounds

theorem FirstOrder.Language.realize_openBounds {L : Language} {M : Type u_1} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaω Empty n) (xs : Fin n → M) : φ.openBounds.Realize xs ↔ φ.Realize Empty.elim xs

Semantic roundtrip: openBounds preserves semantics. For φ : BoundedFormulaω Empty n, evaluating openBounds φ with free variable assignment xs : Fin n → M is equivalent to evaluating φ with bound variable assignment xs.

Ordinal-valued depth for termination of truthLemma

The standard sizeOf measure is inadequate for truthLemma because:

• sizeOf (fun k => φs k) = 1 for function types, so sizeOf (iSup φs) = 2, yet sizeOf (φs k) can be arbitrarily large.
• The all case recurses on (φ.openBounds).subst t, which is not a structural subterm.

We define an Ordinal-valued depth that uses iSup for iSup/iInf cases, then prove it is preserved by castLE, relabel, openBounds, and subst.

noncomputable def FirstOrder.Language.BoundedFormulaω.depth {L : Language} {α : Type u_1} {n : ℕ} : L.BoundedFormulaω α n → Ordinal.{0}

Ordinal-valued depth of a bounded formula. Uses Ordinal.iSup at iSup/iInf nodes to ensure each component φs k has strictly smaller depth.

Equations

• FirstOrder.Language.BoundedFormulaω.falsum.depth = 0
• (FirstOrder.Language.BoundedFormulaω.equal t₁ t₂).depth = 0
• (FirstOrder.Language.BoundedFormulaω.rel R ts).depth = 0
• (φ.imp ψ).depth = max φ.depth ψ.depth + 1
• φ.all.depth = φ.depth + 1
• (FirstOrder.Language.BoundedFormulaω.iSup φs).depth = (⨆ (k : ℕ), (φs k).depth) + 1
• (FirstOrder.Language.BoundedFormulaω.iInf φs).depth = (⨆ (k : ℕ), (φs k).depth) + 1

Truth Lemma

@[irreducible]

noncomputable def FirstOrder.Language.truthLemma {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} {hmax : C.MaximalConsistent S} (σ : L.Sentenceω) : σ ∈ S ↔ σ.Realize (TermModel C S hmax)

Truth Lemma: A sentence belongs to the maximal consistent set S* if and only if it is true in the term model.

This is proved by recursion on the sentence, with the biconditional proved simultaneously at each step. The forward direction uses the consistency property axioms to decompose formulas. The backward direction uses maximality (decidability) and the dual axioms (C1', C3', C4') to derive contradictions.

Cases:

• (C0) for falsum: falsum is never in S (C0) and never realized.
• (C1, C1') for imp: forward uses C1 + IH; backward uses decidability + C1' + IH.
• (C3, C3') for iInf: forward uses C3 + IH; backward uses decidability + C3' + IH.
• (C4, C4') for iSup: forward uses C4 + IH; backward uses decidability + C4' + IH.
• (C5, C6) for equal: uses term model quotient structure.
• Term model structure for rel: uses definition of RelMap on term model.
• (C7, C7_all) for all: uses openBounds roundtrip.

Equations

• ⋯ = ⋯

Model Existence from Truth Lemma

theorem FirstOrder.Language.termModel_models_maximal {L : Language} {C : L.ConsistencyPropertyEq} {S : Set L.Sentenceω} {hmax : C.MaximalConsistent S} : Theoryω.Model S (TermModel C S hmax)

The term model satisfies every sentence in S*.