The Semantics stratum is the largest in the derivation — 125 acts. It transforms the judgemental machinery earned in strata 1–5 into a full relational logic: entailment, combining (Together), choosing (Either), conditional relating (Implies), denial (Negate), morphisms, and the typing interpretations that make coherent distinguishing possible. Mathematicians recognize this structure as a complete Heyting algebra, but it is earned here from the requirements of consistent distinction. The stratum also earns the standard metatheoretic results (preservation, progress, soundness, confluence, normalization) that validate the syntactic theory.
Of the 125 acts, the strata source files document 44 in detail. The analysis below covers these 44. The remaining 81 acts are constructive intermediate steps whose full catalog has not yet been compiled.
What Semantics exports
Of the 44 documented acts, 13 are exports, 12 are intermediates, and 19 are dead ends. The dead-end ratio is extreme: 43% of documented acts are dead ends. This is qualitatively different from other strata and reveals a structural split.
Relational logic exports (the construction)
| Export | External uses | What it provides |
|---|---|---|
| StructureSemantics | 7 | The structured logical organization — feeds Geometry, Profile, Composite |
| Together | 4 | Shared refinement — feeds Geometry and Profile |
| Either | 3 | Combined scope — feeds Geometry and Profile |
| Implies | 3 | Conditional relating — feeds flow-index and Profile |
| Morph | 3 | Morphisms between recognitions — feeds transport and Profile |
| Include | 2 | Mediation — feeds residuation and closure distribution |
| Negate | 2 | Denial — feeds interior dualization and Profile |
| JudgeTyping | 2 | Typing judgements — feeds Profile syntax calculations |
| SubstituteReducibility | 2 | The substitution lemma — feeds reindexing and Term |
| Entails | 1 | Subsumption ordering — feeds Profile invariant order |
| Identity | 1 | Trivial mediation — feeds fixed identity in Profile |
| Compose | 1 | Morphism composition — feeds fixed composition in Profile |
| Equal | 1 | Term equalization — feeds Profile finite limits |
The heaviest export is StructureSemantics (7 external children). It is composed as (CalculateSemantics, Reflex) — the Semantics calculation witnessed by Reflex (the minimal Foundation witness). This act carries the full logical structure forward: Geometry, Profile, and composite profiles all depend on it. Where other strata export specific operations, Semantics exports organization itself.
Metatheoretic dead ends (the validation)
19 of the 44 documented acts are dead ends — acts that nothing else references. But unlike dead ends in other strata (which are typically exploratory or inert), these dead ends are purposeful. They are the standard theorems of the syntactic theory:
Soundness and completeness:
- SoundSyntax — The syntactic theory is sound with respect to the structured semantics
- CanonicalSemantics — The canonical model exists
- CompleteSyntax — The syntactic theory is complete
- ModelSemantics — The semantic model is well-formed
Type safety:
- PreserveTyping — Typing is preserved under reduction (subject reduction)
- ProgressTyping — Well-typed terms that are not values can take a step (progress)
Computation properties:
- NormalizeSyntax — Terms normalize
- EnsureConfluence — Reduction is confluent (Church-Rosser)
- SummarizeReduction — Reduction summarizes
Reducibility method:
- EstablishFundamentalReducibility — The fundamental lemma of the reducibility argument
Algebraic properties:
- RecognizeFixedPoint — Fixed points are recognized
- SubsetSemantics — Subset semantics is well-structured
- ExcludeRecognition — Exclusion within the algebra
- CapRecognition — The top element
Collection acts:
- CollectTypes, CollectContexts, CollectTerms — Catalogs of types, contexts, and terms
- CalculateSyntax, ReflexSyntax — Syntactic calculations
These dead ends are the conclusions of the semantic argument. PreserveTyping, ProgressTyping, SoundSyntax, EnsureConfluence, and NormalizeSyntax are exactly the five theorems you would prove in a standard type theory textbook. The derivation earns them constructively, but they do not feed into further construction because they are endpoints — they verify that the algebra works correctly, and nothing further needs to be built from that verification.
This architectural split — export vs. validation — is unique to Semantics. Other strata (Foundation, Trace, Term, Observation, Judgement) have occasional dead ends (2-5 each), but no stratum has 19. The Semantics stratum is doing two different kinds of work: building algebraic structure (13 exports) and verifying that structure (19 dead ends). The verification is essential to the derivation’s integrity but structurally inert — it proves the construction is correct without adding new constructive material.
How the exports are earned
The relational logic core (10 acts → 7 exports)
The logical structure is built from Foundation and Trace exports through a chain of compositions. Each act earns one of the operations that consistent distinguishing demands.
Entails (RecognizeContext, Recognition) — One recognition subsumes another when context membership guarantees the first whenever it guarantees the second. Export (1 external). This is the ordering that organizes the logic.
Bottom (Recognition, Nothing) — The empty recognition, the one that witnesses Nothing. Intermediate.
Top (Recognition, CompleteTrace) — The universal recognition that witnesses every complete trace. Dead end — Top is defined but not used as a component.
Together (Entails, Entry) — Given two recognitions, their shared refinement — what is recognized under both. Export (4 external).
Either (Entails, ContextualizeTrace) — The combined scope — what is recognized under at least one. Export (3 external).
Include (Entails, Together) — When combining with one recognition leaves the other unchanged. Export (2 external).
Excludes (Together, Bottom) — Combining with the empty recognition gives the empty recognition. Dead end — a valid property but not needed as a component.
Implies (Either, FormFunctionTerm) — The largest recognition whose combination with A is subsumed by B. Export (3 external). The function type from Term provides the internal structure; the combined scope provides the completeness. This is where the relational logic becomes constructive — conditional relating exists but not every question has a determinate answer.
Negate (Implies, Bottom) — The largest recognition that combines with A to give nothing. Export (2 external). Denial in the relational logic is not classical — double denial does not return to the original. This reflects the relational stance that some matters are genuinely indeterminate.
Shape (Implies, Entails) — The form of the conditional-relating/entailment interaction. Intermediate — feeds RecognizeFixedPoint.
Morphisms and structure (5 acts → 4 exports)
Morph (Implies, Either) — Morphisms between recognitions: structure-preserving maps. Export (3 external). Morphisms say how one recognition transforms into another while preserving logical structure.
Identity (Morph, Reflex) — A recognition mapping to itself, the trivial mediation. Export (1 external).
Compose (Morph, Morph) — Chaining structure-preserving maps. Export (1 external).
StructureSemantics (CalculateSemantics, Reflex) — The structured relational logic as a whole. Export (7 external). This act packages the entire construction — entailment, combining, choosing, conditional relating, denial, morphisms — into a single structured object that later strata can reference.
SubsetSemantics (StructureSemantics, Include) — The subset structure within the logic. Dead end.
Typing and syntax (8 acts → 2 exports)
ConstructTypes, ConstructContexts, ConstructTerms — Building the syntactic categories from algebraic operations. All intermediate.
JudgeTyping (TypeSeed, TypeApplication) — Typing judgements formalized within the algebra. Export (2 external). This bridges the Term stratum’s typing seeds with the algebraic structure.
Equal (RecognizeObservation, JudgeTyping) — When two terms are typably equal as witnessed by observation. Export (1 external).
The reducibility argument (4 acts → 1 export)
NormalizeStrongly, SelectReducibilityCandidate, BuildReducibleEnvironment — The intermediate steps of Tait’s reducibility argument, which proves strong normalization. All intermediate.
SubstituteReducibility (BuildReducibleEnvironment, JudgeTyping) — The substitution lemma of the reducibility argument: substituting reducible terms into reducible environments preserves reducibility. Export (2 external: Reindexing, SubstitutionTerm). This is the key technical lemma — and notably, it is used as a component by SubstitutionTerm in the Term stratum, creating the cross-stratum dependency noted there.
Provability and entailment (4 acts → 0 exports)
OrderProvability, RecognizeSyntax, EntailSemantics — The provability ordering, syntactic recognition, and semantic entailment. All intermediate.
CompleteSyntax — Completeness of the syntactic theory with respect to entailment. Dead end — the conclusion of the argument.
The 81 undocumented acts
The strata source files document 44 of the Semantics stratum’s 125 acts. The remaining 81 are constructive steps whose full catalog has not yet been assembled from the act files. Based on the export analysis, many of these 81 acts are likely intermediate construction within the algebraic development — the internal steps needed to compose the exports from Foundation, Trace, Term, Observation, and Judgement inputs. The 44 documented acts already account for all 13 known exports and all 19 known dead ends, suggesting the 81 undocumented acts are predominantly intermediate.
What the Semantics stratum earns
The relational logic. Entailment, combining, choosing, conditional relating, denial — the logical structure that makes coherent distinguishing possible. This is the formal content of Movement I: what begins as the act of distinction ends as a complete constructive logic. Mathematicians recognize this as a Heyting algebra.
Morphisms. Structure-preserving maps between recognitions, their identity, and their composition. These are the arrows that let the logic describe transformation as well as structure.
The metatheory. Soundness, completeness, preservation, progress, confluence, normalization, and the fundamental lemma of reducibility. These are not ingredients for further construction but guarantees that the construction works. The 19 dead ends are the derivation’s quality certificate.
The export/validation split. Semantics is the stratum where the derivation bifurcates into constructive work (building structure for later strata) and reflexive work (verifying that structure). This bifurcation is itself a finding about the relational architecture: at a certain level of complexity, the system must begin checking its own consistency, and that checking produces no new constructive material.
Connection to the derivation
The Semantics stratum completes the derivation’s second phase and provides the logical content of Movement I. The relational logic earned here is the formal realization of the claim that consistent distinguishing requires a complete constructive logic — where not every question has a determinate answer. Mathematicians recognize this structure as a Heyting algebra.
The Stability stratum freezes this logical structure, and Geometry couples the resulting invariants with flow and closure. The Semantics exports provide the vocabulary; the metatheoretic dead ends provide the assurance that the vocabulary is well-formed.