{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T08:09:54Z","timestamp":1649059794340},"reference-count":7,"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":13068,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1978,6]]},"abstract":"<jats:p>In 1930, A. Heyting first specified a formal system for part of intuitionistic mathematics. Although his rules were presumably motivated by the \u201cintended interpretation\u201d or meaning of the logical symbols, over the years a number of other possible interpretations have been discovered for which the rules are also valid. In particular, one might mention the realizablity interpretation of Kleene, the (Dialectica) interpretation of G\u00f6del, and various semantic interpretations, such as Kripke models. (Each of these has several variants or close relatives.) Each such interpretation can be regarded as defining precisely a certain \u201cnotion of constructivity\u201d, the study of which may illuminate the still rather vague notions which underlie the intended interpretation; or, if one doubts that there is a single interpretation \u201cintended\u201d by all constructivist mathematicians, the study of precisely defined interpretations may help to delineate and distinguish the possibilities.<\/jats:p><jats:p>In the last few years, Heyting's systems have been vastly extended, in order to encompass the large and growing body of constructive mathematics. Several kinds of new systems have been put forward and studied. The present author has extended the various realizability interpretations to several of these systems [B1], [B2] and drawn a number of interesting applications. The mathematical content of the present paper is an interpretation in the style of Godel's Dialectica interpretation, but applicable to the new systems put forward by Feferman [Fl]. The original motivation for this work was to obtain certain metamathematical applications: roughly speaking, Markov's rule and its variants.<\/jats:p>","DOI":"10.2307\/2272820","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:47:35Z","timestamp":1146952055000},"page":"213-227","source":"Crossref","is-referenced-by-count":1,"title":["A type-free G\u00f6del interpretation"],"prefix":"10.1017","volume":"43","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200049562_ref001","unstructured":"Beeson M. , Principles of continuous choice and continuity of functions in formal systems for constructive mathematics, Annals of Mathematical Logic (to appear)."},{"key":"S0022481200049562_ref002","unstructured":"Beeson M. , Continuity in intuitionistic set theories (to appear)."},{"key":"S0022481200049562_ref003","first-page":"228","volume":"43","author":"Beeson","year":"1978","journal-title":"Some relations between classical and constructive mathematics"},{"key":"S0022481200049562_ref004","first-page":"87","volume-title":"Algebra and logic, Springer Lecture Notes","author":"Feferman"},{"key":"S0022481200049562_ref005","volume-title":"Notes on the formalization of Bishop's constructive mathematics","author":"Feferman","year":"1977"},{"key":"S0022481200049562_ref006","first-page":"315","volume":"38","author":"Friedman","year":"1973","journal-title":"The consistency of classical set theory relative to a set theory with intuitionistic logic"},{"key":"S0022481200049562_ref007","volume-title":"Springer Lecture Notes","author":"Troelstra"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200049562","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:57:30Z","timestamp":1558987050000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200049562\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978,6]]},"references-count":7,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1978,6]]}},"alternative-id":["S0022481200049562"],"URL":"https:\/\/doi.org\/10.2307\/2272820","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1978,6]]}}}