A characterization of ML in many-sorted arithmetic with conditional application (Q4032872)

The article deals with the question which logic, via the formulas-as- types correspondence, can be identified with Martin-Löf's type theory. The author considers the version of Martin Löf's type theory without higher order types, introduced as \(\text{ML}_ 0\) by \textit{A. S. Troelstra} and \textit{D. van Dalen} [Constructivism in mathematics. An introduction. Vol. II (1988; Zbl 0661.03047)]. As to the logic, an extension of \(\text{HA}^ \omega\), called \(\text{cHA}\) is developed, in which an axiom of choice can be formulated that corresponds closely to the strong sigma-elimination rule of \(\text{ML}_ 0\). The extension \(\text{cHA}\) consists in adding types of functions ranging over the subset of a type, characterized by some \(\exists\)-free formula. I.e., let \(\sigma\) and \(\tau\) be types, let \(\varphi(x^ \sigma)\) be an \(\exists\)-free formula, then in \(\text{cHA}\) there is a so-called conditional \(\Pi\)-type, \(\Pi x^{\sigma:\varphi}.\tau\), of functions \(f\) that are applicable only to elements \(x\in\sigma\) for which \(\varphi(x)\) holds. With conditional \(\Pi\)-types the axiom of conditional choice is formulated: \[ \forall x^ \sigma(\varphi\to\exists y^ \tau\psi(y))\to\exists f\in\Pi x^{\sigma:\varphi}.\tau\quad\forall x^ \sigma(\varphi\to\psi(f(x)))\quad (\varphi\;\exists\;\text{-free}). \tag{cAC} \] It is then proved by formalised realizability that a formula is derivable in the logic \(\text{cHA}+\text{cAC}\) iff the corresponding type is inhabited in the type theory \(\text{ML}_ 0\).