INTUITIONISM AS GENERALIZATION

Philosophia Mathematica, 5(1990), 124--128

I was inspired, not to say provoked, to write this note by Michel J. Blais's article A pragmatic analysis of mathematical realism and intuitionism [2]. Having spent the greater part of my career doing intuitionistic mathematics, while continuing to do classical mathematics, I have come to feel that most comparisons of these two approaches to mathematics miss the essential point: intuitionism, in its simplest form, is a generalization of classical mathematics that accomodates both classical and computational models.

By intuitionism I mean the approach to mathematics based on intuitionistic logic, a well-defined body of axioms and rules of inference [6] [3]. So, for example, my idea of intuitionism does not include the notion of a choice sequence [8], or the various continuity principles associated with intuitionism [9], and it does not refer to the more bizarre consequences that have been drawn from Brouwer's idea of a creating subject [3]. This lean version of intuitionistic mathematics is usually called constructive mathematics. Blais directs his comments in [2] at constructive mathematics rather than at the more esoteric varieties of intuitionistic mathematics.

Most analyses dwell on the relative merits of classical and computational models, despite the fact that constructive mathematics, viewed as a theory rather than as a description of a universe, can be interpreted as speaking about either model. Other flavors of intuitionistic mathematics incorporate axioms that hold only in computational models. For example, Brouwer proved that every totally defined function on the real line is continuous. A theory where this is provable cannot refer to the classical universe, so we have to consider whether we like its models better than the classical model. But any theorem in constructive mathematics is a theorem in classical mathematics, so in this case it is not a question of choosing between models, but of deciding whether it is worthwhile to talk about computational models in addition to the classical model.

By comparing mathematical realism with intuitionism from an informal axiomatic point of view, we can steer clear of most of the metaphysical problems involved in analyzing these notions from the ground up, and concentrate on what may be termed the purely mathematical aspects. In particular we won't have to consider whether intuitionists hold that a theorem "isn't true until it's known to be true", as Blais states [2; p.67]. I am inclined to think that the intuitionist's view is, rather, that you are not entitled to assert that a theorem is true until it's proved, which sounds much like a realist's view also.

It is important to be aware, as background, that a substantial body of mathematics has recently been developed along intuitionistic lines [1] [7]. The scope and depth of this work gives the lie to the misconception of mathematics outside of the realist framework as some sort of crippled stepchild. Any analysis of realism versus intuitionism in mathematics, that desires to say something relevant to mathematical practice, should be informed by this corpus of applied intuitionism.

We may distinguish two types of axiomatic theories, characterizing them by their intent. In the first type, exemplified by Euclidean geometry, arithmetic, and set theory, there is a single intended interpretation, a standard model. The existence of nonstandard models, which is guaranteed by Gödel's results, is an imperfection---we had hoped to give an axiomatic characterization of a mathematical structure, starting with some self-evident truths about it. In the second type of axiomatic theory, exemplified by group theory and point-set topology, the purpose and power of theory lie in the large number of intended models.

The current trend is to treat set theory as a type-2 axiomatic system rather than one of type 1. Set theory is now thought of as more like group theory: we acknowledge the fact that there are many different models of the axioms, many worlds. No agreement has been achieved on the axioms of set theory beyond the Zermelo-Fraenkel axioms, and the axiom of choice. On the other hand, this combination, ZFC, is almost universally taken as the foundation of mathematics; it is the closest we have to a common intuition of what sets are. Other set-theoretic axioms, such as the continuum hypothesis, are added in much the same way that the commutative law is added to group theory: to investigate those worlds in which they hold.

What are the criteria for choosing among axiom systems? Generally there are two opposing criteria: interesting models and beautiful theorems. A tension derives from the fact that in strong theories you can prove lots of theorems about very few models, while weak theories have lots of models but few theorems. Groups are the algebraic systems that satisfy the axioms of group theory. Mathematicians study the consequences of the axioms of group theory, partly because there are many interesting groups, and partly because they can prove beautiful and useful theorems.

The choice of logical axioms is analogous to the choice of nonlogical axioms such as those of set theory or group theory. If we have fewer logical axioms, we will have more models of our theory. The main reason we do intuitionistic mathematics is so that our theorems will hold for computational models. We need not specify exactly what we mean by a "computational model" to see some of the consequences of this requirement. The statement that if amn is a doubly indexed sequence of integers, then there is a function f such that f(m) = 0 if amn = 0 for all n, and f(m) = 1 if amn ¹ 0 for some n, is false in any reasonable computational model. In the standard (realist) computational model, it asserts the solvability of the halting problem, which is well known to be unsolvable. But even knowing nothing about the standard computational model, it is implausible that we could compute the function f because we may need to examine each of the infinitely many terms am1,am2,... to compute f(m).

We construct the function f above as follows. Given m, either there exists n such that amn¹ 0, in which case we define f(m) = 1, or amn = 0 for all n, in which case we define f(m) = 0. This is a fairly straightforward application of the law of excluded middle (LEM). So to admit computational models, we must reject the universal applicability of LEM. As classical logic is intuitionistic logic together with LEM, the relation between the two theories is quite clear. We can prove more theorems with LEM than without, but our theorems will not have the numerical content provided by the computational models if we use LEM to prove them.

