Logic enrichment and erased dependent cores

The frozen ${\mathsf{LTT}}_0$ has separate type, proposition-formation, and classical entailment judgments; small propositions are coded data, not proof terms. Comprehension and induction use small predicates, while ${\mathsf{LTT}}_0^{\ast }$ widens induction only to analytic predicates. The exact imported results relate ${\mathsf{LTT}}_0$ to ${\mathsf{ACA}}_0$ and ${\mathsf{LTT}}_0^{\ast }$ to $\mathsf{ACA}$ under the displayed translations. The reverse route imports Definitions 5.30–5.31, Theorems 5.32–5.33, Corollaries 5.33.1–5.33.3, and the starred transfer of Theorem 6.1; it is not exported as an effective proof translator.

No theorem is claimed for analytic comprehension, the unrestricted Weyl system, HOL, CIC, or Nuprl. Historical Plastic acceptance does not audit the checker or reprove conservativity. The Kappa artifact checks a finite syntactic classifier only.

Kopylov’s connective $x:A\cap B(x)$ contains one untyped subject validated by both PER views. Introduction requires equal beta-eta erasures; projections change annotation without changing the subject. The exact source result is semantic validation of the rules in a selected extensional Nuprl PER model with functional families.

No decidable typing or global Nuprl normalization theorem is claimed. Nor does the book claim annotation normalization merely from a strongly normalizing erased target. The same-subject connective is not a Sigma, refinement proof pair, System S self type, DOT self binder, or identity type.

System S is a Curry-style dependent assignment calculus with erased implicit products, $\iota x.T$, closed nonrecursive term definitions, and singly recursive closed type definitions whose non-erased recursive occurrences are positive. Substitution is local; confluence, preservation, and strong beta normalization are exact imports of Fu–Stump Lemma 1 and Theorems 4, 5, and 8, with Definitions 8–20 and Lemmas 3–7 supplying the erasure, reducibility, and compatibility machinery for this frozen closure.

Dropping positivity, adding arbitrary equi-recursive types, mutual open definitions, or transferring the rules to MLTT invalidates the displayed proof architecture. The Kappa corpus tests only polarity and same-subject tags.

A very-dependent function has range $B[f,x]$, interpreted by well-founded recursion over a strict relation on the domain. Each range may inspect only the restriction of $f$ to strict predecessors. The extracted rules are semantically sound in Hickey’s predicative PER hierarchy; ordered records, width restriction, and the Point example use that exact witness.

Type inference and extensional equality remain undecidable, the order is not inferred by the source, and independently packed representations do not support the desired binary method. No intensional MLTT or HoTT rule is imported.

The later Cedille Core has retained and erased products, same-erasure dependent intersections, heterogeneous untyped equality, rewriting, direct computation, separation, and ascription. The exact imported semantic results are Stump–Jenkins Theorems 1–2, classification soundness and logical consistency, plus the source’s qualified closed-function normalization statement. The chapter derives induction on the Church subject stored in an intersection. It defines the Tarski meet and imports the exact recLB/recGLB/recRoll/recUnroll derivations. Its concrete large-elimination simulation uses the $\mathsf{NaryR}$ relation and the same-subject intersection definition of $\mathsf{TpEq}$; zero-cost reuse retains explicit $\mathsf{Cast}$ hypotheses.

CDLE boundary. Cedille Core is not globally normalizing. The Kleene trick types a nonnormalizing erasure at a true equality. Simulated large elimination is not native type-level reduction, and extensional isomorphism is not a zero-cost cast.

The experimental ${\mathsf{c}}_2$ full-language safety claim is conditional and oracle-relative; its proposed characterization is conjectural. The Kappa corpus establishes only five finite observations.