Abstract
This paper discusses Michael Dummett’s attempt to base the use of intuitionistic logic in mathematics on a proof-conditional semantics. This project is shown to face significant obstacles resulting from the existence of variants of standard intuitionistic logic. In order to overcome these obstacles, Dummett and his followers must give an intuitionistically acceptable completeness proof for intuitionistic logic relative to the BHK interpretation of the logical constants, but there are reasons to doubt that such a proof is possible. The paper concludes by proposing an alternative way of thinking about why one should use intuitionistic logic when doing mathematics.
Similar content being viewed by others
Notes
The term ‘constructive mathematics’ is ambiguous. In this paper, it will be used to refer to any approach to mathematics that makes use of intuitionistic logic. So understood, constructive mathematics might be motivated by a view that mathematical objects are constructed in some sense, but it does not have to be. In the last section of this paper, we will examine the relationship between traditional constructivist ontologies and the use of intuitionistic logic in mathematics.
The acronym contains the initials of Brouwer, Heyting, and the Russian mathematician Andrei Kolmogorov. Brouwer himself never explicitly articulated anything like the BHK interpretation, but Heyting’s work on logic was initially an attempt to formalize the reasoning characteristic of his teacher’s intuitionistic mathematics. Kolmogorov had presented something similar to Heyting’s semantics a little earlier in Kolmogorov (1932).
See Dummett (1975) for a well known presentation of it.
Constructivists reject the full-strength Axiom of Choice, but not on grounds of intuitive clarity. Rather, the problem with the axiom for constructivists is that it entails the validity of the LEM.
Heyting, who tends to be more ecumenical and pragmatic, may be open to holistic justifications, but he does not appeal to them in his arguments for various logical laws.
We have modified the notation in this passage to conform to our standards rather than the ones that Heyting uses in his book.
Elsewhere (Dummett 1991, p. 295), Dummett suggests taking absurdity to be equivalent to the conjunction of every atomic sentence of the language. The problem with this is that, in a suitably restricted mathematical language, this conjunction will not always be absurd. For instance, if our language contains only symbols for equality and the number 1, then the only atomic formula is ‘\(1=1\)’, which is not absurd. The reason why the maximal atomic conjunction is absurd in the language of ordinary arithmetic is because we know in advance that, say, 1 is not 2, so including ‘\(1=2\)’ as a conjunct makes the whole conjunction false. The point is that this will not allows us to avoid smuggling negation back into our understanding of absurdity. See Cook and Cogburn (2000) for more on this.
Dummett describes some of these formal systems in Dummett (2000, ch. 4).
For this reason, it is a bit of a distortion to present Heyting as a precursor to Dummett, as we have done in this paper. Our reason for introducing this distortion earlier was to emphasize that the BHK interpretation has been taken to be an important part of constructive mathematics even before Dummett, even though he more than anybody else has been responsible for tying the mathematics to a particular theory of meaning.
Other parts of Brouwer’s work, such as the theory of choice sequences, call for non-logical explications. Troelstra, in particular, has done much to carry out this sort of explication in Troelstra (1977) and elsewhere.
This is reflected in the sequence of topics in Dummett’s Elements of Intuitionism, which begins with a discussion of the meanings of the logical constants and proceeds to a chapter on intuitionistic logic before turning to the mathematics itself.
This claim is based on the author’s personal experience and conversations with other non-Dummettian proponents of constructive mathematics.
References
Chagrov, A., & Zakharyaschev, M. (1991). The disjunction property of intermediate propositional logics. Studia Logica, 50, 189–216.
Cook, R. T. (2014). Should anti-realists be anti-realists about anti-realism? Erkenntnis, 79(2), 233–258.
Cook, R. T. & Cogburn, J. (2000). What negation is not: Intuitionism and ‘0=1’. Analysis, 60, 5–12.
Dummett, M. (1975). The philosophical basis of intuitionistic logic. In H. E. Rose & J. C. Shepherdson (Eds.), Logic Colloquium ′73 (pp. 5–40). North-Holland. [Reprinted in Dummett, M. (1975). Truth and Other Enigmas 215–247, Harvard University Press].
Dummett, M. (1991). The logical basis of metaphysics. Cambridge: Harvard University Press.
Dummett, M. (2000). Elements of intuitionism (2nd ed.). Oxford: Clarendon Press.
Goodman, N. (1970). A theory of constructions is equivalent to arithmetic. In J. Myhill, A. Kino, & R. Vesley (Eds.), Intuitionism and proof theory (pp. 101–120). Amsterdam: North-Holland.
Haack, S. (1996). Deviant logic, fuzzy logic: Beyond the formalism. Chicago: University of Chicago Press.
Heyting, A. (1930) Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussischen Akademie von Wissenschaften, 9, 42–56, 57–71, 158–169.
Heyting, A. (1931). Die intuitionistische Grundlegung der Mathematik. Erkenntnis, 2, 106–115. [English translation in Benacerraf, P., & Putnam, H. (Eds.) (1983). Philosophy of Mathematics: Selected Readings, 2nd edn. 52–61. Cambridge University Press].
Heyting, A. (1934). Mathematische Grundlagenforschung: Intuitionismus, Beweistheorie. Berlin: Springer.
Heyting, A. (1966). Intuitionism: An introduction (2nd ed.). Amsterdam: North-Holland.
Kleene, S. (1945). On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10(4), 109–124.
Kolmogorov, A. N. (1932). Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35, 58–65.
Kreisel, G. (1962). Foundations of intuitionistic logic. In E. Nagel, P. Suppes, & A. Tarski (Eds.), Logic, methodology and philosophy of science. Proceedings of the 1960 International Congress (pp. 198–210). Stanford: Stanford University Press.
Quine, W. V. (1960). Word and Object. Cambridge: MIT Press.
Rose, G. (1953). Propositional calculus and realizability. Transactions of the American Mathematical Society, 75, 1–19.
Shapiro, S. (2009). We hold these truths to be self-evident: But what do we mean by that? Review of Symbolic Logic, 2(1), 175–207.
Tennant, N. (1987). Anti-realism and logic. Oxford: Clarendon Press.
Troelstra, A. S. (1977). Choice sequences: A chapter of intuitionistic mathematics. Oxford: Clarendon Press.
Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics. Amsterdam: North-Holland.
Acknowledgments
Earlier versions of this paper were presented at California State University, San Bernardino and the University of Western Ontario. The author is grateful to the philosophy departments at those institutions for useful discussions. Thanks are also due to two anonymous reviewers, Matt Carlson, David Fisher, Gary Ebbs, Neil Tennant, and especially Charles McCarty for fruitful feedback.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Koss, M.R. Some Obstacles Facing a Semantic Foundation for Constructive Mathematics. Erkenn 80, 1055–1068 (2015). https://doi.org/10.1007/s10670-014-9697-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10670-014-9697-7