Logic-Enriched Type Theory and Predicative Mathematics

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

The assertion that a natural number is even needs no computational payload in order to define the set of even numbers. Under propositions-as-types, however, the assertion and its proofs inhabit the same typed term language as the number. Classical double-negation elimination then becomes a data constructor with no reduction rule. A predicative development has a second reason to resist this identification: a set may be defined by quantifying over numbers without thereby permitting quantification over the totality of all sets.

Write $$\mathsf{Even}(n):=\mathrm{\exists }k:\mathsf{N}.n=k+k.$$ The expression $\mathsf{Even}(n)$ below is a proposition, not a type, and a derivation of it is not a term stored beside $n$. This separation is the operation performed by a logic-enriched type theory: its logical judgments may depend on typed terms, while its term judgments do not acquire proof objects merely because the logic is classical.

The four judgments

The context split has a visible consequence. If $h:\mathsf{Even}(n)$ were a term variable, then $\mathrm{\Gamma },h:\mathsf{Even}(n)$ would be a term context, which is ill formed because $\mathsf{Even}(n)$ is not a type. The correct hypothesis is $\mathsf{Even}(n)\in \mathrm{\Delta }$.

The logical formation rules are stated before their proof rules. The omitted well-formedness premises are restored where a dependency matters.

$\mathrm{\Gamma }\mathsf{valid}$

$\mathrm{\Gamma }⊢\mathrm{\perp }\mathsf{Prop}$

$\mathrm{\Gamma }⊢P\mathsf{Prop}$$\mathrm{\Gamma }⊢Q\mathsf{Prop}$

$\mathrm{\Gamma }⊢P\Rightarrow Q\mathsf{Prop}$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma },x:A⊢P\mathsf{Prop}$

$\mathrm{\Gamma }⊢\mathrm{\forall }x:A.P\mathsf{Prop}$

$\mathrm{\Gamma }⊢a:\mathsf{U}$$\mathrm{\Gamma }⊢t:\mathsf{T}(a)$$\mathrm{\Gamma }⊢X:\mathsf{Set}(\mathsf{T}(a))$

$\mathrm{\Gamma }⊢t{\in }_{a}X\mathsf{Prop}$

Classical entailment is generated by the following introduction, elimination, and classical rules together with structural exchange, weakening, and contraction on $\mathrm{\Delta }$.

$P\in \mathrm{\Delta }$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P$

$\mathrm{\Gamma };\mathrm{\Delta },P⊢Q$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P\Rightarrow Q$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P\Rightarrow Q$$\mathrm{\Gamma };\mathrm{\Delta }⊢P$

$\mathrm{\Gamma };\mathrm{\Delta }⊢Q$

$\mathrm{\Gamma },x:A;\mathrm{\Delta }⊢P$$x\notin \mathrm{FV}(\mathrm{\Delta })$

$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathrm{\forall }x:A.P$

$\mathrm{\Gamma };\mathrm{\Delta }⊢\mathrm{\forall }x:A.P$$\mathrm{\Gamma }⊢t:A$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P[t/x]$

$\mathrm{\Gamma };\mathrm{\Delta },P\Rightarrow \mathrm{\perp }⊢\mathrm{\perp }$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P$

For example, let $P$ be well formed. The derivation

$P\in \mathrm{\Delta },P$

$\mathrm{\Gamma };\mathrm{\Delta },P⊢P$

$\mathrm{\Gamma };\mathrm{\Delta }⊢P\Rightarrow P$

has no corresponding term $\lambda p.p$ in the type language. Its absence is not proof irrelevance; there are simply no proof terms to compare.

Predicative sets

The type component may depend on a name of a small proposition. This is the one controlled passage from logic to data.

Let $\widehat{\mathsf{Even}}(n)$ be a code for $\mathrm{\exists }k:\mathsf{N}.n=k+k$. The set $$E:=\{n:\mathsf{N}\mid \widehat{\mathsf{Even}}(n)\}$$ is well formed. At $6$, membership computes by LTT-Set-$\beta$ to $\mathrm{\exists }k:\mathsf{N}.6=k+k$, and the witness $3$ proves that proposition. At $5$, classical arithmetic proves its negation. Neither proof changes the runtime representation of $E$; $E$ is a characteristic specification, not a list containing certificates.

The tempting set $$\{n:\mathsf{N}\mid \mathrm{\forall }X:\mathsf{Set}(\mathsf{N}).n\in X\Rightarrow n\in X\}$$ is rejected. Its predicate is analytic but not small. Analyticity is enough for induction in ${\mathsf{LTT}}_0^{\ast }$, not for comprehension in either predicative subsystem.

Recursion and induction have different ranges

Natural-number recursion constructs terms; induction derives propositions. Conflating the two would erase the architectural distinction.

Define $\mathsf{double}(n)$ by recursion with $z=0$ and $s(k,r)=r+2$. Its first three reductions are $$\mathsf{double}(2)\stackrel{LTT-Nat-rec-S}{\equiv }\mathsf{double}(1)+2\stackrel{LTT-Nat-rec-S}{\equiv }\mathsf{double}(0)+2+2\stackrel{LTT-Nat-rec-0}{\equiv }4.$$ The derivation that $\mathsf{double}(n)$ is even is instead an instance of LTT-Nat-Ind${}_0$. Its step uses the arithmetic implication $\mathsf{Even}(r)\Rightarrow \mathsf{Even}(r+2)$; no certificate appears in the recursive output.

The exact conservativity calculation

Write $⟨t⟩$ for the translation of a second-order arithmetic term into a term of $\mathsf{N}$, and $⟨P⟩$ for the translation of a formula into an LTT proposition. The decisive clauses are An arithmetical formula also has a small code $|P|$ satisfying $\mathsf{V}(|P|)\equiv ⟨P⟩$. This equation is what converts the arithmetical comprehension axiom into LTT-Set-I.

