Interview with a constructive mathematician

Fred Richman
Florida Atlantic University

Modern Logic, 6 (1996), 247--271

This interview is cobbled together from a series of conversations that took place on the list, l-math, during the fall of 1994. Because the interviewer's remarks (in italics) have been modified and quoted out of context, I have not credited them to the people who suggested them, although a lot has been quoted verbatim. The interviewee's remarks are mine.

I am indebted to Jim Murdock, Wayne Myrvold, Peter Nyikos, Randall Holmes, Ray Mines and Adriano Palma for inspiring this and for giving their permission to quote freely and anonymously from their posts. I am also indebted to Gabriel Stolzenberg and to Geoffrey Hellman for previous correspondences that crystallized my views on many of these matters.

Are we talking about the same things?

We have a long-running paradigm conflict between classical and constructive mathematics that has not yet spun itself out. I think it should end with accepting both as viable research programs which are about different things; to some extent this has already happened.

That doesn't strike me as a typical outcome of a paradigm conflict. It seems to me that conflicting paradigms are concerned with the same thing. When I think about real numbers, for example, I believe that I am talking about the same objects that a classical mathematician is. The difference is that I don't accept certain methods of reasoning about real numbers which obliterate distinctions that I think are important.

In order to avoid a paradigm conflict, the classical mathematician tends to dismiss constructive mathematics as the study of computability questions, and the constructive mathematician dismisses classical mathematics as an exercise in formal logic, much like investigating the consequences of large cardinal axioms.

But isn't it true that, if you are a constructivist, then you should think that classical mathematicians are not talking about real objects at all? For instance, every real number in the classical mathematician's universe is either positive, negative, or zero. That's not true of every real number in the constructivist's universe.

When you phrase things in terms of "the classical mathematician's universe" and "the constructivist's universe," then of course it will be hard to see how we are talking about the same things. I view your real number example in terms of what people can prove, not as what the objects are. A classical mathematician can prove that every real number is either positive, negative, or zero. I think that the logical principles that he employs in order to do that are suspect, or, at best, crude. My logical principles give me a more refined view of the universe---I can see delicate structural differences that the classical mathematician is blind to.

That's going a little far, isn't it? Classical mathematicians can subsume constructivism quite nicely by making the proper distinctions.

If by "the proper distinctions" you mean pointing out when the law of excluded middle is used, then I agree. But then you would really be operating as a constructive mathematician. If you mean distinguishing between computable and noncomputable real numbers, for example, then I really don't think that constructive mathematics is captured at all.

Fine. Pointing out when the law of excluded middle is used is like pointing out when the axiom of choice is used in a proof. Most mathematicians don't bother to do it, but they could.

I'm not so sure that they could. They don't bother pointing out when it is used because they think, at the gut level, that it is true. Possibly the majority of mathematicians could point out the majority of tacit appeals to the unrestricted axiom of choice, although even that is not clear to me (free modules are projective, for example). However I am quite sure that most mathematicians would miss most tacit appeals to the countable axiom of choice. Like a countable union of countable sets is countable. Or an infinite set has a countably infinite subset (dependent choices).

Catching when the law of excluded middle is used is much more difficult. It's been my experience that most mathematicians cannot do it. That's because the law of excluded middle is an ingrained habit at a very low level.

Let me put it this way: they could do it if they made a strong effort, but most would rather not make the effort. And at this point in time, few are convinced it is worth the effort. I think any mathematician worth his salt could train himself to do it after a lot of concerted effort. But you constructivists really have your work cut out for you, trying to sell us on this.

Certainly. I never meant to suggest that classical mathematicians couldn't learn how to work without the law of excluded middle. Just that they can't do it now, and, as you point out, that it is a nontrivial task to acquire that ability.

Getting back to our different conceptions of the real numbers, let f(x) be a continuous function defined on [0,1]. I say it has a maximum, you don't. So I am saying that my real number system contains a real number that yours may not contain.

Yes, that's what a classical mathematician typically would say. But I reject the idea that your system contains numbers that mine does not. Your system contains theorems that mine does not, and those theorems can assert the existence of numbers. As you believe in those theorems, and here I am, an apparently sane individual, who doubts them, you are inclined to think that I am not playing with a full deck. I'm not denying that your function has a maximum; you simply have not proved it to my satisfaction.

