Documentation

InfinitaryLogic.Methods.WellOrdering.ModelExtraction

Model extraction from the completed well-ordering set (issue #12, step 5) #

The completion endpoint hands step 5 a Henkin-complete S containing the base diagram Bφ = {φ̂} ∪ {d_q < d_r : q < r} opaquely; the quotient term model of the forward truth lemma then realizes every member of S, hence every member of Bφ.

This file is the relational/countable extraction: [L.IsRelational] is consumed by the quotient term model (the relational-core collapse of closed terms to constants), and [Countable (Σ l, L.Relations l)] by the fair enumeration. Removing both restrictions is the later transport step, not done here.

source
theorem FirstOrder.Language.exists_model_baseDiagram {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (h : HasWellOrderedChains φ lt) :
∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M), ∀ χ ∈ baseDiagram φ lt, χ.Realize M

Model extraction (relational/countable form): under the well-ordered-chains hypothesis, some nonempty L[[ℕ]]-structure realizes every member of the base diagram — the lifted root and the full positive rational diagram. Composition of the completion endpoint with the forward-truth-lemma model existence theorem; the Henkin-complete set is consumed opaquely.

The rational map through the interpreted constants #

source
def FirstOrder.Language.ratConstMap {L : Language} (M : Type) [(L.withConstants ℕ).Structure M] (q : ℚ) :
M

The rational map of an L[[ℕ]]-structure: q ↦ d_q^M, the interpretation of the rational constant. Step 5's f : ℚ → M.

Equations
Instances For
    source
    theorem FirstOrder.Language.realize_constTermS_eq_constTerm {L : Language} {M : Type} [(L.withConstants ℕ).Structure M] (c : ℕ) (v : Empty ⊕ Fin 0 → M) :
    Term.realize v (constTermS c) = Term.realize Empty.elim (constTerm c)

    The sentence-context constant term realizes to the interpretation of the closed constant, under any (vacuous) assignment.

    source
    theorem FirstOrder.Language.realize_ratLtAtom {L : Language} (lt : L.Relations 2) {M : Type} [inst : (L.withConstants ℕ).Structure M] (q r : ℚ) :
    (ratLtAtom lt q r).Realize M ↔ Structure.RelMap (Sum.inl lt) ![ratConstMap M q, ratConstMap M r]

    A positive diagram atom realizes as the expansion relation at the mapped rationals.

    The step-5 endpoint (relational/countable form) #

    source
    theorem FirstOrder.Language.exists_model_relPreserving_relational {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (h : HasWellOrderedChains φ lt) :
    ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M) (f : ℚ → M), φ.Realize M ∧ RelPreserving lt f

    Step 5 endpoint, relational/countable form (Marker, Theorem 4.26 at a relational language with countable relational core): under the well-ordered-chains hypothesis, some nonempty model of φ carries a relation-preserving map f : ℚ → M — the rational map of the extracted expansion, through its reduct L-structure. The raw positive conclusion (D2): no injectivity, no order-embedding packaging; those are derived corollaries tracked for subsequent commits, and the arbitrary-language form is the later transport step.