The forward truth lemma for the quotient term model (issue #8, commit 5b)

From a Henkin-complete set S over the relational core L[[ℕ]], QuotientTermModel.lean (commit 5a) built the closed-term quotient model QModel hsc and its atomic semantics. This file lifts that to the full forward, polarity-sensitive truth lemma and packages a consumer-shaped model-existence theorem.

Discipline

The truth lemma is not a biconditional M ⊨ φ ↔ φ ∈ S. It is two separate forward implications — one per polarity — proven together by a single simultaneous recursion:

• truth_pos : σ ∈ S → M ⊨ σ (positive polarity)
• truth_neg : σ.not ∈ S → ¬ M ⊨ σ (negative polarity)

No excluded middle / by_cases on membership _ ∈ S, and no maximality/decisiveness of S, is used anywhere. Every step is driven by a constructive HenkinComplete field:

• connectives — imp / neg_imp / iInf / neg_iInf / iSup / neg_iSup;
• quantifiers — all_inst (positive) and neg_all_witness (negative) only;
• atomics — the commit-5a quotient API (qmk_eq_of_mem / qmk_ne_of_neg_mem / relMap_of_mem / not_relMap_of_neg_mem), with the Empty ⊕ Fin 0 sentence-term bridge below;
• contradictions — no_falsum / no_contradiction (C0).

The all case (depth-measure recursion)

The quantifier cases are handled by well-founded recursion on an ordinal depth measure, mirroring the shape of the legacy Methods/Henkin/Construction.lean truth lemma: from (all body) ∈ S the all_inst field yields, for every constant c, the sentence instConst c body = (body.openBounds).subst (fun _ => constTerm c), whose depth is strictly smaller than that of all body; recursion on that sentence plus realize_instConst_qmodel and surjectivity of qmk discharges the universal (dually for the negated universal via neg_all_witness).

The Empty ⊕ Fin 0 sentence-term bridge

Sentence atomics equal t u / rel R ts carry terms in L[[ℕ]].Term (Empty ⊕ Fin 0). Since both Empty and Fin 0 are uninhabited, every such term is ground; we collapse it to L[[ℕ]].Term Empty (a re-statement of the private helpers in Methods/Henkin/Construction.lean).

def FirstOrder.Language.Term.toGround {L : Language} : (L.withConstants ℕ).Term (Empty ⊕ Fin 0) → (L.withConstants ℕ).Term Empty

Collapse a sentence-atomic term (variables in the uninhabited Empty ⊕ Fin 0) to a closed Term Empty.

Equations

• (FirstOrder.Language.var (Sum.inl e)).toGround = e.elim
• (FirstOrder.Language.var (Sum.inr i)).toGround = i.elim0
• (FirstOrder.Language.func f ts).toGround = FirstOrder.Language.func f fun (i : Fin l) => (ts i).toGround

theorem FirstOrder.Language.Term.toGround_relabel_inl {L : Language} (t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)) : relabel Sum.inl t.toGround = t

Relabeling a toGround-collapsed term back to Empty ⊕ Fin 0 recovers the original.

theorem FirstOrder.Language.Term.realize_toGround {L : Language} {M : Type u_1} [(L.withConstants ℕ).Structure M] (t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)) (v : Empty ⊕ Fin 0 → M) : realize v t = realize Empty.elim t.toGround

Evaluating a sentence-atomic term with any assignment equals evaluating its toGround collapse with Empty.elim (both variable types are uninhabited).

closeBy and its realization (validated commit-5b foundation)

theorem FirstOrder.Language.realize_closeBy {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} {n : ℕ} (hsc : HenkinComplete U S) (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) : (closeBy φ τ).Realize (QModel hsc) ↔ φ.Realize Empty.elim fun (i : Fin n) => qmk hsc (constTerm (τ i))

Realizing closeBy φ τ in QModel hsc is realizing φ at the classes of the constants τ.

