Skip to main content
SpringerLink
Log in

Axioms for Intuitionistic Mathematics Incompatible with Classical Logic

  • Chapter
Logic, Foundations of Mathematics, and Computability Theory

Part of the book series: The University of Western Ontario Series in Philosophy of Science ((WONS,volume 9))

Abstract

Standard formalizations of constructive mathematics (’constructive’ here in the narrow sense of Bishop (1967): choice sequences are regarded as inacceptable, and Church’s thesis is not assumed) can be carried out in formal systems based on intuitionistic logic which become classical formal systems on addition of the principle of the excluded third. The fact that in such systems for constructive mathematics the logical operations permit an interpretation different from the classical truth-functional one is then solely expressed by the fact that less axioms are assumed. As is well-known, this results in formal properties1 such as.

$$\begin{array}{l} \vdash A \vee B \Rightarrow {\rm{ }}{\mkern 1mu} \vdash A{\rm{ }}or \vdash B,\\ \vdash \exists xAx \Rightarrow \vdash At{\mkern 1mu} for{\rm{ }}some{\rm{ }}term{\rm{ }}t\left( {\exists xAx{\mkern 1mu} {\rm{ }}closed} \right). \end{array}$$

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  • Beeson, M. J.: 1972, Metamathematics of Constructive Theories of Effective Operations, Thesis, Stanford University. (See also Beeson, 1975.).

    Google Scholar 

  • Beeson, M. J.: 1975, ‘The Nonderivability in Intuitionistic Formal Systems of Theorems on the Continuity of Effective Operations’, Journ. Symbolic Logic 40, 321–346.

    Article  Google Scholar 

  • Beeson, M. J.: A,’ The Unprovability in Constructive formal Systems of the Continuity of Effective Operations on the Reals’. To appear.

    Google Scholar 

  • Beeson, M. J.: B, ‘Principles of Continuous Choice and Continuity of Functions in Formal Systems for Constructive Mathematics’. To appear.

    Google Scholar 

  • Bishop, E.: 1967, Foundations of Constructive Analysis, McGraw Hill, New York.

    Google Scholar 

  • Čeitin, G. S.: 1959, ‘Algorithmic Operators in Constructive Complete Separable Metric Spaces’ (Russian), Doklady Akad. Nauk 128, 49–52.

    Google Scholar 

  • Dalen, D. van: 1973, ‘Lectures on Intuitionism’, in A. R. D. Mathias, H. Rogers (eds.), Cambridge Summer School in Mathematical Logic, Springer-Verlag, Berlin, pp. 1–94.

    Chapter  Google Scholar 

  • Dalen, D. van: 1974A, ‘Choice Sequences in Beth models’, Notes on Logic and Computer Science 20, Dept. of Mathematics, Rijksuniversiteit, Utrecht (The Netherlands). Revised in ‘An Interpretation of Intuitionistic Analysis’, to appear in Annals of Math. Logic.

    Google Scholar 

  • Dalen, D. van: 1975, ‘Experiments in Lawlessness’, Notes on Logic and Computer Science 28, Dept. of Mathematics, Rijksuniversiteit, Utrecht (The Netherlands). Revised in ‘An Interpretation of Intuitionistic Analysis’, to appear in Annals of Math. Logic.

    Google Scholar 

  • Dalen, D. van: 1975A, ‘The Use of Kripke’s Schema as a Reduction Principle’, Preprint 11, Dept. of Mathematics, University of Utrecht.

    Google Scholar 

  • Dragalin, A. G.: 1973, ‘Constructive Mathematics and Models of Intuitionistic Theories’, in P. Suppes, L. Henkin, Gr. C. Moisil, A. Joja (eds.), Logic, Methodology and Philosophy of Science IV, North-Holland Publ. Co., Amsterdam, 111–128.

    Google Scholar 

  • Friedman, H.: 1975, ‘Set Theoretic Foundations for Constructive Analysis and the Hilbert Program’, Manuscript, Dept. of Mathematics, State University of New York at Buffalo, Buffalo, N.Y.

    Google Scholar 

  • Jongh, D. H. J. de and Smorynski, C. A.: 1974, ‘Kripke Models and the Theory of Species’ Report 74-03, Dept. of Mathematics, Univ. of Amsterdam. Appeared in: Annals of Mathematical Logic 9 (1976), 157–186.

    Article  Google Scholar 

  • Kleene, S. C: 1965, ‘Logical Calculus and Realizability’, Acta Philosophica Fennica 18, 71–80.

    Google Scholar 

  • Kleene, S. C. and Vesley, R. E.: 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, North-Holland Publ. Co., Amsterdam.

    Google Scholar 

  • Kreisel, G.: 1968, ‘Lawless Sequences of Natural Numbers’, Compositio Math. 20, 222–248.

    Google Scholar 

  • Kreisel, G.: 1971, ‘A Survey of Proof Theory II’, in J.-E. Fenstad (ed.) Proceedings of the Second Scandinavian Logic Symposium, North-Holland Publ. Co., Amsterdam, pp. 109–170.

    Chapter  Google Scholar 

  • Kreisel, G.: 1972, ‘Which Number-Theoretic Problems can be Solved in Recursive Progressions on Paths Through 0?’, J. Symbolic Logic 37, 311–344.

    Article  Google Scholar 

  • Kreisel, G. and Troelstra, A. S.: 1970, ‘Formal Systems for Some Branches of Intuitionistic Analysis’, Annals of Math. Logic 1, 229–387.

    Article  Google Scholar 

  • Moschovakis, J. R.: 1973, ‘A Topological Interpretation of Second-order Intuitionistic Arithmetic’, Compositio Math. 26, 261–275.

    Google Scholar 

  • Moschovakis, Y. N.: 1964, ‘Recursive Metric Spaces’, Fund. Math. 55, 215–238.

    Google Scholar 

  • Orevkov, V. P.: 1963, ‘A Constructive Map of the Square into itself, which Moves every Constructive Point’ (Russian), Doklady Akad. Nauk SSSR 152, 55–58; translated in Soviet Mathematics 4 (1963), 1253-1256.

    Google Scholar 

  • Orevkov, V. P.: 1964, ‘On Constructive Mappings of a Circle into itself (Russian)’, Trudy Mat. Inst. Steklov 72, pp. 437–461; translated in Translations AMS 100, 69-100.

    Google Scholar 

  • Troelstra, A. S.: 1969, Principles of Intuitionism, Springer-Verlag, Berlin.

    Google Scholar 

  • Troelstra, A. S. (ed.): 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer-Verlag, Berlin.

    Google Scholar 

  • Troelstra, A. S.: 1973A, ‘Notes on Intuitionistic Second-Order Arithmetic’, in A. R. D. Mathias, H. Rogers (eds.), Cambridge Summer School in Mathematical Logic, Springer-Verlag, Berlin, 171–205.

    Chapter  Google Scholar 

  • Troelstra, A. S.: 1976, Choice Sequences, a Chapter of Intuitionistic Mathematics, Oxford University Press, Oxford. To appear.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematical Institute, University of Amsterdam, The Netherlands

    A. S. Troelstra

Authors
  1. A. S. Troelstra
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. The University of Western Ontario, Canada

    Robert E. Butts

  2. The Academy of Finland and Stanford University, USA

    Jaakko Hintikka

Rights and permissions

Reprints and permissions

Copyright information

© 1977 D. Reidel Publishing Company, Dordrecht, Holland

About this chapter

Cite this chapter

Troelstra, A.S. (1977). Axioms for Intuitionistic Mathematics Incompatible with Classical Logic. In: Butts, R.E., Hintikka, J. (eds) Logic, Foundations of Mathematics, and Computability Theory. The University of Western Ontario Series in Philosophy of Science, vol 9. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-1138-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-94-010-1138-9_4

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-94-010-1140-2

  • Online ISBN: 978-94-010-1138-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation