The quotient term model and its atomic semantics (issue #8, commit 5a)

From a Henkin-complete set S (the output of commit 4b's exists_henkinComplete_of_root) over the relational core L[[ℕ]], this file builds the closed-term quotient model and establishes its atomic semantics — everything the forward truth lemma (commit 5b) needs below formula induction.

Over a relational base every closed L[[ℕ]]-term collapses to a constant (exists_eq_constTerm), so the equality relation on closed terms is the constant equality constEq · · ∈ S, and the HenkinComplete atomic fields (eq_refl/eq_symm/eq_trans, rel_congr) supply exactly the constant-specialized equality and congruence laws.

Acceptance lemmas

• qRel_equiv: the equality-membership relation on closed terms is an equivalence.
• qmk_eq_iff / qmk_constTerm_eq_iff: mk t = mk u iff the collapsed constants are S-equal.
• relInst_congr / relInst_congr_iff: relation membership is invariant, coordinatewise, under S-equal arguments — the iterated tuple congruence, with the iff via equality symmetry.
• qModelStructure: the L[[ℕ]]-structure; RelMap on quotient tuples is well-defined by construction.
• qterm_realize_eq_mk: a closed term evaluates to its own quotient class.
• Positive/negative atomic realization: qmk_eq_of_mem / qmk_ne_of_neg_mem (equality) and relMap_of_mem / not_relMap_of_neg_mem (relations). The negative lemmas reflect through the representatives chosen by the quotient relation map (relMap_qmk_iff) and close with C0 (no_contradiction) — not by any decisiveness or maximality of S.

These atomic biconditionals are legitimate — they follow from the quotient definition, atomic congruence, and C0 alone. There is no M ⊨ φ ↔ φ ∈ S for arbitrary φ.

The relational collapse of closed terms

noncomputable def FirstOrder.Language.qtConst {L : Language} [L.IsRelational] (t : (L.withConstants ℕ).Term Empty) : ℕ

The constant a closed term collapses to over the relational core.

Equations

• FirstOrder.Language.qtConst t = ⋯.choose

theorem FirstOrder.Language.eq_constTerm_qtConst {L : Language} [L.IsRelational] (t : (L.withConstants ℕ).Term Empty) : t = constTerm (qtConst t)

theorem FirstOrder.Language.constTerm_injective {L : Language} {a b : ℕ} (h : constTerm a = constTerm b) : a = b

theorem FirstOrder.Language.qtConst_constTerm {L : Language} [L.IsRelational] (c : ℕ) : qtConst (constTerm c) = c

The quotient carrier

def FirstOrder.Language.qRel {L : Language} [L.IsRelational] {S : Set (L.withConstants ℕ).Sentenceω} (t u : (L.withConstants ℕ).Term Empty) : Prop

The equality relation on closed terms: their collapsed constants are S-equal.

Equations

• FirstOrder.Language.qRel t u = (FirstOrder.Language.constEq (FirstOrder.Language.qtConst t) (FirstOrder.Language.qtConst u) ∈ S)

theorem FirstOrder.Language.qRel_equiv {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) : Equivalence qRel

The equality relation is an equivalence (from the atomic equality fields of S).

def FirstOrder.Language.qSetoid {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) : Setoid ((L.withConstants ℕ).Term Empty)

The setoid on closed terms.

Equations

• FirstOrder.Language.qSetoid hsc = { r := FirstOrder.Language.qRel, iseqv := ⋯ }

def FirstOrder.Language.QModel {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) : Type

The quotient term model.

Equations

• FirstOrder.Language.QModel hsc = Quotient (FirstOrder.Language.qSetoid hsc)

def FirstOrder.Language.qmk {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (t : (L.withConstants ℕ).Term Empty) : QModel hsc

The class of a closed term.

Equations

• FirstOrder.Language.qmk hsc t = ⟦t⟧

theorem FirstOrder.Language.qmk_eq_iff {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (t u : (L.withConstants ℕ).Term Empty) : qmk hsc t = qmk hsc u ↔ constEq (qtConst t) (qtConst u) ∈ S

theorem FirstOrder.Language.qmk_constTerm_eq_iff {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (a b : ℕ) : qmk hsc (constTerm a) = qmk hsc (constTerm b) ↔ constEq a b ∈ S

Iterated tuple congruence for relation instances

theorem FirstOrder.Language.relInst_congr {L : Language} {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) {l : ℕ} (R : L.Relations l) (g g' : Fin l → ℕ) (h : ∀ (i : Fin l), constEq (g i) (g' i) ∈ S) (hg : relInst R g ∈ S) : relInst R g' ∈ S

Coordinatewise relation congruence: S-equal argument tuples give the same relation membership. Iterates the atomic one-coordinate congruence HenkinComplete.rel_congr.

theorem FirstOrder.Language.relInst_congr_iff {L : Language} {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) {l : ℕ} (R : L.Relations l) (g g' : Fin l → ℕ) (h : ∀ (i : Fin l), constEq (g i) (g' i) ∈ S) : relInst R g ∈ S ↔ relInst R g' ∈ S

The tuple congruence as an iff (using equality symmetry for the reverse).

The L[[ℕ]]-structure on the quotient

instance FirstOrder.Language.qfuncSuccIsEmpty {L : Language} [L.IsRelational] (n : ℕ) : IsEmpty ((L.withConstants ℕ).Functions (n + 1))

@[implicit_reducible]

noncomputable instance FirstOrder.Language.qModelStructure {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) : (L.withConstants ℕ).Structure (QModel hsc)

The quotient term model as an L[[ℕ]]-structure. Function interpretation is the constant embedding (higher arities are empty over the relational core); RelMap on a quotient tuple holds iff some constant representatives make the atomic relation instance a member of S.

Equations

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

theorem FirstOrder.Language.qterm_realize_eq_mk {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (t : (L.withConstants ℕ).Term Empty) : Term.realize Empty.elim t = qmk hsc t

Closed-term evaluation is its quotient class.

Positive and negative atomic realization

theorem FirstOrder.Language.relMap_qmk_iff {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : (Structure.RelMap (Sum.inl R) fun (i : Fin l) => qmk hsc (constTerm (g i))) ↔ relInst R g ∈ S

RelMap of a constant tuple reflects to atomic membership. Forward reflects through the representatives chosen by the relation map (via the tuple congruence); backward is the identity representative.

theorem FirstOrder.Language.qmk_eq_of_mem {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (a b : ℕ) (hmem : constEq a b ∈ S) : qmk hsc (constTerm a) = qmk hsc (constTerm b)

Positive atomic (equality).

theorem FirstOrder.Language.qmk_ne_of_neg_mem {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) (a b : ℕ) (hmem : BoundedFormulaω.not (constEq a b) ∈ S) : qmk hsc (constTerm a) ≠ qmk hsc (constTerm b)

Negative atomic (equality). Closes with C0 — not maximality.

theorem FirstOrder.Language.relMap_of_mem {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) (hmem : relInst R g ∈ S) : Structure.RelMap (Sum.inl R) fun (i : Fin l) => qmk hsc (constTerm (g i))

Positive atomic (relation).

theorem FirstOrder.Language.not_relMap_of_neg_mem {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} (hsc : HenkinComplete U S) {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) (hmem : BoundedFormulaω.not (relInst R g) ∈ S) : ¬Structure.RelMap (Sum.inl R) fun (i : Fin l) => qmk hsc (constTerm (g i))

Negative atomic (relation). Reflects through the relation map's chosen representatives, then closes with C0 — not maximality.