## Interpreting descriptions in intensional type theory.(English)Zbl 1089.03051

Summary: Natural deduction systems with indefinite and definite descriptions $$(\varepsilon$$-terms and $$\iota$$-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.

### MSC:

 03F35 Second- and higher-order arithmetic and fragments 03F50 Metamathematics of constructive systems 03F55 Intuitionistic mathematics
Full Text:

### References:

 [1] Annals of the Japan Association for Philosophy of Science 4 pp 49– (1971) · Zbl 0287.02014 [2] The logic of description and existence (1973) [3] Twenty-five years of constructive type theory (Venice, 1995) 36 pp 221– (1998) [4] DOI: 10.2969/jmsj/00740323 · Zbl 0067.25003 [5] Existential instantiation in a system of natural deduction for intuitionistic arithmetics (1973) · Zbl 0261.02015 [6] Intuitionism: An introduction (1956) [7] DOI: 10.2307/2181485 [8] Zeitschrift für Philosophic und philosophische Kritik 100 pp 25– (1892) [9] Types for proofs and programs, second international workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24–28, 2002, selected papers 2646 pp 78– (2003) [10] Foundations of constructive analysis (1967) · Zbl 0183.01503 [11] Types for proofs and programs, international workshop, TYPES 2000, Durham, UK, December 8–12, 2000, selected papers 2277 pp 1– (2002) [12] Foundations of software science and computation structures, 7th international conference, FOSSACS 2004, Barcelona, Spain, March 29–April 2, 2004, proceedings 2987 pp 12– (2004) [13] Introduction to mathematical philosophy (1920) · JFM 47.0036.12 [14] Mind 14 pp 479– (1905) [15] Type-theoretical grammar (1994) · Zbl 0855.68073 [16] Natural deduction: a proof-theoretical study (1965) · Zbl 0173.00205 [17] Programming in Martin-LÖf’s type theory (1990) · Zbl 0744.03029 [18] DOI: 10.1007/BF01091551 · Zbl 0404.03045 [19] A course in constructive algebra (1988) · Zbl 0725.03044 [20] Intuitionistic type theory (1984) [21] Annals of the Japan Association for Philosophy of Science 3 pp 242– (1970) · Zbl 0226.02032 [22] Journal of the Faculty of Science University of Tokyo, Section 1 7 pp 419– (1957) [23] Proceedings of the third Scandinavian logic symposium pp 197– (1975) [24] DOI: 10.1007/BFb0061839
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.