{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,21]],"date-time":"2024-05-21T05:13:26Z","timestamp":1716268406492},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":11789,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1981,12]]},"abstract":"<jats:p>It is probably because intuitionism is founded on the concept of (abstract) <jats:italic>proof<\/jats:italic> that it has been possible to develop various kinds of models. The following is but a partial list: Gabbay [5], Beth [2], Kripke [8], Kleene [7], L\u00e4uchli [9], McKinsey and Tarski [10], Rasiowa and Sikorski [14], Scott [15], de Swart [16], and Veldman [17].<\/jats:p><jats:p>The original purpose for having the models appears to have been for obtaining independence or consistency results for certain formalizations of intuitionism [see Beth [2], Prawitz [13]]; of course, if the models could be also justified as being plausible interpretations of intuitionistic thinking, so much the better. In fact, having some kind of plausible interpretation makes it much easier to work with the models. Occasionally the models were used to suggest possible extensions of the formal systems; for example, the Kripke models with constant domains have motivated interest in the formal logic <jats:bold>CD<\/jats:bold> which extends the Intuitionistic Predicate Calculus (<jats:bold>IPC<\/jats:bold>) by having the axiom schema<\/jats:p><jats:p><jats:disp-formula><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0022481200045072_eqnU1\" \/><\/jats:disp-formula><\/jats:p>","DOI":"10.2307\/2273226","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T17:57:46Z","timestamp":1146938266000},"page":"773-780","source":"Crossref","is-referenced-by-count":3,"title":["Equivalence between semantics for intuitionism. I"],"prefix":"10.1017","volume":"46","author":[{"given":"E. G. K.","family":"L\u00f3pez-Escobar","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200045072_ref008","first-page":"92","volume-title":"Formal systems and recursive functions","author":"Kripke","year":"1963"},{"key":"S0022481200045072_ref003","unstructured":"Caicedo X. , Back and forth in infinitary languages, Ph. D. thesis, University of Maryland, 1978."},{"key":"S0022481200045072_ref010","first-page":"1","volume":"13","author":"McKinsey","year":"1948","journal-title":"Some theorems about the sentential calculi of Lewis and Heyting"},{"key":"S0022481200045072_ref016","first-page":"564","volume":"42","author":"de Swart","year":"1977","journal-title":"An intuitionistically plausible interpretation of intuitionistic logic"},{"key":"S0022481200045072_ref007","first-page":"109","volume":"10","author":"Kleene","year":"1945","journal-title":"On the interpretation of intuitionistic number theory"},{"key":"S0022481200045072_ref005","first-page":"306","volume":"42","author":"Gabbay","year":"1977","journal-title":"A new version of Beth semantics for intuitionistic logic"},{"key":"S0022481200045072_ref013","volume-title":"Proof theory and Intuitionism","author":"Prawitz","year":"1968"},{"key":"S0022481200045072_ref009","volume-title":"Intuitionism and proof theory","author":"L\u00e4uchli","year":"1968"},{"key":"S0022481200045072_ref001","volume-title":"Constructivity in mathematics","author":"Beth","year":"1957"},{"key":"S0022481200045072_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(78)90029-3"},{"key":"S0022481200045072_ref012","volume-title":"Natural deduction, a proof-theoretical study","author":"Prawitz","year":"1965"},{"key":"S0022481200045072_ref011","volume-title":"Categories for the working mathematician","author":"MacLane","year":"1971"},{"key":"S0022481200045072_ref002","volume-title":"The foundations of mathematics","author":"Beth","year":"1959"},{"key":"S0022481200045072_ref015","volume-title":"Completeness proofs for the Intuitionistic sentential calculus","author":"Scott","year":"1957"},{"key":"S0022481200045072_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(76)90008-5"},{"key":"S0022481200045072_ref014","volume-title":"The mathematics of metamathematics","author":"Rasiowa","year":"1963"},{"key":"S0022481200045072_ref017","first-page":"159","volume":"41","author":"Veldman","year":"1976","journal-title":"An intuitionistic completeness theorem for intuitionistic predicate logic"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200045072","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T15:19:59Z","timestamp":1558797599000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200045072\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1981,12]]},"references-count":17,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1981,12]]}},"alternative-id":["S0022481200045072"],"URL":"https:\/\/doi.org\/10.2307\/2273226","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1981,12]]}}}