Interpreting Descriptions in Intensional Type Theory

Journal of Symbolic Logic 70 (2):488 - 514 (2005)
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
Download options
PhilPapers Archive

Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 20,048
External links
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles
Kent Bach (2004). Descriptions: Points of Reference. In Marga Reimer & Anne Bezuidenhout (eds.), Descriptions and Beyond. Clarendon Press 189-229.
B. H. Slater (1991). The Epsilon Calculus and its Applications. Grazer Philosophische Studien 41:175-205.
Berit Brogaard (2007). Sharvy's Theory of Definite Descriptions Revisited. Pacific Philosophical Quarterly 88 (2):160–180.

Monthly downloads

Added to index


Total downloads

10 ( #324,729 of 1,793,278 )

Recent downloads (6 months)

1 ( #463,804 of 1,793,278 )

How can I increase my downloads?

My notes
Sign in to use this feature

Start a new thread
There  are no threads in this forum
Nothing in this forum yet.