Classical predicative logic-enriched type theories (Q636367)

The authors develop two systems of type theory, \(\text{LTT}_0\) and \(\text{LTT}^*_0\), and prove these systems are conservative over the systems \(\text{ACA}_0\) and \(\text{ACA}\) of second-order arithmetic, respectively. The systems developed here are quite different from ones based on \(\text{E-PRA}^\omega\) previously considered by \textit{U. Kohlenbach} [``Higher order reverse mathematics'', Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)]. These theories include types for both sets and functions, perhaps modeling classical usage more closely. More importantly, the theories studied here are ``logic-enriched'': they include a formalized logic for propositions, and terms from this logic are used in forming terms for sets. The authors compare their two systems of type theory with a third system, \(\text{LTT}_W\), which they developed in their previous work [``Weyl's predicative classical mathematics as a logic-enriched type theory'', Lect. Notes Comput. Sci. 4502, 1--17 (2007; Zbl 1178.03019)]. They argued there that \(\text{LTT}_W\) corresponds closely with Weyl's programme of predicativism. Both \(\text{LTT}_0\) and \(\text{LTT}^*_0\) are subsystems of \(\text{LTT}_W\); the authors show that \(\text{LTT}_0\) is strictly weaker than \(\text{LTT}_W\), while leaving as an open question the equivalence of \(\text{LTT}_W\) and \(\text{LLT}_0^*\). The authors discuss possible interpretations of their results in terms of Weyl's programme. The authors obtain, as a variation of their methods, an elegant new proof that \(\text{ACA}_0\) is conservative over first-order Peano arithmetic. They also state that their methods give a translation of \(\text{ACA}_0^+\) into \(\text{LTT}_W\), leaving open the question of finding a subsystem of \(\text{LTT}_W\) that is conservative over \(\text{ACA}_0^+\).