So if I say a function has a maximum at a point (that I don't know), you can deny (or be unsure) that the function has a maximum without thinking that I believe in a real number that you don't. What gets confusing is the word "exist." You can say the maximum doesn't exist, without denying the existence of a real number.

I wouldn't deny that the function has a maximum, or say that the maximum doesn't exist. Even a fundamentalist excluded-thirdist would admit the distinction between failing to assert and denying.

Would you say that there is a constructive definition for any sequence of integers between 0 and 9 that I, as a classical mathematician, believe in? I think you ought to be agnostic about that, if you grant any meaning to the question at all. Probably you shouldn't grant any meaning to the question, because how could you know what sequences I believe in?

In any case, my point is this: suppose there is such a sequence that is not constructive. Then my real numbers have an element with that decimal expansion and yours do not.

Your statement "suppose there is a such a sequence that is not constructive" presupposes that there are sequences, some of which are constructive and some of which may not be. I don't buy that. Let me illustrate with a concrete example. You probably believe that there exists a binary sequence an such that an = 1 if and only if the n-th Turing machine halts. I'm pretty sure that I can't prove such a sequence exists. What we have here is a subset of N × {0,1} consisting of those pairs (n,e) such that either e = 0 and the n-th Turing machine does not halt, or e = 1 and the n-th Turing machine halts. We can both agree to that, I think. The question is whether that defines a function---you have a proof that it does; I don't.

When a constructivist says consider a sequence an of digits, he doesn't have to say a "constructive" sequence of digits all the time---we know he means that.

Does he mean that? The word "constructive" is not even in his mathematical vocabulary. This is a central point of disagreement between us. You say that I am proving things about constructive sequences; in fact I am proving things about sequences.

I think the real numbers of classical and constructive mathematicians are an example of the incommensurability of paradigms. For constructivists, mathematical reality consists only of computation with integers, and things reducible to that.

That is a common point of view, but I don't agree with it. Constructivists can and do deal with most any mathematical structure. Bishop's definitions of "set" and "function," for example, don't refer to computation with integers. I offer the following easy theorem in constructive mathematics:

I won't bore you with a proof; the obvious argument is constructive. In what way does this result reduce to computation with integers? The best spin I can put on it is that if the hypothesis can be reduced to computation with integers, then the conclusion can be reduced to computation with integers. But this theorem and its proof are constructively valid whether or not the hypothesis can be reduced to computation with integers.

Doesn't this fly in the face of an explicit statement of Bishop's to the effect that no matter how far you go in constructive mathematics, even if it is Haar measure on Lie groups, the meaning of every statement must be a fact about computation with integers?

I don't identify constructive mathematics with Bishop's every thought on the matter, so I am willing to "fly in the face" of some of his explicit statements. Any statement about Haar measure on a specific Lie group may indeed reduce to facts about computation with integers, and this is no doubt what he had in mind, but it is not clear to me how more general and abstract statements, like the easy theorem I just gave, can so be reduced.

Axiomatics

If you study sets, or something similar, and your methodology is axiomatics, you will naturally arrive at a classical viewpoint.

I don't see that. Most of my constructive mathematics is done from an axiomatic point of view. I prove things about local rings, about countable abelian groups, about finitely presented modules.

I think we might be talking about different meanings of "axiomatics." The axioms for a ring are rather simple-minded things: definitions rather than bold claims about what is true about such an overarching concept as the universe of sets.

A good point. Nevertheless there is a general notion of "axiomatic" versus "constructive" that may be operating in the background here. "Axiomatic" corresponds to describing a circle by the equation x2 + y2 = 1, giving the condition for a point to lie on the circle, while "constructive" corresponds to the parametric form (cos t,sin t), telling you how to construct points on it. In these discussions one rarely gets beyond rather concrete theorems about real numbers and functions. It's a little harder to insist that the constructive theorem that a polynomial ring over a coherent Noetherian ring is coherent and Noetherian be reduced to a statement about computing in the integers, because the axioms for a ring do not refer to the integers. There are no particular obstacles that I know of to treating constructive mathematics from the point of view of axiomatic set theory (using intuitionistic logic, of course), so I don't see how axiomatics even in the "bold claims" sense leads to the classical viewpoint.

I have a feeling that there is often a misunderstanding on the meaning of "the axiomatic method." Some people use this phrase for Zermelo-Fraenkel set theory with the axiom of choice (ZFC), while others use it to describe group theory.

I don't think that there is any misunderstanding. My contention is that there is really not all that much difference, other than intent, between these two uses. It's probably impossible to draw a firm line between logical axioms and theory-specific axioms. Is there really any difference between deducing the consequences of set theory axioms and doing the same for group theory axioms? Is "every set is either empty or nonempty" a logical axiom or a set theory axiom?

I really think that deriving consequences from the axioms of group theory is different from deriving consequences from ZFC. For example, we know that the group axioms are consistent.

How about deriving the consequences of Peano's axioms for arithmetic? I suppose that we know that those are consistent also. Is that like group theory or like ZFC?

The revolutionary thing about noneuclidean geometry was that we started thinking of geometry as group theory rather than ZFC (so to speak). Now we are starting to think of set theory as group theory rather than ZFC. Set theory is twentieth-century Euclidean geometry.

Classical mathematics is not peculiarly suited to presentation by axioms. We can just as well work within IZF (intuitionistic) as ZFC---even if Brouwer didn't like the idea of formalization.

Many mathematicians regard constructivism as simply a topic, or group of topics, within mathematics. They feel that constructivists who don't recognize classical mathematics as legitimate have serious philosophical delusions which cause them to work in very restricted areas of mathematics, but that their view of those areas is the same as that of the classical mathematician, once the definitions are understood correctly.

I regard excluded-thirdism as a topic, or group of topics, within mathematics---a perfectly respectable area, but not to be confused with all of mathematics. In that sense I certainly regard classical mathematics as "legitimate." However, the claim that constructivists work in a very restricted area comes from an incorrect understanding of their definitions by mathematicians who cannot see past the law of excluded middle.

Here is a question that has bothered me ever since the first time I read Bishop. In what sense can your real line be used as a model for either space or time in physics? Are there moments in our lives which are neither earlier than nor later than other moments?

I don't know exactly how to respond to the first question, given that I have already rejected the idea that constructivists have a real line that is different from the classical real line.

The second question seems to presuppose that constructivists believe that there are points on the real line that are incomparable. I know of no such theorem in constructive mathematics. In fact, any theorem in constructive mathematics (although not in full blown intuitionism) is also a theorem in classical mathematics. What constructivists do not accept is that any two points on the real line are comparable. But there is no constructive theorem that precludes that any two points on the real line are comparable.

Maybe I can clarify my view. It now seems apparent to me---although I did not realize this for many years---that for all practical purposes, constructive mathematics coincides with mathematics done in the context of intuitionistic logic. That is, constructive mathematicians work within intuitionistic logic, and any mathematics done in that framework will be judged constructive by them.

There is a lot of talk by constructive mathematicians, myself included, about algorithms and computation. That is because one model of constructive mathematics involves these things, and that model can serve as a guide to when certain classically valid steps are constructively invalid. There are other models in which you have two real numbers that are not comparable, but these are not the intended models. Another model is the classical model---this is simply a reinterpretation of the (trivial) fact that any theorem in constructive mathematics is a theorem in classical mathematics.

The intended models, in my view, are the computational one (usually informally construed) and the classical one. But that really makes no difference. The important point is that any model for classical mathematics is a model for constructive mathematics. That's an essential ingredient, for me, in what makes constructive mathematics so interesting. If we were just proving theorems about certain kinds of algorithms, dealing with some restricted subset of the real numbers, I don't think I would pursue it. But we are proving theorems about real numbers, and these theorems also have computational interpretations---two for one.

Platonism and the law of excluded middle

Only those who believe in the real numbers (in some Platonic sense) strongly enough would even be tempted to think that constructive and classical mathematicians are talking about "the same" real numbers; and if you are that much of a Platonist, then how can you think you are a constructivist?

I think this is somewhat of a separate issue, but it is an issue that intrigues me. Exactly what in the Platonistic point of view precludes a constructivist from holding it? I have never seen a convincing argument that a Platonist must believe in the law of excluded middle. Of course it may be part of the definition of "Platonist." But I don't think you were accusing me of believing in the law of excluded middle.

The point is that if you believe that the real numbers (say) are really there, then you have to believe that each meaningful statement about them is either true or false, whether or not we can (yet, or ever) prove it.

Is this an argument? It seems to me that it can be paraphrased as "if you are a Platonist, then you must believe in excluded middle." Maybe that's the best one can do---it's the best that I have ever seen anyone do.

If the real numbers exist independent of mankind, then how could trichotomy fail to hold?

The question should be, "if the real numbers exist independent of mankind, then why should trichotomy hold?" I don't think that believing that the real numbers exist independent of mankind has any effect on constructive mathematicians, except that it might prevent us from talking about time-dependent truth, which seems like a good thing, and it might allow us to talk about truth, which also seems like a good thing.

What would a Platonic universe be like if LEM did not hold?

It would be like the universe that we constructive mathematicians are familiar with.

It had not occurred to me that one could be a Platonist about the classical real numbers and at the same time insist on constructive proofs about these real numbers simply because one wants stronger proofs and computational interpretations.

I would insist on removing the word "classical" from this characterization. Other than that it seems fair, although "stronger proofs" are not desired as such, but only because they allow computational interpretations of the theorems.

You acknowledged that there are two different subjects of study: (a) computable real numbers and (b) classical real numbers.

I tried to be accommodating. My hope was that we could find some common ground by talking about models. But in so doing, I have distorted my position a bit.

I don't really think in terms of the classical real numbers as being a model for the mathematics that I do. That kind of formulation is strictly for external consumption---to communicate some idea of why constructive mathematics applies in a classical environment, and why it does not simply deal with computable real numbers, as is the common conception. Rather I am simply conscious that my proofs are acceptable, if sometimes a bit mysterious, to the classical mathematician, without his having to interpret them in terms of computable things.

Also, I am not sure what you mean by "computable real numbers." The usual classical sense of this phrase is in terms of recursive functions. These computable real numbers---which form a subset of the real numbers even from the constructive point of view, although not demonstrably proper as yet---can be used as a model. They allow us to show that certain statements, although not refutable within constructive mathematics, are unprovable because false in that model. The classical theorem that there exists a uniformly continuous computable function on the computable real numbers in [0,1], that is always positive but whose infimum is zero, shows that we can't hope to find a constructive proof that an everywhere positive uniformly continuous function on [0,1] has a positive infimum.

But that model is not of primary interest to the constructive mathematician. When I referred to "the computational model (usually informally construed)" I really meant "our view of the real numbers." When I referred to "the classical model" I really meant the standard view of the real numbers as reflected by the theorems that can be proved about them using the law of excluded middle. Because constructive mathematics assumes less than classical mathematics, which assumes the law of excluded middle, any theorem in the former is a theorem in the latter---that is really the only sense in which I would assert that the classical universe is a model for constructive mathematics.

There is a fundamental asymmetry between constructive and classical mathematics because the former is a generalization of the latter (fewer assumptions). I have no difficulty understanding what the classical mathematician is up to because I can view his efforts as exploring the consequences of the law of excluded middle, and I can easily talk to him on his own terms. But judging by the attempts of classical mathematicians to understand constructive mathematics solely in terms of recursive function theory---constructive real numbers as special kinds of real numbers---because they cannot shake their dependence on the law of excluded middle, I would say that it is much more difficult for them to understand what we are doing.

The whole and the part

Most mathematicians simply do mathematics as we see fit, and if some of us like to be more restrictive in the axioms and techniques than others, that's generally fine with them.

Ah, the spirit of tolerance! Why would they care? No one has actively tried to prevent me from doing constructive mathematics. On the other hand, I don't think I could get away for long teaching the required introductory analysis course from a constructive point of view.

When constructivists claim that theirs is the only true mathematics and that classical mathematics is at best a small part of mathematics, in the sense that a classical theorem can only point the way to what could be a constructive theorem, but is empty of positive mathematical content unless proven in a constructive manner, they step outside the classical framework. But in so doing, they are also stepping outside constructivism per se and stepping into the philosophy of mathematics.

It seems perfectly okay for classical mathematicians to say that constructive mathematics is just a small part of mathematics. They think, rather they know, that theirs is the only true mathematics. No "stepping into the philosophy of mathematics" there.

Okay, so we live in glass houses too. But we don't throw stones with the vigor you constructivists do. We are, or should be, perfectly willing to accommodate you as fellow mathematicians. Are you willing to do the same for us?

What need have you to throw stones? Flicking away flies is a more appropriate image. It's a very asymmetric situation---we are a tiny minority. We have a message that implies, no matter how tactfully it is phrased, that you really ought to be doing mathematics in a different way. We too could be patronizing if we were the majority. Even as it stands, if anyone wishes to study the consequences of the law of excluded middle, then far be it from us to say that they shouldn't. We might even be interested in the results. But we view this as a small corner of mathematics, and not the most interesting part, in much the same way as most mathematicians view the theory of recursive functions.

"Small corner" in what sense? I'd wager that the vast majority of published research is in this "small corner."

Well, if mathematics is what mathematicians do, then of course you are correct---and there can be no paradigm changes. The sense is in terms of my vision of what mathematics is.

My claim would be that classical mathematics is only a small part of mathematics in the sense that constructive mathematics is more general. Although the notion of positive mathematical content is tricky in the presence of the law of excluded middle, which confounds a statement with its double negation, I wouldn't say that a classical theorem is empty of positive mathematical content unless proven in a constructive manner. I would only use the terms "classical theorem" and "constructive theorem" to refer to a theorem with a classical proof and to a theorem with a constructive proof. I make no distinction between classical and constructive statements. So a classical theorem that is proven in a constructive manner is a constructive theorem.

The Bishop and Bridges distinction between "finite" and "subfinite" would seem to contradict this. When I talk about finite sets, I mean both kinds. Do you have a way out of this predicament?

Every finite set is subfinite, so of course you mean both kinds. You don't really have a notion of subfinite set, or, rather, you think you have no need of one, because you are under the impression that every subfinite set is finite. Yet you are still capable of distinguishing the two ideas.

By the way, I dislike the term "subfinite" as Bishop uses it because it suggests a subset of a finite set. It means a set of the form {x1,x2,... ,xn}, what Ray Mines has called a "finitely enumerable set." We can't assert that such a set is finite because don't have the law of excluded middle to justify the claim that either x1 = x2, or x1 ¹ x2. And, according to the definition we prefer, a finite set can be put into one-to-one correspondence with the set 1,2,... ,m for some nonnegative integer m.

The richness of constructive mathematics lies in the fact that concepts that are equivalent in the presence of the law of excluded middle, need not be equivalent. This is typical of generalizations: the notion of a normal subgroup is equivalent to that of a subgroup in the context of the commutative law, just as the notion of a detachable subset is equivalent that of a subset in the context of the law of excluded middle. (A subset A of a set B is detachable if for each b in B, either b is in A, or b is not in A.)

My personal view is that the mathematical content of a theorem is contained in its statement, although I realize that some constructivists, and others, have held that you can't understand a theorem until you see the proof. So I would not be tempted to say that the content of a theorem depended on whether on not it was proved in a constructive manner. However a theorem of the form, "if the law of excluded middle, then P" does not seem to me to have much positive content, because the law of excluded middle obliterates the notion of positive content (every statement is equivalent to a statement of the form "not Q").

What exactly does it mean to say "either ... or" in an intuitionistic statement such as "for all real x, either x > 1 or x < 2"? Is the quantifier classical? the disjunction?

I don't distinguish between classical and intuitionistic quantifiers. There are just quantifiers. What I distinguish between are classical and intuitionistic proofs.

Are there results in constructive analysis that can not be translated into classical analysis?

No. But I claim that the proper "translation" is just verbatim. The theorem should read the same as it did before translation.

Can classical mathematics be expressed in terms constructivists can understand? In the formalized versions of intuitionistic mathematics that I'm aware of, classical mathematical results can indeed be expressed, but are of an unsatisfactory character.

It seems to me that constructivists can understand classical mathematics perfectly well as it is normally stated, so there is really no problem of being able to express classical mathematical results. The problem is to express those results in such a way that they admit intuitionistic proofs. The cheap solution is to replace "P" by "LEM Þ P". A more elaborate solution, some sort of negative translation, does indeed result in unsatisfactory theorems. But this simply reflects the reason that constructivists find classical mathematics unsatisfactory.

Time-dependent truth

I understand Bishop to say that for any sequence of digits which today is not known to be constructive, the corresponding real number does not exist today, but may tomorrow, if someone tomorrow discovers the construction. So not only do I have different real numbers from constructivists, but constructivists have different real numbers on different days.

I sort of doubt that Bishop would talk about sequences that are not known to be constructive. That would have to take place in a framework where there are sequences, some of which are constructive. Constructive mathematicians talk about sequences, not constructive sequences---just like everybody else. The only people who talk about constructive sequences are recursive function theorists, and classical mathematicians trying to understand constructive mathematics.

There is no more reason for a constructive mathematician to think in terms of what real numbers exist today and what will exist tomorrow, than for a classical mathematician to think that there are no odd perfect numbers today, but there might be tomorrow. Is the problem here Platonism versus excluded-thirdism again?

If you believe that there is really no such thing as the real numbers, but that talk about real numbers is really disguised talk about possible calculations with integers, then it actually makes no sense to ask whether a given statement about the real numbers is true, unless you mean by that whether it has been proved. That is why a consistent constructivist must believe in time-dependent truth.

The implication here seems to be that constructivists don't believe in the real numbers. I wonder why they write so much about them. Why do you think that's just a code for talking about something else?

In "Constructive analysis," Bishop and Bridges say

  1. nothing is true unless and until it has been proved.

  2. This does not rule out the possibility that at some time in the future [the set] A will have become countably infinite or subfinite.
These quotes also appear (with a slight change in the second) in Bishop's original book "Foundations of constructive analysis." Doesn't this show that truth is time dependent in constructive mathematics?

These quotes certainly go against my claims regarding the lack of time dependence in constructive mathematics. And they go far beyond simply asserting that truth is the same as provability---which is a lot more appealing, but still goes too far for my Platonist leanings. I like to think that the authors went overboard here in their zeal to explain the difference between constructive and classical mathematics. I believe that there is no need to buy into these two statements in order to understand the book. So, although Bishop's book was my initiation into constructive mathematics, I don't feel compelled to take every remark in it as a defining condition for constructive mathematics.

Along those lines, I think that Bishop and his followers (myself included) tended to overemphasize the difference between constructive mathematics and classical mathematics in the early days. That was natural in that we had to establish that we were really doing something, and not just producing trivial modifications of well-known proofs---we had to point out what kind of obstacles we were cleverly overcoming. One of the results of this was an impression that constructive mathematics was a completely different thing, which had to do with completely different objects from those dealt with in classical mathematics.

When Ian Stewart wrote, in a review of "Constructive analysis," that all Bishop and Bridges had shown, in their proof that the real numbers were complete, was that a constructively defined sequence of constructively defined Cauchy sequences converged constructively to a constructive real number (or something very much like that), I realized that we had oversold the idea that constructive mathematics really was different. It's different all right, but it's not the study of constructive things---it is the constructive study of things.

Constructivists understand Bishop's claim that nothing is true unless and until it has been proved as saying that we cannot assert that something is true until it has been proved. After all no one knows that something is true before there is a proof. Maybe God, but he is doing his own mathematics (to use Bishop's image).

