Confessions of a formalist, Platonist intuitionist

April 9, 1994
1. Algebraists

All algebraists are formalists---it comes with the territory. Analysts are grounded in the real numbers, and when they get a little abstract they are accused of being soft. Geometers and topologists have their pictures. But algebraists simply posit a few uninterpreted finitary operations, and some equations, and they are off and running.

Algebra is the mathematics of mathematics. Just as it's perfectly acceptable to be a little weak in mathematics, so it is okay for a mathematician to be a little weak in algebra. "After that (the interesting part) it's just algebra (which we won't do because it's boring dog-work that only a nerd would enjoy)." Am I confusing high school algebra with modern algebra? The unifying theme is the formal manipulation of symbols with an attenuated sense of what they stand for.

It is no surprise that I, a born algebraist---brought into the mathematical world by no less than Irving Kaplansky---should be a formalist at heart. What is surprising is that I should be aware of this state of affairs. Real mathematicians aren't interested in foundations.

I've always been interested in foundations, despite the fact that I share the average mathematician's contempt for the subject (it's all very well if you like that sort of thing). Paul Halmos told me that my problem was that I had been exposed to a very good logician at an early age: I took a year's course from Alonzo Church as an undergraduate. I went to the University of Chicago in the hopes of studying algebraic logic under Halmos, but it turned out that his real interests were measure theory, ergodic theory, and operators on Hilbert spaces. Yuck!

Nonetheless, Halmos remained my mentor and I chose information theory and Boolean algebra as my two topics for the examination that served as prelims at that time (the masters exam played the role of comprehensives). Partly on this basis I inherited a PhD student in information theory early in my career---his adviser was denied tenure because he had not quite managed to write up his own dissertation yet. We sent the student's draft of his dissertation to an expert in the field, who said the main theorem was too trivial. In fact, it turned out to be incorrect! Although this sounds like the stuff of a joke---"not only is this result obvious but it's not true"---I think it was probably an accurate appraisal. We managed to formulate a more interesting theorem along the same lines, which might even have been true.

Halmos left Chicago and me for Michigan. My first contact with Kap was when he was serving as chairman. He said he would give me as good a recommendation as possible to another university. Well, don't we all periodically try to clear out the dead wood among our graduate students? But it turned out that I was very good at taking Graduate Record Examinations; and as Kap sadly informed me, the people responsible for handing out NSF Cooperative Fellowships are unduly impressed by those scores. So the department, not wishing to forego a university-wide award, let me continue.

Imagine Kap's surprise when one day I informed him that algebra was my first love and that I would like to work in commutative rings! The words "this is so sudden" stick in my mind. I don't know when he accepted me as a student, if ever, but at some point he gave me a problem that I could do.

In the spring of 1963 I got a call from Ralph Crouch, who was visiting Scott-Foresman in Chicago, asking me if I would like a position at New Mexico State University that fall. I told him that I wouldn't be getting out by then, to which he replied, "Yes you will." You can't refuse an offer like that. Recruiting expenses: one 7-Up from a machine. Agonizing faculty debate about who to hire: none. The good old days.

The algebra at New Mexico State University was abelian groups. I'm a team player so I joined the gang. They probably thought that a student of Kaplansky's would know some abelian group theory, but in fact I had never read his famous little red book. I've often thought that, as an abelian group theorist, I am a student of John Irwin's. Certainly he introduced me to the subject, and, looking back on it, I wrote my abelian groups dissertation under his direction that first year at NMSU. Unlike Kap, he suggested I turn it into a joint paper.

2. A Platonist in trouble

What about foundations? The theory of torsion abelian groups, which is what was hot at NMSU, is really quite far out. Every modern algebra student learns the story for finite ones, and the countable ones were completely classified in the thirties. So current research had to deal with uncountable groups, and the problems were intimately tied up with cardinality. Moreover, the centerpiece of the subject, the classification theorem for countable torsion abelian groups, cannot even be stated without ordinal numbers. If you study torsion abelian groups, cardinal and ordinal numbers are part of your everyday life---transfinite constructions are your bread and butter.

Who can understand the first uncountable ordinal, let alone some of the more exotic creatures that live further down the line? And what about things like free ultrafilters? I remember realizing at one point that I didn't understand big ordinals---had no real feeling for them at all---although I could certainly prove theorems about them. The formalist was doing fine, but the Platonist was in trouble.

We are all Platonists, aren't we? In the trenches, I mean---when the chips are down. Yes, Virginia, there really are circles, triangles, numbers, continuous functions, and all the rest. Well, maybe not free ultrafilters. Is it important to believe in the existence of free ultrafilters? Surely that's not required of a Platonist. I can more easily imagine it as a test of sanity: "He believes in free ultrafilters, but he seems harmless."

3. Constructive mathematics and recursive function theory

When I returned to New Mexico State from a sabbatical leave at Florida Atlantic University, people there were talking about Errett Bishop's book Foundations of constructive analysis. Stanley Tennenbaum had visited the previous semester and conducted a very popular seminar on the subject. It reminded me of how Church would talk about effective processes, and of the two-quarter course in recursive function theory that I sat in on at the University of Chicago.

In a spur-of-the-moment comment to Mark Mandelkern, I likened the logicians who kept alive the notion of an effective process to the monks who kept learning alive in the dark ages. I guess my thought was that Bishop had recognized the importance of finite procedures after a long period in which they were neglected; but even during that time, the logicians, with no support from the rest of the mathematical community, nurtured the idea. Of course no real mathematician thinks that logicians do anything that is worthwhile, and constructive mathematicians are real mathematicians (at least we think we are).

Mark's instant dismissal of this analogy was my first hint of the conflict between the world-views of constructive mathematicians of the Bishop stripe, and mathematicians who approach constructivity through recursive function theory. You would think that the two groups would constantly be exchanging ideas, but the truth is that neither group thinks it has much to learn from the other. Recursive function theorists think that constructive mathematicians are hopelessly imprecise. Constructive mathematicians consider recursive function theory, in the context of classical logic, to be nonconstructive---and artificially limiting.

The much touted equivalence of Turing machines, recursive functions, and Markov algorithms presumably settled once and for all the precise definition of "computable." Bishop claimed, to the contrary, that if you had a constructive proof that a Turing machine halted and produced the desired result, then you didn't need the Turing machine in the first place; and in the absence of such a proof, the Turing machine didn't establish computability.

Kleene showed how to model intuitionistic logic with recursive functions, so there is a sense in which constructive mathematicians could be talking about recursive functions. But that misses the point of constructive mathematics, which is to do mathematics itself. I like to make the distinction between a theory of constructive X's, and a constructive theory of X's. If you want to create a theory of constructive functions, then you might well invent Turing machines---there are functions, among which are the ones computable by a Turing machine. But if you want to create a constructive theory of functions, if you want to study all functions from a constructive point of view, then you will not try to identify a class of constructive functions to study; rather you will develop constructive techniques for dealing with any kind of object: you will invent something like intuitionistic logic.

4. Different subject matter?

Are constructive mathematicians talking about the same things as other mathematicians? Do I mean the same thing by "real number" as they do? There are people in both camps who insist that we mean different things---perhaps every classical mathematician takes that position. To those in possession of the truth there are no genuine alternative views, so any apparent disagreement must be ascribed to error or to difference in meaning. The classical mathematician is inclined to think that I am talking about something different, while I tend to favor the idea that he is in error.

As a concrete example of a difference in ontology the classical mathematician may point to something like the Specker sequence: a bounded, primitive recursive, ascending sequence of rational numbers that is eventually bounded away from any given computable real number. He will say that this sequence converges to a noncomputable real number---part of his universe, not part of mine. So---the argument goes---if I say that something is true for all real numbers, I am not including the Specker number in the range of my quantifier, whence I am saying something different.

Of course I never said that I was ruling out the Specker number. I simply deny that my classical colleague has given a valid proof of the existence of a number that is the supremum of the Specker sequence; but, if such a number exists, then it is in the range of my quantifier. Let n be the smallest degree of a polynomial that shows that pi and e are algebraically dependent, if any (this hasn't been resolved yet, has it?). Does this number, if it happens to exist, fail to be in the domain of my colleague's quantifiers just because he does not know a proof of the existence of such a number?

There is a bit of a misunderstanding here that I may have swept under the rug. Because the Specker sequence is eventually bounded away from any given computable real number, my classical colleague believes that it is absurd for me to think that it could exist. After all, I'm supposed to believe only in computable real numbers. By "computable" I understand "Turing-computable," so the proposition that all real numbers are computable is, in the context of constructive mathematics, Church's thesis. Constructive mathematics with Church's thesis is another ballgame---in effect, constructive recursive function theory. I don't say that the Specker number doesn't exist because it's not computable; all I say is that the alleged proof of the existence of the Specker number, which relies essentially on the least upper bound principle, is not valid.

My constructive colleague is more likely to point to the characteristic function of the rational numbers as an example of an object that exists for the classical mathematician but not for us. We all pretty much agree on the existence of the set of pairs (x,n) such that x is rational and n is one, or x is irrational and n is zero. The question is whether or not this defines a function. To show that, one invokes the law of excluded middle: every real number is either rational or irrational. Constructive mathematicians do not rule out the possibility that this might be a function---although Brouwer did---but they do not expect ever to prove that it is. If it were excluded from the range of our quantifiers, we could reasonably expect to be able to prove that there does not exist a function that takes the value one on the rationals and zero on the irrationals. We cannot.

5. Intuitionistic logic

Because constructive mathematics is based on intuitionistic logic, many mathematicians consider it to be a part of logic. These same people generally do not consider their own mathematics to be a part of logic, although ordinary mathematics is based on classical logic in exactly the same way. The underlying logic in either case is taken for granted. However, when passing from one view to the other, one becomes conscious of the difference in logics, and hence of logic itself. In the brave new mathematical world where people are raised as constructivists---"one great constructive nation, with everyone engaged in computation," as Bishop put it---appeal to the law of excluded middle will brand you as a logician.

Why is classical existence unproblematic while constructive existence needs to be explained in terms of it? I would think that the people who believe that there exists a well ordering of the real numbers would have the explaining to do.

Does a Platonist have to believe in the law of excluded middle? Think of a sequence of zeros and ones, say generated by a primitive recursive function. I believe I know what it means for the sequence to consist of all zeros. I had better, because the intuitionistic explanation of "for all" does not clarify anything here: to verify "for all n, f(n)," produce a method that, for every object n, yields a verification of the proposition f(n). Computing f(n) is already such a method. (There is another phrase that is added to avoid this problem---something like "and we know it works")

Bishop formulates it in terms of predictions: one predicts that each term in the sequence will be a zero. Does this differ from a realist or Platonist position? We are talking about truth conditions for the statement even though we cannot verify them all directly (by checking the terms one-by-one and seeing that they are indeed all zero). Perhaps the distinction between potential infinity and actual infinity is surfacing here---more about that later.

I also think that I know what it means for a one to appear somewhere in the sequence---in this case the truth condition and the verification condition are the same. So here I am, believing in the objective existence of numbers, and thinking in terms of truth, not verification. Am I committed to the proposition that either the terms are all zeros, or some term is a one? This strikes me as a separate issue.

6. Formalism

How do we tell whether something is a piece of constructive mathematics? Take somebody who could be expected to recognize a piece of constructive mathematics, and see if he thinks the work is constructive. Now I contend that he will judge the work constructive exactly when it uses only intuitionistic logic. An implicit appeal to the law of excluded middle will automatically disqualify it, while if it is free of such appeals, it will be accepted. The practical and the formal criteria coincide. There is no need for an analysis of ontology, for algorithms and finite procedures, for the phrase "and you can tell which." Such considerations may be involved in one's choice to eschew the law of excluded middle, but they are not involved in the mathematics as such. Beautiful!

I am just an informal formalist---serious formalists start out by deciding what symbols they are going to use. Nevertheless, the spirit is the same in that the emphasis is on form rather than substance. How shallow that sounds! But formalism is the big tent under which we can all work, the mechanism by which we can communicate, and the embodiment of our most characteristic activity: abstraction.