Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-23T06:09:51.902Z Has data issue: false hasContentIssue false
  • English
  • Français

The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations

Published online by Cambridge University Press:  12 March 2014

Michael J. Beeson
Michael J. Beeson*
Affiliation:
University of Texas at Austin, Austin, Texas 78712
Get access Rights & Permissions [Opens in a new window]

Extract

The primary purpose of this work is to analyze the constructive interpretations of classical theorems concerning the continuity of effective operations. These theorems are the “recursivizations” of the statements that all functions (on various spaces) are continuous. To discuss the question whether these statements are constructively valid, it would be necessary to analyze the notion of “constructively valid,” which is beyond the scope of this paper. We now proceed to describe our results. We deal with two kinds of effective operations: (i) partial operations on indices of partial functions, and (ii) total operations on indices of total functions. The two principal theorems of the subject assert that each such operation is continuous; for (i) this is due to Myhill-Shepherdson [7] and called MS here; for (ii) it is due to Kreisel, Lacombe, and Shoenfield [5] and called KLS. (Explicit formulations of these and other principles mentioned in the introduction will be given in §1 below.)

Several interpretations (of, e.g., Heyting's arithmetic HA) in the literature satisfy Markov's principle MP, and for these MS and KLS are valid, since a close inspection of the classical proofs of MS and KLS shows that they are derivable in HA + MP. But we also find an interpretation in the literature under which MS and KLS are valid while MP is not (hence MS and KLS do not imply MP in systems for which this interpretation is sound). This work is in §2.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 40 , Issue 3 , September 1975 , pp. 321 - 346
Copyright
Copyright © Association for Symbolic Logic 1975

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

[1]Friedman, H., Realizability in intuitionistic logics, arithmetics, type theories, and set theories, Stanford University (mimeographed).Google Scholar
[2]Kreisel, G., Interpretation of analysis by means of constructive functional of finite types, Constructivity in mathematics (Proceedings of the Colloquium at Amsterdam 1957) (Heyting, , Editor), North-Holland, Amsterdam, 1959.Google Scholar
[3]Kreisel, G., Mathematical logic, Lectures on modern mathematics, vol. 3 (Saaty, T., Editor), Wiley, New York, 1965.Google Scholar
[4]Kreisel, G., On weak completeness of predicate logic, this Journal, vol. 27 (1962), pp. 139–158.Google Scholar
[5]Kreisel, G., Lacombe, and Shoenfield, J. R., Partial recursive functional and effective operations, Constructivity in mathematics (Proceedings of the Colloquium at Amsterdam 1957) (Heyting, , Editor), North-Holland, Amsterdam, 1959.Google Scholar
[6]Kreisel, G., Shoenfield, J. R. and Wang, Hao, Number theoretic concepts and recursive well-orderings, Archiv für matkematische Logik und Grundlagenforschung, vol. 5, pp. 42–64.CrossRefGoogle Scholar
[7]Myhill, J. and Shepherdson, J. C., Effective operations on partial recursive functions, Zeitschrift für matkematische Logik und Grundlagen der Mathematik (1955), No. 1, pp. 310–317.Google Scholar
[8]Rogers, H., Theory of recursive functions and effective computability, McGraw-Hill, New York, 1967.Google Scholar
[9]Spector, Clifford, Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Recursive Function Theory (Proceedings of Symposia in Pure Mathematics), vol. 5, American Mathematical Society, Providence, R.I., 1962.Google Scholar
[10]Troelstra, A. S., Notions of realizability for intuitionistic arithmetic and intuitionistic arithmetic in all finite types, Proceedings of the Second Scandinavian Logic Symposium (Fenstad, J. E., Editor), North-Holland, Amsterdam, 1971.Google Scholar
[11]Troelstra, A. S., Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.CrossRefGoogle Scholar