Blais refers to the "greater generality" of realist mathematics [2; p.69]; in fact, just the opposite is true. Because intuitionistic mathematics is the weaker theory, its theorems have more models, so they are more general---a theorem that holds for all groups is more general than one holding only for abelian groups. It is, of course, harder to prove more general theorems. The talk about a realist mathematician's finding intuitionistic logic "an unacceptable restriction upon the freedom necessary for his activity" [2; p.69] should be compared with an abelian group theorist rejecting group theory because he thinks that he should have the freedom to employ the rule ab = ba.

Blais [2; p.74] says that intuitionists hold that "nothing is truly mathematical unless it is effectively constructive." I'm not sure what that means, but it seems to conflict with the fact that any realist proof of a statement A, not using the axiom of choice, is an intuitionistic proof of LEM® A; and, as AC®LEM is a theorem of intuitionistic mathematics [5], any realist proof of A is an intuitionistic proof of AC® A. It is a common misconception that intuitionistic mathematics deals with a special class of mathematical objects that are, in some sense, constructive. Part of the reason for this is the way intuitionists try to explain what they are doing. Another is that in the most well-known realist model of intuitionistic mathematics, all functions are recursive. But when an intuitionist does group theory, he is developing a constructive theory of groups, not a theory of constructive groups.

Intuitionistic analysis, unlike recursive analysis, is not the study of constructive functions of constructive real numbers. If it were, then we could plausibly think of realist analysis as being more general, since it would deal with a broader class of objects; and we would chafe at the limitations of intuitionistic analysis. But any theorem in intuitionistic analysis is a theorem in realist analysis, interpreted in terms of realist functions of realist real numbers; and an intuitionistic proof is an acceptable proof to a realist mathematician, although he may not understand why some of the moves are made. There is no need to find a broader perspective, such as pragmatism, to reconcile the conflicts between realist and intuitionistic mathematics; intuitionistic mathematics is that broader perspective.

That "the realist mathematician recognizes the superiority of a constructive proof over a pure existence proof", as claimed by Blais [2; p.69], is simply false in my experience. Some mathematicians prefer to have an algorithm with their proof, but most find a pure existence proof more elegant. Even those who like algorithms have remarkably little appreciation of the thoroughgoing algorithmic thinking that is required for a constructive proof. This is illustrated by the nonconstructive nature of many proofs in books on numerical analysis, the theoretical study of practical numerical algorithms. I would guess that most realist mathematicians are unable even to recognize when a proof is constructive in the intuitionist's sense.

It is a lot harder than one might think to recognize when a theorem depends on a nonconstructive argument. One reason is that proofs are rarely self-contained, but depend on other theorems whose proofs depend on still other theorems. These other theorems have often been internalized to such an extent that we are not aware whether or not nonconstructive arguments have been used, or must be used, in their proofs. Another reason is that the law of excluded middle is so ingrained in our thinking that we do not distinguish between different formulations of a theorem that are trivially equivalent given LEM, although one formulation may have a constructive proof and the other not.

Blais suggests that the realist mathematician continue "production of pure existence proofs of the (a) type, if accompanied by specific recognition that the results are interim only, and not final" [2; p.77]. But this would concede the argument to the intuitionist, whose only real requirement is that the use of the law of excluded middle be recognized and recorded. Once this is done, the game is being played according to intuitionist rules. It is then simply a matter of taste as to how much we like theorems of the form LEM® A, and this issue is somewhat predecided, given the mathematician's predilection for generality and elegance.

The issue here is LEM, not realism. The conventional wisdom seems to be that the law of excluded middle is a necessary consequence of a realistic view of mathematics, but I have never seen an argument advanced for this point of view that does not assume that the law of excluded middle is part and parcel of a realistic view.

References

[1]
Bishop, Errett and Douglas S. Bridges, Constructive analysis, Springer-Verlag 1985

[2]
Blais, Michel J., A pragmatic analysis of mathematical realism and intuitionism, Philosophia Mathematica 4(1989) 61--85

[3]
Bridges, Douglas S. and Fred Richman, Varieties of constructive mathematics, London Math. Soc. Lecture Notes Series 97, Cambridge University Press 1987

[4]
Brouwer, L.E.J., Cambridge lectures on intuitionism, edited by D. van Dalen, Cambridge University Press 1981

[5]
Goodman, N.D. and J. Myhill, Choice implies excluded middle, Z. Math. Logik Grund. Math. 23(1978) 461

[6]
Heyting, A. Intuitionism, North-Holland 1971

[7]
Mines, R., F. Richman and W. Ruitenburg, A course in constructive algebra, Springer-Verlag 1988

[8]
Troelstra, A.S., Choice sequences, a chapter of intuitionistic mathematics, Clarendon Press, Oxford 1977

[9]
__________, Aspects of constructive mathematics, Mathematical logic, edited by Jon Barwise, North-Holland 1977

This document was translated from LATEX by HEVEA.