Extending Martin-Löf type theory by one Mahlo-universe (Q1568707)

We define a type theory \(\mathbb{M}\mathbb{L}\mathbb{M}\), which has proof-theoretical strength slightly greater than Rathjen's theory \(\mathbb{K}\mathbb{P}\mathbb{M}\). This is achieved by replacing the ordinary universe in Martin-Löf's type theory by a new universe \(\mathbb{V}\). \(\mathbb{V}\) has the property that for every function \(f\), mapping families of sets in \(\mathbb{V}\) to families of sets in \(\mathbb{V} \), there exists a subuniverse of \(\mathbb{V}\) closed under \(f\) and represented in \(\mathbb{V}\). We show that the proof-theoretical strength of \(\mathbb{M}\mathbb{L} \mathbb{M}\) is \(\geq\psi_{\Omega_1} \Omega_{\mathbb{M} +\omega}\). Therefore we reach a strength slightly greater than that of \(\mathbb{K}\mathbb{P}\mathbb{M}\) and \(\mathbb{V}\) can be considered as the type-theoretic equivalent of a recursively Mahlo ordinal. Together with the author's ``A model for a type theory with Mahlo universe'' [Draft. Available via \url{http://www.math.uu.se/~setzer/articles/uppermahlo.dvi.gz}], in which \(\mathbb{M} \mathbb{L} \mathbb{M}\) is modelled in a suitable extension of \(\mathbb{K}\mathbb{P}\mathbb{M}\), it follows \(|\mathbb{M} \mathbb{L} \mathbb{M}|= \psi_{\Omega_1}(\Omega_{\mathbb{M}+\omega})\).