Lots of people, not just constructivists, would agree that we cannot (justifiably) assert that something is true until it has been proved. Very few would agree that nothing is true until it has been proved. If Bishop simply meant the former, he could have written that instead of the latter. Also, don't constructivists sometimes assert that a theorem is true before anybody has given a proof? I'm sure they have even been known to assert the truth of a false theorem.

Don't we tell our students that nothing is true unless and until it has been proved? Do we say that the Reimann hypothesis is true? or false? I think we would say that we don't know. Isn't that what Bishop is saying? How does this brings in temporal truth?

The word "until" is temporal; the sentence talks about truth. How do you phrase this sentiment so as not to bring in temporal truth? Maybe, "We can't (justifiably) claim that anything is true until we have a proof of it."

Bishop goes on to say "it is untrue that x > 0 or x = 0." What did he mean by that? He already said "we are unable to prove x > 0 or x = 0." At the least this means that untruth is temporal.

Is it comprehensible to say that the Riemann hypothesis is true? If so, is that statement false? untrue?

How can you hold that things are true before they have been proven unless you are a Platonist? If I were to define a concept called "wizwang," then would all the truths about wizwangs be determined at that point? So that if we were able to prove that all wizwangs are flat, then "wizwangs are flat" had been true all along? If you think that, doesn't that require you to be a Platonist of some sort?

