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:
-
If f maps the set A onto the set B,
and g maps B onto the set C, then the composition gf maps A onto C.
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
-
nothing is true unless and until it has been proved.
- 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:
-
There is an ascending, bounded, recursive sequence of rational
numbers that is eventually bounded away from any given recursive real
number.
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:
-
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."
- 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
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.