ch:logic-enriched-type-theory: logic-enriched type theory

Assume $h:(P\Rightarrow \mathrm{\perp })\Rightarrow \mathrm{\perp }$. To apply LTT-Classical, add $k:P\Rightarrow \mathrm{\perp }$. Then $h,k:\mathrm{\perp }$ by LTT-$\Rightarrow$-E; LTT-Classical discharges $k$ and yields $P$. Finally LTT-$\Rightarrow$-I discharges $h$. This is the unique classical step. Every line is an entailment judgment $\mathrm{\Gamma };\mathrm{\Delta }⊢Q$; no term judgment $\mathrm{\Gamma }⊢t:A$ is produced, so the derivation adds no inhabitant of an object type.

The number-quantified proposition is small and hence analytic. It may occur in comprehension and in both induction schemes. The set-of-naturals quantified proposition is analytic but not small; it is forbidden in comprehension and ${\mathsf{LTT}}_0$ induction, but permitted in ${\mathsf{LTT}}_0^{\ast }$ induction. The set-of-sets quantified proposition is neither; all three uses reject it. The matrix being a tautology or $\mathrm{\perp }$ does not change these classifications because the offending binder remains.

Let $p(n)$ be the small code for $\mathrm{\exists }k:\mathsf{N}.n=k\cdot k$ and put $S:=\{n:\mathsf{N}\mid p(n)\}$. Then LTT-Set-$\beta$ gives $$\mathrm{\Gamma };\varnothing ⊢n\in S\iff \mathsf{V}(p(n))\equiv \mathrm{\exists }k:\mathsf{N}.n=k\cdot k.$$ The left-to-right direction is biconditional elimination followed by its first implication; the right-to-left direction uses the second implication. Existential introduction at $S$ proves the translated comprehension instance.

In type-free second-order arithmetic the translation is $$\mathrm{\forall }X\mathrm{\exists }n(n\in X),$$ where $X$ is a set variable and $n$ is a number variable. Removing type annotations does not change the source-level smallness judgment. The outer quantifier $$\mathrm{\forall }X:\mathsf{Set}(\mathsf{N})$$ does not range over a decoded small type. It is therefore the precise obstruction to a small proposition code and hence to comprehension.

For arithmetical $P(n)$, translate comprehension by $\{n:\mathsf{N}\mid |P(n)|\}$ and use LTT-Set-$\beta$; translate number induction by LTT-Nat-Ind${}_0$, since $|P|$ is small. These are the two nonlogical cases of the forward rule induction.

The imported reverse chain is $${\mathsf{LTT}}_0⟶T_{\omega }U⟶T_{\omega }⟶T_2⟶{\mathsf{ACA}}_0.$$ Definitions 5.30–5.31 provide satisfaction for the bounded signatures; Theorems 5.32–5.33 give soundness and completeness, and Corollary 5.33.1 therefore lowers a $B_{n+1}$ derivation of an already-$B_n$ judgment to $B_n$. Corollaries 5.33.2–5.33.3 complete the displayed chain. This is a semantic existence argument using interpretations and satisfaction, not a recursive transformation on derivation syntax, so the imported theorem does not supply an effective proof translator.