{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,7,13]],"date-time":"2023-07-13T13:13:56Z","timestamp":1689254036164},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":3206,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2005,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Natural deduction systems with indefinite and definite descriptions (\u03b5-terms and \u03b9-terms) are presented, and interpreted in Martin-L\u00d6f'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 \u2018the element such that the property holds\u2019 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.<\/jats:p>","DOI":"10.2178\/jsl\/1120224725","type":"journal-article","created":{"date-parts":[[2005,7,1]],"date-time":"2005-07-01T15:03:48Z","timestamp":1120230228000},"page":"488-514","source":"Crossref","is-referenced-by-count":5,"title":["Interpreting descriptions in intensional type theory"],"prefix":"10.1017","volume":"70","author":[{"given":"Jesper","family":"Carlstr\u00f6m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200007040_ref017","volume-title":"Type-theoretical grammar","author":"Ranta","year":"1994"},{"key":"S0022481200007040_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/BF01091551"},{"key":"S0022481200007040_ref016","volume-title":"Natural deduction: a proof-theoretical study","author":"Prawitz","year":"1965"},{"key":"S0022481200007040_ref015","volume-title":"Programming in Martin-L\u00d6f's type theory","author":"Nordstr\u00d6m","year":"1990"},{"key":"S0022481200007040_ref009","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/00740323"},{"key":"S0022481200007040_ref006","doi-asserted-by":"publisher","DOI":"10.2307\/2181485"},{"key":"S0022481200007040_ref022","doi-asserted-by":"publisher","DOI":"10.4288\/jafpos1956.4.49"},{"key":"S0022481200007040_ref023","volume-title":"The logic of description and existence","author":"Stenlund","year":"1973"},{"key":"S0022481200007040_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061839"},{"key":"S0022481200007040_ref001","first-page":"12","volume-title":"Foundations of software science and computation structures, 7th international conference, FOSSACS 2004, Barcelona, Spain, March 29\u2013April 2, 2004, proceedings","volume":"2987","author":"Abadi","year":"2004"},{"key":"S0022481200007040_ref012","volume-title":"Intuitionistic type theory","author":"Martin-L\u00d6f","year":"1984"},{"key":"S0022481200007040_ref003","volume-title":"Foundations of constructive analysis","author":"Bishop","year":"1967"},{"key":"S0022481200007040_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70732-8"},{"key":"S0022481200007040_ref010","first-page":"419","article-title":"Equality axiom on Hilbert's \u03b5-symbol","volume":"7","author":"Maehara","year":"1957","journal-title":"Journal of the Faculty of Science University of Tokyo, Section 1"},{"key":"S0022481200007040_ref005","first-page":"25","article-title":"\u00dcber Sinn und Bedeutung","volume":"100","author":"Frege","year":"1892","journal-title":"Zeitschrift f\u00fcr Philosophic und philosophische Kritik"},{"key":"S0022481200007040_ref004","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/3-540-39185-1_5","volume-title":"Types for proofs and programs, second international workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24\u201328, 2002, selected papers","volume":"2646","author":"Carlstr\u00f6m","year":"2003"},{"key":"S0022481200007040_ref020","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1093\/oso\/9780198501275.001.0001","volume-title":"Twenty-five years of constructive type theory (Venice, 1995)","volume":"36","author":"Sambin","year":"1998"},{"key":"S0022481200007040_ref002","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-45842-5_1","volume-title":"Types for proofs and programs, international workshop, TYPES 2000, Durham, UK, December 8\u201312, 2000, selected papers","volume":"2277","author":"Aczel","year":"2002"},{"key":"S0022481200007040_ref007","volume-title":"Intuitionism: An introduction","author":"Heyting","year":"1956"},{"key":"S0022481200007040_ref018","doi-asserted-by":"publisher","DOI":"10.1093\/mind\/XIV.4.479"},{"key":"S0022481200007040_ref011","doi-asserted-by":"publisher","DOI":"10.4288\/jafpos1956.3.242"},{"key":"S0022481200007040_ref008","volume-title":"Existential instantiation in a system of natural deduction for intuitionistic arithmetics","author":"Leivant","year":"1973"},{"key":"S0022481200007040_ref019","volume-title":"Introduction to mathematical philosophy","author":"Russell","year":"1920"},{"key":"S0022481200007040_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8640-5"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200007040","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,12]],"date-time":"2021-07-12T21:01:32Z","timestamp":1626123692000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200007040\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["S0022481200007040"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1120224725","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,6]]}}}