I suspect that I am a Platonist. That's the reason I am interested in the connection between Platonism and LEM. When you define the notion of a wizwang, mightn't you legitimately ask whether every wizwang is flat? Or do you have to wonder whether or not every wizwang "will be" flat? In fact, since we haven't constructed all wizwangs yet, even if you prove that every wizwang is flat, don't you still have to say, "Every wizwang will be flat."?

Maybe you do, and it's just a vestige of Platonism that we don't express our theorems in that way. But now the question is, was the statement "every wizwang will be flat" true all along? As we now have a proof of that, it looks to me like it was true when uttered. A true prediction about the future, as if you had said early in 1994 that the Republicans would gain control of Congress.

When a constructivist proves something about "all" real numbers it seems like "whatever real number you can come up with, this will be true about it." But you may be able to come up with different real numbers on different days, so there is never any definite "set" of real numbers in the classical sense.

What is this metaphor of "coming up with different real numbers on different days"? I've explained that I think that Bishop and Bridges went overboard when they alluded to a time-dependent view of truth, and that it is completely unnecessary for an understanding of their work. Furthermore, I don't see why any mathematician might not explain the quantifier "for all" to a beginning class by saying "whatever real number you can come up with, this will be true about it."

What is it that makes you think that a classical set is somehow more definite than a constructive one? Suppose Bishop had said, "to define a set, we must say what it means for an object to be in it, and what it means for two elements of it to be equal." Would that make it more definite?

