{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T16:26:33Z","timestamp":1767198393367,"version":"build-2238731810"},"reference-count":5,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":13890,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1976,3]]},"abstract":"<jats:p>\n                    The question of continuity of functions defined on Baire space\n                    <jats:italic>\n                      N\n                      <jats:sup>N<\/jats:sup>\n                    <\/jats:italic>\n                    or on the reals has been of great interest to constructivists. We have little hope of answering the question without a fundamental philosophical analysis of the notion of constructive function. However, one can ask whether the continuity of functions can be derived in known intuitionistic formal systems, and answer these questions by mathematical means.\n                  <\/jats:p>\n                  <jats:p>\n                    The constructivist does not generally wish to restrict himself to reals (or members of\n                    <jats:italic>\n                      N\n                      <jats:sup>N<\/jats:sup>\n                    <\/jats:italic>\n                    ) given by a recursive law; therefore the most natural formal systems have variables for reals, sequences and functions. The axioms of these systems turn out to be compatible with the assumption that every real or sequence is given by a recursive law, and every function by an effective operation. An underivability result, therefore, is only strengthened if this assumption is taken as an axiom; and once this is done, we may as well work with (indices of) effective operations, within arithmetic.\n                  <\/jats:p>\n                  <jats:p>\n                    By KLS is meant the assertion that each effective operation on Baire space\n                    <jats:italic>\n                      N\n                      <jats:sup>N<\/jats:sup>\n                    <\/jats:italic>\n                    is continuous. In [B1] it is shown that this statement cannot be proved in various intuitionistic formal systems. The continuity of functions on the reals has been of even greater interest to constructivists than the continuity of functions on\n                    <jats:italic>\n                      N\n                      <jats:sub>N<\/jats:sub>\n                    <\/jats:italic>\n                    ; by KLS(\n                    <jats:italic>R<\/jats:italic>\n                    ) is meant the assertion that each effective operation from the real numbers\n                    <jats:italic>R<\/jats:italic>\n                    to\n                    <jats:italic>R<\/jats:italic>\n                    is continuous. It is the purpose of the present note to show that KLS(\n                    <jats:italic>R<\/jats:italic>\n                    ) is also underivable in intuitionistic formal systems.\n                  <\/jats:p>","DOI":"10.2307\/2272940","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T17:40:11Z","timestamp":1146937211000},"page":"18-24","source":"Crossref","is-referenced-by-count":4,"title":["The unprovability in intuitionistic formal systems of the continuity of effective operations on the reals"],"prefix":"10.1017","volume":"41","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200051707_bib005","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"Troelstra","year":"1971"},{"key":"S0022481200051707_bib003","volume-title":"Foundations of constructive analysis","author":"Bishop","year":"1967"},{"key":"S0022481200051707_bib004","first-page":"1250","article-title":"Remarques sur les op\u00e9rateurs recursifs et sur les fonctions recursives d'une variable r\u00e9elle","volume":"241","author":"Lacombe","journal-title":"Comptes Rendus"},{"key":"S0022481200051707_bib002","volume":"40","author":"Beeson","year":"1975","journal-title":"Derived rules of inference related to the continuity of effective operations"},{"key":"S0022481200051707_bib001","first-page":"321","volume":"40","author":"Beeson","year":"1975","journal-title":"The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200051707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,22]],"date-time":"2023-03-22T06:41:52Z","timestamp":1679467312000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200051707\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1976,3]]},"references-count":5,"aliases":["10.1017\/s0022481200051707"],"journal-issue":{"issue":"1","published-print":{"date-parts":[[1976,3]]}},"alternative-id":["S0022481200051707"],"URL":"https:\/\/doi.org\/10.2307\/2272940","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1976,3]]}}}