Layer 7b, checkpoint 5b-3: the restricted schema truth lemma #
The truth lemma for the schema term model (SchemaTermCarrier/schemaTermStructure): realization
of a staged-family formula in the quotient, on the classes of closed terms, is equivalent to
membership of its schemaFormulaSentence in the completed theory Tσ. Restricted — the induction
runs over the staged family Γlocal s₀ (k+1) (the LocalEMContext.truthLemmaStage organization),
never over arbitrary formulas.
This file opens with the all-case input: locSkWitness_universal_constInterp_nat, the
σ-generalization of locSkWitness_universal from the deep interpretations locDeepInterp to an
arbitrary constant interpretation σ : ℕ → M (the shape a Marker certificate body supplies). The
proof is the same contrapositive Hilbert-choice argument — localSkolem_funMap_spec needs no
tuple-shape hypothesis, so nothing about σ is used beyond interpreting the argument terms.
The all-case Skolem input #
Arbitrary-constant local Skolem-witness universality: under any constant interpretation
σ : ℕ → M of the sequence constants, if the body ψ of a staged universal ∀ψ ∈ Γlocal s₀ k
holds at the σ-value of its Skolem-witness term, it holds at every M-element. Generalizes
locSkWitness_universal from the deep tuples locDeepInterp to the interpretations a Marker
certificate body supplies.
The truth-lemma helper layer #
Three small bridges the induction consumes at every case: the sign flip on universe members (negation membership ↔ non-membership), the carrier term bridge (open terms realized at classes are classes of closed substitution instances), and the substitution/valuation exchange for closed instances in an arbitrary structure.
Sign flip on the universe. For a universe member, the completed theory contains its
negation iff it does not contain the sentence itself (forward: a two-element fragment of Tσ
would be a consistent set containing a sentence and its negation; backward: completeness).
The carrier term bridge: an open (localColim s₀)[[ℕ]]-term realized in the schema term
model at class-valued variables is the class of its closed substitution instance.
Substitution/valuation exchange: a closed substitution instance realizes (in any structure) to the open term realized at the values of the substituted terms.
The staged restricted truth lemma #
The staged restricted schema truth lemma. For a successor-stage family formula
ψ ∈ Γlocal s₀ (k + 1) and closed argument terms ts, realizing the colimit image of ψ in the
schema term model on the classes of ts is equivalent to membership of its
schemaFormulaSentence in the completed theory Tσ. The source M carries the CANONICAL
localColimStructure (the all case consumes the Hilbert-choice Skolem interpretations via
locSkWitness_universal_constInterp_nat). Modeled on LocalEMContext.truthLemmaStage: the
induction threads the family membership; atoms normalize to the 5a atomic API through the carrier
term bridge and semantic sign transport; imp is propositional completeness; iSup/iInf
consume the canonical-deForm connective witnesses (5b-2) — the negative iInf direction is
exactly what the completion repair pinned; all runs the Skolem-witness argument against a
certificate body. (The heartbeat bump is for the seven-case induction as a single elaboration
unit; no individual step is deep.)
Stage-agnostic lift corollary: the staged schema truth lemma for an original stage-k
family member, at any stage including the raw seed stage 0. Lifts the member one stage (along
LlocalHom, via liftGamma_mem_Γlocal_succ) where subformula closure is available, then rewrites
the colimit image back down with the cocone coherence mapLanguage_LlocalInclusion_lift.
The ΓEMlocal sequence-realization bridge, layer 1: closing terms along the sequence #
The exported bridge (below) is narrowly scoped to the distinguished sequence: realization of a
ΓEMlocal member on schemaSeq ∘ t in the base-language reduct of the term model, iff the
lifted template sentence is in Tσ. This layer supplies the term plumbing: closing an open
Fin m-variable base term along an increasing tuple of sequence constants, its value under a
certificate-body interpretation (σ (t i) at the variables), and its class in the term model
(the class of the closed instance). Plus the neutral restatement of the canonical-deForm
realization lemma (the residual file's copy is Conditional-facing and not imported here).
Realization of a canonical deForm in any structure: substituting the Fin p-variable terms
g for the bound variables and rebinding realizes as φ on the term values. Neutral twin of the
residual-file realize_canonDeForm.
Closing a term along the sequence: an open Fin m-variable base-language term, mapped
into the constant expansion and its variables substituted by the sequence constants d_{t i}.
Equations
- FirstOrder.Language.schemaCloseTerm u t = (((FirstOrder.Language.localColim s₀).lhomWithConstants ℕ).onTerm u).subst fun (i : Fin m) => FirstOrder.Language.henkinConst (t i)
Instances For
A sequence constant realizes to its interpretation.
The body value of a closed instance: under a certificate-body interpretation σ, the
closed instance realizes to the open term realized at the σ-values of the tuple.
The class of a closed instance: in the schema term model, the expansion image of an open
term realized on the sequence classes schemaSeq ∘ t is the class of its closed instance.
The reduct value of a closed instance: in the base-language reduct of the schema term model, an open term realized on the sequence classes is the class of its closed instance.
The three sign transports (semantic equivalence of universe sentences) #
Colimit-member transport: the formula sentence at the sequence constants and the lifted
template sentence at the tuple receive the same sign — under every body interpretation both say
"φ on σ ∘ t".
Equality-atom transport: the closed-instance equality sentence and the lifted canonical equality atom receive the same sign.
Relation-atom transport: the closed-instance relation sentence and the lifted canonical relation atom receive the same sign.
Canonical-deForm transport: the formula sentence of the base member at the closed
instances of g and the lifted template of the deForm receive the same sign.
The ΓEMlocal sequence-realization bridge #
The colimit-family truth lemma: the staged truth lemma at the colimit level, unpacking a
ΓlocalColim membership into its stage representation.
The ΓEMlocal sequence-realization bridge (the exported statement, narrowly scoped to the
distinguished sequence): a ΓEMlocal member realized on schemaSeq ∘ t in the base-language
reduct of the schema term model, iff its lifted template sentence at t is in the completed
theory. Four summands: colimit members through the staged truth lemma; canonical equality and
relation atoms through the 5a atomic API on closed instances; canonical deForms by closing the
substituted terms along t and reducing to the base member. Every case ends in the matching
sign transport.
Full indiscernibility and the Ω-witnesses #
Full indiscernibility of the schema sequence (cutoff 0): in the base-language reduct of
the schema term model, schemaSeq is Lω₁ω-indiscernible on all of ΓEMlocal — realization at
any two strictly monotone tuples transports through the bridge to theory membership at the two
lifted templates, which agree by tuple uniformity.
The tail-template truth collapse to the standard tuple: by full indiscernibility, the
eventually-form template truth of a ΓEMlocal member equals theory membership of its lifted
template at the standard tuple.
The schema-template Ω-witness property for the schema sequence — the Layer-7a target,
discharged by the completed theory: a disjunction's template truth yields a component's (the
positive iSup witness pinned by the completion), and joint component truth yields the
conjunction's (via the negative-iInf witness pinned by the completion repair: were the
conjunction negative, its fixed refuted conjunct would contradict that component's truth).
Checkpoint 5c substrate: validity positivity and pairwise distinctness #
The two term-model facts the Morley-seed agreement (morleySeed_template_agreement_cross)
consumes: a universe sentence valid under every body interpretation gets the positive sign (the
route to seed-sentence realization), and the schema sequence is pairwise distinct (a body for the
equality sentence, evaluated on a support enlarged to both indices, would violate the strictness
of its skeleton interpretation).
Validity forces the positive sign: a universe sentence realized under EVERY body interpretation pair cannot be decided negatively — the body of its singleton negation would refute itself.
The schema sequence is pairwise distinct: if two sequence classes were equal, the completed theory would contain their equality sentence; a certificate body for it, evaluated on a support enlarged to contain both indices, would equate two values of a strictly monotone skeleton interpretation.