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 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).
The three sign transports (semantic equivalence of universe sentences) #
The ΓEMlocal sequence-realization bridge #
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 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.