The constructive Hilbert program and the limits of Martin-Löf type theory (Q813417)

This is a survey of proof-theoretic investigations of Martin-Löf type theory. Hilbert's original program aimed at a consistency proof for the systems of working mathematics in finitistic systems. Constructive Hilbert's program allows for systems which are constructive and predicative. In this connection the author studies constructive type theories due to Martin-Löf and their extensions. After a general discussion of the theory of meaning due to Prawitz and Martin-Löf, some specific systems and their connection with popular subsystems of classical analysis are discussed. The system \textbf{MLF}, introduced by Rathjen, extends original Martin-Löf type theory by an operation producing a new universe operator \textbf{S(F)} from each operator \textbf{F} from families of types to families of types. A stronger system, \textbf{MLQ}, introduced independently by Rathjen and Palmgren, has universes of type two. It contains a universe \textbf{M} and a universe \textbf{Q} of codes for type constructors like \textbf{S}. A. Setzer gave a formalization \textbf{TTM} of a Mahlo universe in constructive type theory. This addition is fundamentally different (``not foreshadowed in Martin-Löf's original papers''): models of such a Mahlo universe are generated by a nonmonotonic inductive definition. Moreover, \textbf{TTM} is incompatible with elimination rules for the universe. This prompted Martin-Löf to respond that universes need not be equipped with elimination rules. Original Martin-Löf type theory is equiconsistent with the subsystem \((\Sigma^1_2\text{-AC})+\text{TI}\) of analysis. In a less formalized section, the author argues that everything a Martin-Löf type theorist can ever develop can be emulated in a system \(\mathbf{KP}^r+\forall x \exists M(x\in M\and M\prec_1 V)\) where \(\mathbf{KP}^r\)is \(\mathbf{KP}\) with foundation scheme restricted to sets and \(\prec_1\) means \(\Sigma_1\)-substructure.