{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,11]],"date-time":"2024-01-11T03:21:25Z","timestamp":1704943285285},"reference-count":9,"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>This paper is devoted to the general question, which assertions \u03c6 have the property,<\/jats:p><jats:p>if \u03c6 is provable classically, then \u03c6 is<\/jats:p><jats:p>(*) provable constructively.<\/jats:p><jats:p>More generally, we consider the question, what is the \u201cconstructive content\u201d of a given classical proof? Our aim is to formulate rules in a form applicable to mathematical practice. Often a mathematician has the feeling that there will be no difficulty constructivizing a certain proof, only a number of routine details; although it can be quite laborious to set them all out. We believe that most such situations will come quite easily under the scope of the rules given here; the metamathematical machinery will then take care of the details.<\/jats:p><jats:p>This basic idea is not new; it has been discussed by G\u00f6del and by Kreisel. Kreisel's investigations [Kr] were based on Herbrand's theorem; in unpublished memoranda he has also used G\u00f6del's methods on some examples. These methods of G\u00f6del (the double-negation and Dialectica interpretations) lie at the root of our work here. Previous work, however, has been limited to traditional formal systems of number theory and analysis. It is only recently that formal systems adequate to formalize constructive mathematics as a whole have been developed. Thus, for the first time we are in a position to formulate logical theorems which are easily applicable to mathematical practice. It is this program which we here carry out.<\/jats:p><jats:p>Now that the work has been placed in some historical context, let us return to the main question: which \u03c6 have the property (*)? Upon first considering the problem, one might guess that any \u03c6 which makes no existential assertions (including disjunctions) should have the property (*).<\/jats:p>","DOI":"10.2307\/2272821","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:47:35Z","timestamp":1146952055000},"page":"228-246","source":"Crossref","is-referenced-by-count":13,"title":["Some relations between classical and constructive mathematics"],"prefix":"10.1017","volume":"43","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200049574_ref006","volume-title":"Notes on the formalization of Bishop's constructive analysis","author":"Feferman","year":"1977"},{"key":"S0022481200049574_ref005","first-page":"87","volume-title":"Algebra and logic, Springer Lecture Notes","author":"Feferman"},{"key":"S0022481200049574_ref008","volume-title":"Springer Lecture Notes","author":"Troelstra"},{"key":"S0022481200049574_ref009","volume-title":"Springer Lecture Notes","author":"Zucker"},{"key":"S0022481200049574_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":"S0022481200049574_ref002","unstructured":"Beeson M. , Continuity in intuitionistic set theories (to appear)."},{"key":"S0022481200049574_ref003","first-page":"213","volume":"43","author":"Beeson","year":"1978","journal-title":"A type-free G\u00f6del interpretation"},{"key":"S0022481200049574_ref007","first-page":"155","volume":"23","author":"Kreisel","year":"1958","journal-title":"The metamathematical significance of consistency proofs"},{"key":"S0022481200049574_ref004","volume-title":"Foundations of constructive analysis","author":"Bishop","year":"1967"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200049574","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:57:52Z","timestamp":1558987072000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200049574\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978,6]]},"references-count":9,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1978,6]]}},"alternative-id":["S0022481200049574"],"URL":"https:\/\/doi.org\/10.2307\/2272821","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1978,6]]}}}