{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,23]],"date-time":"2024-01-23T23:38:17Z","timestamp":1706053097814},"reference-count":7,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":3845,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2003,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Restricted to first-order formulas, the rules of inference in the Curry-Howard type theory are equivalent to those of first-order predicate logic as formalized by Heyting, with one exception: \u2203-elimination in the Curry-Howard theory, where \u2203<jats:italic>x<\/jats:italic>:<jats:italic>A,F<\/jats:italic>(<jats:italic>x<\/jats:italic>) is understood as disjoint union, are the projections, and these do not preserve first-orderedness. This note shows, however, that the Curry-Howard theory is conservative over Heyting's system.<\/jats:p>","DOI":"10.2178\/jsl\/1058448436","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T21:06:35Z","timestamp":1109797595000},"page":"751-763","source":"Crossref","is-referenced-by-count":5,"title":["The completeness of Heyting first-order logic"],"prefix":"10.1017","volume":"68","author":[{"given":"W. W.","family":"Tait","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200008495_ref002","unstructured":"Howard W. , The formula as-types notion of construction, In Hindley and Sheldon [1], pp. 479\u2013490."},{"key":"S0022481200008495_ref005","unstructured":"Tait W. , A second order theory of functional of higher type, with two appendices. Appendix A: Intensional functional. Appendix B: An interpretation of functional by convertible terms, Stanford Seminar Report 1963, pp. 171\u2013206. A published version is [6]."},{"key":"S0022481200008495_ref007","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1093\/oso\/9780195079296.003.0004","volume-title":"Mathematics and Mind","author":"Tait","year":"1994"},{"key":"S0022481200008495_ref001","volume-title":"To H.B. Curry: Essays on Combinatorial Logic, Lambda Calculus and Formalism","author":"Hindley","year":"1980"},{"key":"S0022481200008495_ref006","first-page":"198","volume":"32","author":"Tait","year":"1967","journal-title":"Intensional interpretations of functional offinite type I"},{"key":"S0022481200008495_ref003","unstructured":"Martin-L\u00f6f P. , An intuitionistic theory of types, In Sambin and Smith [4], pp. 221\u2013244."},{"key":"S0022481200008495_ref004","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198501275.001.0001","volume-title":"Twenty five years of constructive type theory","author":"Sambin","year":"1998"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200008495","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,23]],"date-time":"2024-01-23T22:45:46Z","timestamp":1706049946000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200008495\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":7,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S0022481200008495"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1058448436","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}