Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-11-29T16:56:14.230Z Has data issue: false hasContentIssue false
  • English
  • Français

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

Published online by Cambridge University Press:  12 March 2014

M. D. G. Swaen
M. D. G. Swaen*
Affiliation:
Fakulteit Wiskunde en Informatika, Universiteit van Amsterdam, 1018 TV Amsterdam, The Netherlands
Get access Rights & Permissions [Opens in a new window]

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 in ML, resulting in a characterization of strong Σ-elimination by an axiom of conditional choice.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 57 , Issue 3 , September 1992 , pp. 924 - 953
Copyright
Copyright © Association for Symbolic Logic 1992

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Martin-Löf, P. [80], Intuitionistic type theory, Bibliopolis, Naples.CrossRefGoogle Scholar
de Lavalette, G. R. Renardel [85], Theories with type-free application and extended bar-induction, Thesis, Universiteit van Amsterdam, Amsterdam.Google Scholar
Smith, J. M. [84], An interpretation of Martin-Löf's type theory in a type-free theory of propositions, this Journal, vol. 49, pp. 730–753.Google Scholar
Swaen, M. D. G. [89], Weak and strong sum-elimination in intuitionistic type theory, Thesis, Universiteit van Amsterdam, Amsterdam.Google Scholar
Troelstra, A. S. (editor) [73], Metamathematical investigations of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin.Google Scholar
Troelstra, A. S. and van Dalen, D. [88], Constructivism in mathematics. II, North-Holland, Amsterdam.Google Scholar