Publisher： Cambridge University Press
E-ISSN： 1943-5886|70|2|488-514
ISSN： 0022-4812
Source： The Journal of Symbolic Logic, Vol.70, Iss.2, 2005-06, pp. : 488-514
Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.
Abstract
Natural deduction systems with indefinite and definite descriptions (ε-terms and ι-terms) are presented, and interpreted in Martin-LÖf's intensional type theory. The interpretations are formalizations of ideas which are implicit in the literature of constructive mathematics: if we have proved that an element with a certain property exists, we speak of ‘the element such that the property holds’ and refer by that phrase to the element constructed in the existence proof. In particular, we deviate from the practice of interpreting descriptions by contextual definitions.
Related content
Intensional logic and two-sorted type theory
The Journal of Symbolic Logic, Vol. 54, Iss. 1, 1989-03 ,pp. :
Access to resources
Recommend
An intensional type theory: motivation and cut-elimination
The Journal of Symbolic Logic, Vol. 66, Iss. 1, 2001-03 ,pp. :
Intensional models for the theory of types
The Journal of Symbolic Logic, Vol. 72, Iss. 1, 2007-03 ,pp. :
General models, descriptions, and choice in type theory
The Journal of Symbolic Logic, Vol. 37, Iss. 2, 1972-06 ,pp. :
Intensional interpretations of functionals of finite type I
The Journal of Symbolic Logic, Vol. 32, Iss. 2, 1967-08 ,pp. :