theorem FirstOrder.Language.realize_instConst_qmodel {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (body : (L.withConstants ℕ).BoundedFormulaω Empty 1) (c : ℕ) : (instConst c body).Realize (QModel hsc) ↔ body.Realize Empty.elim fun (x : Fin 1) => qmk hsc (constTerm c)

The constant instance instConst c body realizes in QModel hsc exactly as body at the class of c in its single variable. This is the semantic bridge the all case consumes; it needs no syntactic substitution-composition identity.

Surjectivity of the quotient map

theorem FirstOrder.Language.qmk_surjective {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (x : QModel hsc) : ∃ (c : ℕ), x = qmk hsc (constTerm c)

Every element of the quotient term model is the class of some constant.

Ordinal depth: strict decrease for the constant instance

The generic preservation/strict-decrease calculus for BoundedFormulaω.depth now lives in the neutral Lomega1omega/Depth.lean (shared with Methods/Henkin/Construction.lean); only the instConst combination is derived here.

Two small realization bookkeeping facts

theorem FirstOrder.Language.constTermS_qtConst_toGround {L : Language} [L.IsRelational] (t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)) : constTermS (qtConst t.toGround) = t

A ground sentence-atomic term is the standard constant term of its collapsed constant.

The simultaneous forward truth lemma

truth_both hsc σ bundles the two polarities. It is a single well-founded recursion on σ.depth: connectives recurse on structural subformulas (strictly smaller depth), and the all case recurses on instConst c body (a sentence of strictly smaller depth).

theorem FirstOrder.Language.truth_both {L : Language} {U S : Set (L.withConstants ℕ).Sentenceω} [L.IsRelational] (hsc : HenkinComplete U S) (σ : (L.withConstants ℕ).Sentenceω) : (σ ∈ S → σ.Realize (QModel hsc)) ∧ (BoundedFormulaω.not σ ∈ S → ¬σ.Realize (QModel hsc))

The forward, polarity-sensitive truth lemma (bundled). For every sentence σ, membership in S forces truth in QModel hsc (positive), and membership of σ.not forces falsity (negative). Proven by one simultaneous well-founded recursion on the ordinal depth of σ.

theorem FirstOrder.Language.truth_pos {L : Language} {U S : Set (L.withConstants ℕ).Sentenceω} [L.IsRelational] (hsc : HenkinComplete U S) {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) (hmem : closeBy φ τ ∈ S) : φ.Realize Empty.elim fun (i : Fin n) => qmk hsc (constTerm (τ i))

Forward truth lemma, positive polarity (open form). If the constant closure closeBy φ τ belongs to S, then φ is realized in QModel hsc at the classes of the constants τ. A thin realize_closeBy wrapper over the sentence-level engine truth_both.

theorem FirstOrder.Language.truth_neg {L : Language} {U S : Set (L.withConstants ℕ).Sentenceω} [L.IsRelational] (hsc : HenkinComplete U S) {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) (hmem : BoundedFormulaω.not (closeBy φ τ) ∈ S) : ¬φ.Realize Empty.elim fun (i : Fin n) => qmk hsc (constTerm (τ i))

Forward truth lemma, negative polarity (open form). If the negation of the constant closure closeBy φ τ belongs to S, then φ is not realized in QModel hsc at the classes of the constants τ.

The consumer model-existence theorem

theorem FirstOrder.Language.exists_model_of_henkinComplete {L : Language} {U S : Set (L.withConstants ℕ).Sentenceω} [L.IsRelational] (hsc : HenkinComplete U S) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M), (∀ φ ∈ S, φ.Realize M) ∧ ∀ (φ : (L.withConstants ℕ).Sentenceω), BoundedFormulaω.not φ ∈ S → ¬φ.Realize M

Model existence from a Henkin-complete set. The quotient term model is a nonempty L[[ℕ]]-structure realizing every member of S and falsifying every sentence whose negation is in S. Both polarities are exposed for members of S.