Proof of Theorem 92.5 — Displayed conservativity pair

Proof. For the first implication, translate an ${\mathsf{ACA}}_0$ derivation rule by rule. Logical rules map to the rules above. An arithmetical comprehension instance $\mathrm{\exists }X.\mathrm{\forall }n.(n\in X\iff P(n))$ maps to the set $\{n:\mathsf{N}\mid |P(n)|\}$; rule LTT-Set-$\beta$ supplies the translated biconditional. Set induction maps to LTT-Nat-Ind${}_0$ because its predicate has a small code.

The reverse implication is the imported half. Adams and Luo first define the satisfaction relation for the exact bounded signatures $B_n$ in Definitions 5.30 and 5.31, prove its soundness and completeness in Theorems 5.32 and 5.33, and derive Corollary 5.33.1: $$J\text{ a }{B}_n\text{ judgment},B_{n+1}⊢J⟹B_n⊢J.$$ Corollaries 5.33.2 and 5.33.3 then compose the exact chain $${\mathsf{LTT}}_0⟶T_{\omega }U⟶T_{\omega }⟶T_2⟶{\mathsf{ACA}}_0.$$ In the notation of this theorem, Corollary 5.33.3 has precisely the signature $$\overline{n}:\mathsf{N},\overline{X}:\mathsf{Set}(\mathsf{N});\varnothing ⊢⟨P⟩⟹{\mathsf{ACA}}_0⊢P.$$ We import that corollary, including its satisfaction definitions and the well-formedness hypotheses on the displayed contexts, from pages 35–36 of the primary source. For the analytic system we import Theorem 6.1 and the three transferred corollaries listed immediately after it on page 37; they replace $T_2,T_{\omega },T_{\omega }U,{\mathsf{LTT}}_0$ by their starred signatures and conclude conservativity over $\mathsf{ACA}$. This import widens induction, not comprehension [AL10a]. ◻

Dropping the smallness premise from comprehension destroys the displayed argument: the characteristic predicate can quantify over the very collection of sets being encoded, so depth lowering no longer produces an arithmetical membership formula. The theorem makes no conservativity claim for that impredicative extension or for ${\mathsf{LTT}}_{\mathrm{W}}$.

One predicative analysis construction

A bounded increasing rational sequence $q:\mathsf{N}\to \mathbb{Q}$ determines a lower cut without quantifying over sets: The predicate is small because its only quantifier ranges over $\mathsf{N}$. If $r\in L_q$ and , choose $n$ with ; transitivity gives and hence $s\in L_q$. If $r\in L_q$, choose $n$ with and then a rational $t$ with ; thus $t\in L_q$. These two calculations prove downward closure and roundedness. The construction does not form the set of all upper bounds of an arbitrary set of reals; that tempting neighbor quantifies over a large set type and lies outside small comprehension.

Five architectures, five answers

The rows do not define translations. In particular, the conservative translation above does not transport an arbitrary theorem from HOL, CIC, or Nuprl into ${\mathsf{LTT}}_0$.

The recovered Plastic distribution accepts the historical chain weyl.lf -> set.lf -> nat.lf and the pluralist chain construct.lf -> example1.lf. This is preservation evidence for those scripts under the 2010–2011 i386 checker. The Weyl formalization index marks later results that remain axioms, and the replay neither audits the historical kernel nor reproves theorem 92.5.

Suggested first pass.

Begin with exercise 92.4, then complete exercise 92.6.

Exercise 92.4¶

★★☆ For the proposition $$\mathrm{\forall }X:\mathsf{Set}(\mathsf{N}).\mathrm{\exists }n:\mathsf{N}.n\in X,$$ write its translation to the type-free second-order language. Then explain why the translation does not make the proposition small. Identify the exact quantifier that prevents its use in comprehension.

Referenced from 4 locations

• Logic-Enriched Type Theory and Predicative Mathematics
• ch:logic-enriched-type-theory: logic-enriched type theory

Exercise 92.5¶

★★★ Reconstruct the comprehension and induction cases of the first implication in theorem 92.5. For the imported reverse implication, write the exact four-stage chain from ${\mathsf{LTT}}_0$ to ${\mathsf{ACA}}_0$, identify the satisfaction soundness/completeness result that lowers $B_{n+1}$ to $B_n$, and state why this semantic import supplies no effective proof translator.

Referenced from 3 locations

• Logic-Enriched Type Theory and Predicative Mathematics
• ch:logic-enriched-type-theory: logic-enriched type theory

Exercise 92.6¶

★★★ Practical project.ltt-predicativity-classifier Implement in Kappa a classifier for proposition syntax with quantifiers over $\mathsf{N}$, $\mathsf{Set}(\mathsf{N})$, and $\mathsf{Set}(\mathsf{Set}(\mathsf{N}))$. Maintain the invariant that small implies analytic. The program must print, for each named input, whether comprehension, ${\mathsf{LTT}}_0$ induction, and ${\mathsf{LTT}}_0^{\ast }$ induction are permitted. It must accept number-only quantification for all three operations, reject a set-of-naturals quantifier for comprehension and ${\mathsf{LTT}}_0$ induction while accepting it for ${\mathsf{LTT}}_0^{\ast }$ induction, and reject a set-of-sets quantifier for all three. Mutating the comprehension check to use analyticity must make the acceptance test fail.

Referenced from 5 locations

• Logic-Enriched Type Theory and Predicative Mathematics
• Logic enrichment and erased dependency: executable records
• ch:logic-enriched-type-theory: proposition classification