Yes, because this language implies that each thing definitely is or is not in each set, and that you know what it means for the object to be in the set regardless of whether or not you know that the object is (or isn't) in the set. With this kind of definite meaning, you get the law of excluded middle for free.

I don't see why this language implies that each thing is or is not in each set. I know what it means for a real number to be positive. Why am I committed to the proposition that each real number is either positive or not positive? You are not getting the law of excluded middle for free---you are simply declaring that it's true.

We can't talk constructively about "all" x that have property P(x) because we can't prove or disprove P(x) for each and every x. We can only talk about "any" x for which we have currently proved P(x), and such a wishy-washy "set" can't be real.

Why should constructivists be limited to considering P(x) only when they can either prove or disprove P(x)? The only reason I can see for doing that is to preserve the law of excluded middle. Do you mean that I can't even talk about the Riemann hypothesis, let alone the continuum hypothesis?

Sets and algorithms

Aren't you obligated to believe that some sets that I would talk about are unreal?

How did I give you that impression? I said that classical mathematicians and constructive mathematicians are talking about the same things---the difference lies in what we can prove. You might be able prove that a certain set of ordered pairs specifies a function (for each x, there exists a y, and so on), and I might be unable. That doesn't mean I'm going to think that your set is unreal.

It seems to me that we are going in circles because you obstinately refuse, even for the purpose of discussion, to consider the possibility of any meaning to nonconstructive statements. Of course, as long as you do that there cannot be a conversation.

On the contrary, it is you who are insisting that I should think that there is no meaning to nonconstructive statements. I don't even think in terms of constructive and nonconstructive statements. There are statements, there are constructive proofs, and there are nonconstructive proofs.

I'm beginning to formulate things to myself this way: a real number is given when a Cauchy sequence is given; a real number is constructively given when an algorithm for a Cauchy sequence is given, together with an algorithm for determining, given n, how far out you have to go before the terms differ by less than 1/n. That way I can think about Bishop without making futile efforts to abandon all classical thinking and ending up not knowing which way is up.

This is really just a modification of the usual approach to constructive mathematics by way of the classical theory of algorithms---even though you don't say explicitly what an algorithm is. My personal opinion is that you will never get a real feeling for constructive mathematics by constructing classical models for it. The main problem is that you will never realize that you are not simply proving theorems about that model, that your theorems are also true as theorems about the classical universe. On the other hand, such an intermediate stage may be necessary in order for a classically trained mathematician to acquire any feeling at all for operating without LEM.

I should point out, if that is necessary, that my views are a bit different from Bishop's. He emphasizes the idea of an algorithm, or finite procedure. My feeling is that constructive mathematics is simply mathematics done in the context of intuitionistic logic, that all the talk about algorithms is ultimately superfluous. In actual practice, it doesn't seem to make much difference which point of view you take.

I'm not trying to construct classical models for constructive mathematics; I'm just trying to understand it. So far, this "classical model" (as you call it) is the only way I can find to attach any meaning to Bishop's words.

You are trying to understand it from within classical logic. That seems much the same to me as trying to construct a classical model for it. You are trying to distinguish constructive sets from ordinary sets by endowing them with extra structure. That's exactly how people construct classical models of constructive mathematics. I've already allowed that a classically trained person may have to start that way.

When I think about Bishop's sets I seem to need to think about other sets in a classical way. That may be just because of my training; or it may be that you guys haven't noticed that you are relying on, or that your language entails, these other sets. That's what I want to figure out.

As I've said, I don't think in terms of two kinds of sets. Bishop is not looking at special kinds of sets, he is looking at sets from a different perspective. But I see now that you are not really talking about two kinds of sets here. In fact, some constructivists have played with the idea of having these "other" sets that you are talking about. The model is the set of Cauchy sequences as opposed to the set of real numbers. The difference is in the equality relation. Of course they don't reason about these other sets classically. Their idea is to clarify Bishop's notion of an operation. My personal preference is to forget about Bishop's notion of an operation.

A classical set can be given by stating the properties of its elements. The set A is constructively given if a set B of algorithms for the elements of A is given (plus maybe something about equality).

That might work if A is a set of real numbers, but what if A is a set of sets of real numbers? You don't have to give an algorithm to construct a set of real numbers. For example, maybe the real number in [0,1] are constructively given by a set of algorithms, but the set of open sets of real numbers is not constructively given by a set of algorithms. Bishop certainly considers such sets.

Let me try to summarize what I take to be your position here. There are classical sets and there are constructive sets. In order to understand a classical set, I have to subscribe to classical logic. So if you can show that constructive sets are really classical sets, then the only way I can understand constructive sets is through classical logic. That would certainly cause me a problem.

My position is that there are sets, there is classical logic, and there is constructive logic. I don't understand the notion of a classical set versus that of a constructive set. I don't find classical statements about sets incomprehensible; I see them simply as statements about sets.

It looks to me like Bishop's definition of a set is compatible with your notion of giving a set by stating the properties of its elements. Certainly for subsets of the real numbers they are the same. If you define a subset A of the real numbers by the property P(x), then I believe Bishop would define the same set by saying, "to construct an element of A, construct a real number x and prove P(x)." Of course he means something different by "prove."

This is interesting and strange. I'm not sure that it fits my notion of "algorithm." What if to prove P(x) requires a different proof for each x? Is that algorithmic? It certainly doesn't fit my notion of "construct," in so far as I have one. When I've constructed x, x is constructed; it doesn't change (or get any more "constructed") when I've proved P(x). At the moment, this seems bizarre enough to make me doubt that my "classical model" (as you called it) fits what Bishop is saying, so once again I'm in the dark.

Let's be specific. Suppose I want to define the set of algebraic real numbers, so P(x) is the statement that x is algebraic. To construct an algebraic real number, I have to construct a real number x and prove that it is algebraic. Of course the proof may vary from x to x. To prove that x is algebraic, I have to construct a nonzero polynomial p with integer coefficients and prove that p(x) = 0. What is the problem here? How does your notion of an algorithm enter into it?

An algorithm should be completely spelled out before I start. So you have to tell me before I construct any of the real numbers (that are algebraic) exactly how I'm supposed to prove that they are algebraic. If you leave that open, then it seems you have a notion of constructive that is not algorithmic. For such a notion, Church's thesis seems much less likely to be true than it does for the algorithmic notion that I had in mind. I don't require that an algorithm be programmable, hence recursive, but I strongly suspect that they all are.

Do you want me to spell out what it means to construct a nonzero polynomial p with integer coefficients, or just spell out what it means to prove that p(x) = 0? I assume its the latter. But that is really just asking what it means for a real number to be equal to zero; presumably you understand how to compute p(x). All of that is covered pretty well in Bishop's development of the real numbers.

Perhaps you are really asking how you prove anything without appealing to the law of excluded middle. I say this because you wouldn't bring up this issue of exactly how you were supposed to prove things in classical mathematics.

As for Church's thesis, there can be no constructive proof that every function from the positive integers to themselves is recursive because that is classically refutable. I want the notion of "algorithm," if you insist on using that word, to be broad enough to encompass an arbitrary classical function. In addition, I would like to be free to interpret it in a more computational way, and still have the theorems true. So I want my notion of constructive to be both algorithmic and not necessarily algorithmic.

Gabriel Stolzenberg claims that the statements of classical mathematics have no meaning. That is the whole basis of his rejection of classical mathematics: he claims (as I understand it) that constructivism rests on an analysis of the possible meaning of mathematical statements, and that as understood by classical mathematicians, they simply have none. If you do not agree with Stolzenberg, that is fine with me. Or have I misunderstood him?

I couldn't speak authoritatively as to whether you misunderstood Stolzenberg, but it seems to me that you have captured some of his spirit. He and I differ on this issue (obviously). (Click here for a comment by Stolzenberg about this.)

Two algorithms for which it is constructively provable that the output is the same, but which differ in their working, are equal in extension but different in intension---both senses of equality are significant for constructivists.

As far as I know, constructivists don't normally refer to equality of algorithms ("in their working"), and I doubt that intensional equality is significant for them. For example, recall that for Bishop equality is conventional, something that is defined when a set is constructed. I don't remember his ever saying what equality of algorithms was.

Bishop's criterion that "a set is defined by describing what must be done to construct an element of the set, and what must be done to show that two elements of the set are equal" speaks also to the classical mathematician. The equality here is extensional, as always. The way I see it, you can't really understand what the elements of a set are until you know when two of them are considered equal---the notion of equality clarifies the essential properties of the elements. This is analogous to the categorical point of view in mathematics which suggests that we don't really understand mathematical structures until we know what the maps between them are, or at least the isomorphisms.

Platonism and the law of excluded middle

In the back of my mind is the idea that Bishop is somehow trying to say we can do set theory even with sets that are not viewed as complete totalities.

Maybe Bishop was indeed trying to say that, but I don't see constructive mathematics in that way. I don't really know what a completed infinite totality is, as opposed to an incomplete one. I know that we are all supposed to understand this idea, which presumably goes back to Aristotle. As far as I can tell, it just means that we feel free to use the law of excluded middle. Other than that, I don't have the faintest notion of what it means.

It seems to me that if a specific real number is a definite thing at all, then it either is or isn't positive. I don't see any way to doubt that. The reason why one is tempted to doubt the law of excluded middle is that maybe real numbers aren't definite things in some sense; maybe they are (as you would say) constructed, and don't exist until they are constructed, and before a particular number exists it can't be positive or negative.

To go a little far afield, don't the results on the continuum hypothesis suggest that one should doubt the law of excluded middle? One could argue that we just don't have the right formulation of set theory yet, but I don't think it likely that we will ever come down on one side or the other of this question. Rather I think we will just stop paying attention to it.

The conundrum you present me with is that whenever I propose any of the reasons that I have heard for disbelieving in the law of excluded middle, you tell me you don't accept those. You don't think truth is time dependent; you don't think sets are incomplete; you don't think the existence of particular real numbers depends on someone having already constructed them; you demand the right to talk about properties of things, and that these have meaning, before they have been proved or disproved; so what possible reason is left for disbelieving in excluded middle?

This looks like a proof by contradiction to me. It's hard to discuss the law of excluded middle without using it to justify itself. There is also the delicate issue of the difference between disbelieving something and believing that it is false. I'm not even sure there is a difference. I'm not asserting that LEM is false; I'm saying that the mathematics is better when you don't invoke it. Theorems proved without the use of LEM have valid computational interpretations that theorems proved using LEM do not.

Here is an example that may help. It is an easy argument, using LEM, that some digit appears infinitely often in the decimal expansion of p . A constructive proof of that theorem would contain some way of getting hold of one of those digits. I have a little difficulty even understanding what it might mean for this theorem to be true short of getting hold of such a digit. Here is a related quote from Wittgenstein:

[If] a proof convinces you that there is a root of an equation (without giving you any idea where)---how do you know that you understand the proposition that there is a root?
I do understand that it is contradictory for each digit to appear only a finite number of times. That seems to me to be a different theorem. And there is no way that I can make that distinction in the context of the law of excluded middle.

Constructivists are often accused of confusing epistemology and ontology. But surely the line is less sharp than some believe. In what sense can something be shown to exist without some clue being given as to how to find it in principle?

I would say the contradictoriness of each digit appearing a finite number of times means either some digit appears infinitely many times, or mathematics is inconsistent. Is that what you mean? Or do you imagine that there is another possibility that we haven't thought of yet?

It's a gut issue whether this theorem is different from the one that says it is contradictory for each digit to appear only a finite number of times. It has nothing to do with the consistency of mathematics. You are forced to those conclusions by your unwavering belief in the law of excluded middle. I don't know if I can clarify this further. I sort of hoped that the example would strike a responsive chord.

It seems to me that dropping LEM just removes the distinction between existence and computability.

What is computability? If it does not refer to recursive functions, what does it refer to? In the usual classical usage, the difference between a function and a computable function is that the latter is recursive. Perhaps your distinction between existence and computability is parallel to my distinction between

(a) It is impossible for each digit to appear only a finite number of times in the decimal expansion of p .

(b) Some digit appears infinitely often in the decimal expansion of p .

Yes, I suspect that it is. But to me, my distinction seems natural and obvious whereas yours seems forced and odd and unclear. I don't see that I am obliged to have a necessary and sufficient condition for constructivity in order to use the concept classically. "Constructive" for me is not a mathematical term, it is a metamathematical term---hence informal---and it is explicitly time dependent, as are many terms in informal language such as "President of the United States."

I probably got off on the wrong track there. But are you saying here that classical mathematics admits time-dependent terminology? Maybe you are thinking of "constructive" as something one would use to describe a proof in much the same way as one would use "elegant," but somehow more precise. Mathematicians will demand that you be even more precise---in particular, they are going to wonder why they should give up their hard won, universally accepted, Church's thesis for something that sounds incoherent and vaguely sociological.

As you say, this notion of computability is nonmathematical and time dependent. I don't see what you buy with it. We always knew that we could compute certain things in practice, and couldn't compute other things. It seems to identify constructive mathematics with numerical analysis and engineering: on the one hand there is mathematics with its theorems and proofs, on the other hand we could interest ourselves in the details of computation. There seems to be none of the systematic treatment of computability that characterizes both the constructive approach and the classical recursive function theory approach.

Constructive mathematics and classical logic

There are obstacles to a constructivization of quantum mechanics---one must do away with unbounded operators.

Why is that? Can't constructivists take derivatives? Can't they consider the operator T that takes the n-th basis element en of Hilbert space to the element nen? That's the kind of misconception you get when you attempt to use classical methods to investigate constructive mathematics.

Geoffrey Hellman argues, on the basis of a theorem of Pour-El and Richards, that constructive mathematics cannot handle unbounded operators . For example, consider the unbounded operator T mentioned before. You construct a particular recursive element x of the Hilbert space, give a nonconstructive proof that x is in the domain of T, and show that T(x) is not recursive. So T takes some recursive element to a nonrecursive element, which presumably makes T impossible to study from a constructive point of view.

If constructive mathematics were the study of recursive objects, or even the study of constructive objects, then this might seem like a serious objection. But as it stands, we simply have an element x that we cannot prove is in the domain of T. So what? That kind of thing happens throughout constructive mathematics---you don't have to go to unbounded operators in a Hilbert space to run into it.

If constructive mathematics is not the study of recursive objects, what is the relationship between constructive mathematics and the classical theory of algorithms?

Consider this theorem in the classical theory of algorithms:

This is even a theorem in constructive mathematics. But you cannot prove, within constructive mathematics, that there is an increasing bounded sequence of rational numbers that is eventually bounded away from any given real number. How could you, in light of the fact that you can prove classically that every increasing bounded sequence of rational numbers converges to a real number?

I've always felt that the following example constituted a reductio ad absurdum of the classical notion of computability. But I had always had recursive function theory in mind. In fact, I believe that the example shows that we cannot capture the intuitive notion of computability in the context of classical logic.

Let f(n) = 1 if there is a run of (at least) n consecutive 4's in the decimal expansion of p , and f(n) = 0 otherwise. I am speaking classically here, of course---we have only a classical proof that such a function exists.

I claim two things:

  1. To assert that f is computable, in our present state of knowledge about the decimal expansion of p , flies in the face of our intuitive understanding of the word "computable."

  2. Classical logic forces us to conclude that f is computable.
The fact is that we don't know how to compute f(20), nor can we point to an algorithm that would in principle calculate f(20). It is ludicrous to say that f is computable.

On the other hand, classical logic informs us that there is a simple algorithm for computing f. For each natural number m there is a (clearly computable) function g defined by

g(n)= ì
í
î
1 if n < m
0 otherwise.
The function g that is always equal to 1 is also computable. It's pretty easy to see that our function f cannot be different from each of those functions g. So it must be one of them, hence computable.

I once heard Vladimir Lifschitz say---quoting Heyting, I think---that classical mathematics had a notion of a computable function, but no notion of a computable number.

We can define intensional objects under classical logic. Your function f would constitute an algorithm (an intensional object) for which we cannot say whether it is computable or not, but we can say that it must have the same extension as some (trivially) computable function. This is classically all perfectly true, comprehensible, and not a reductio ad absurdum of anything. Identity conditions for intensional objects are different from those for extensional objects, that's all.

Computability is "naturally" a property of intensional objects. The oddity of the terminology is part of the price we pay for working with extensions, which are much easier to understand and work with than intensions. None of this has much to do with the choice of classical logic over intuitionistic logic.

I think it does. I work with extensions and I don't talk about computable functions when I'm doing mathematics. My theorems have computational interpretations because I use intuitionistic logic. Classical mathematicians argue that they can do better by studying algorithms using classical logic. They claim they don't want to work with intensions, but they invoke them to explain computability. Does a comprehensible explanation of a counterintuitive result say that our intuition was wrong? Perhaps. But choosing intuitionistic logic avoids working with intensions yet allows us to preserve the intuitive notion of computability.

Computability is not properly a mathematical notion (exclusively) but one involving the interaction of mathematics and minds. The function f would be computable by an omniscient mind, but isn't by us, now.

The interaction of a mind with the mathematical universe is a metaphor that I think is useful. In fact, if you read the beginning of Chapter 1 of "A course in constructive algebra" you will see that I use it to explain the difference between constructive and classical mathematics. An important feature is that we do not rule out the possibility of an omniscient mind, but we do our mathematics without assuming an omniscient mind.

I don't think that using intuitionistic logic avoids intensions, or failures of extensionality, for that matter. Intuitionistic logic has the effect of coding information about intensions into the truth values of the logic. Observed from a classical standpoint, it is an elegant way of working with intension and making it look like extension.

That brings us back to the start of this conversation: the idea of a paradigm shift. When you look at constructivism from a classical standpoint, you are going to see something different from what the constructivist sees. If classical logic is just plain true, then your idea of what is happening is better than his. Personally, I think the constructivist sees things more clearly.



richman@fau.edu

This document was translated from LATEX by HEVEA.