Universe presentation and paradox boundaries

Russell hierarchy

Signature.

External natural levels; Russell membership; closure under the $\mathrm{\Pi }$, $\mathrm{\Sigma }$, W, sum, void, unit, Boolean, and natural-number formers available through chapter 28. Explicit strict lifting is optional and is kept distinct from the cumulative-membership extension used by the level-solving section.

Locally proved.

Families-as-maps, the ${\mathsf{Fin}}_{\mathrm{LE}}$ computation, least solutions for one-sided normalized unknown constraints relative to external-parameter assumptions, large Boolean elimination, and soundness in the stages $V_{{\kappa }_i}$ for strongly inaccessible ${\kappa }_i$.

Model boundary.

Relative consistency and Boolean separation assume an omega-sequence of strongly inaccessible cardinals. No normalization, conversion decision, or necessity result is inferred.

Engineering boundary.

The Kappa corpus evaluates concrete finite constraints built from maxima and successors. The cited Mugen and fuss-free results retain their own signatures and hypotheses.

Strict Tarski presentation

Signature.

Codes and decoding for exactly the chapter 29 former fragment, with judgmental decoding equations and structural substitution.

Locally proved.

Substitution, erasure to the Russell presentation, and fixed-derivation decoration in the constructor-generated fragment. The round trip is comparison-aligned conclusion by conclusion; equality of proof trees is not claimed.

Coherence boundary.

Derivation-independent decoration needs an additional coherence theorem. At Kovács’s semantic signature this consists of natural inverse $\mathsf{Code}$/$\mathsf{El}$ operations and the Russell identifications displayed in the chapter. Propositional decoding would require transports and higher coherence; decoding injectivity is not assumed, and the tagged-code model in the seminar shows it can fail.

Artifact boundary.

The Kappa corpus checks a finite de Bruijn code language and its scope-sensitive round trips, not the general comparison theorem.

Hurkens and Reynolds–Hurkens

Signature.

The ${\mathsf{U}}^{-}$ interface has two decoded universes, two large and two small product operations, all four introduction and application operations, and beta only for the two large products. The chapter uses judgmental large-beta equations to expose the conversion ledger. Spiwack’s source states equality axioms and transports along them, so the chapter’s presentation is intentionally stronger at this point.

Exact replay.

The typed $V,U,\mathsf{sb},\mathsf{le},\mathsf{Ind},\mathsf{WF},\mathsf{D},\mathsf{J},I$ spine is reconstructed locally. Explicit terms $\mathrm{\Omega },L_1,L_2$ inhabit the three intermediate types, and $L_2{\cdot }_0\mathrm{\Omega }$ inhabits an arbitrary decoded small code. The three inhabitants yielding ${\mathsf{El}}_0(F)$ for arbitrary $F:U_0$ are replayed from Spiwack’s proof pages, with a one-for-one operation map and an explicit four-conversion ledger. The preceding item records the deliberate change in equality presentation.

Separate theorem card.

Coquand’s higher-order-logic variation assumes maps $T(A)\to A$ and $A\to T(A)$, together with the judgmental equation $\mathsf{match}\circ \mathsf{intro}=T(\mathsf{intro}\circ \mathsf{match})$. It is not derived from the Hurkens card.

Not claimed.

Consistency of every weakened interface, inconsistency of ordinary predicative hierarchies, or transfer from a type-in-type replay. The Kappa artifact is only a ten-flag, eight-case assumption-use ledger; it is not a parser, a dependent term checker, or a mechanization of the proof.