A Characterization of $\mathbf{ML}$ in Many-Sorted Arithmetic with Conditional Application
Swaen, M. D. G.
J. Symbolic Logic, Tome 57 (1992) no. 1, p. 924-953 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
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 in $\mathrm{ML}$, resulting in a characterization of strong $\Sigma$-elimination by an axiom of conditional choice.
Publié le : 1992-09-14
Classification:  
@article{1183744049,
     author = {Swaen, M. D. G.},
     title = {A Characterization of $\mathbf{ML}$ in Many-Sorted Arithmetic with Conditional Application},
     journal = {J. Symbolic Logic},
     volume = {57},
     number = {1},
     year = {1992},
     pages = { 924-953},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744049}
}

Swaen, M. D. G. A Characterization of $\mathbf{ML}$ in Many-Sorted Arithmetic with Conditional Application. J. Symbolic Logic, Tome 57 (1992) no. 1, pp.  924-953. http://gdmltest.u-ga.fr/item/1183744049/