A characterization of ML in many-sorted arithmetic with conditional application
M. D. G. Swaen · Journal of Symbolic Logic · 1992
Abstract In this paper we discuss an interpretation of intuitionistic type theory in many-sorted arithmetic with so-called conditional application. Via the formulas-as-types correspondence the arithmetical system in turn can be embedded inML, resulting in a characterization of strong Σ-elimination by an axiom of conditional choice.