[FOM] Ask Dr. Bill

[William Tait]

Gabriel, Your subject line borders, at least to my ear, on insulting.  
I hope that you did not intend it to be.

>   -3.  True or false?  A classical existence proof is often a
> good first step towards getting a construction.

  I would guess that it sometimes can be. When Bishop began his  
project of constructivizing analysis, what he had on hand was  
(besides the negative critique of the intuitionists) the body of  
classical analysis. Do you think that I am wrong to say that what he  
did was to see what and how classical results, by suitable  
strengthening of definitions, could be constructivized (perhaps in a  
modified form)? Even in cases like the intermediate value theorem,  
which is not constructive, the technique used to prove a  
constructively valid weaker form is a refinement of Bolzano's  
original nested intervals argument.

On the other hand,  given a particular real function f, a classical  
proof that it is continuous + Heine-Borel will generally not be a big  
help in finding a proof that f is continuous in Bishop's sense  
(locally uniformly continuous), i.e. in actually constructing the  
modulus of local uniform continuity. But, of course, this remark  
applies anyway only to the cases in which f has a constructive  
modulus of luc.

My last remark is motivated by a consideration that your question may  
be ignoring: The agenda of classical mathematics is not restricted to  
finding constructive bounds or to proving existential propositions  
only when constructive bounds exist.

>   -2.  True or false?  A classical existence proof is often an
> annoying distraction from getting a construction.

Like -3, this is too imprecise to have a truth-value. It is certainly  
annoying when, trying to prove 'there exists' constructively, you  
realize that you have only proved 'not-not-there exists'. But if one  
is used to constructive reasoning, that is not so likely to happen.

But I think my real answer (neither a 'true' nor a 'false') is in my  
response to -3.  Sometimes the passage from the argument for 'not-not- 
there exists' can be replaced by a direct argument for 'there  
exists,' while the rest of the classical argument remains intact and  
is perfectly constructive.  But sometimes it can't. Reference:  
Bishop's book on constructive analysis.

>   -1.  Among classical mathematicians, constructive math is the
> study of what can be proved without omniscience.  How does your
> own interpretation of it as a part of classical math differ from
> this?

"Among classical mathematicians, constructive math is the
study of what can be proved without omniscience." First of all, I  
doubt that you are right about what classical mathematicians would  
say. Proof is defined by means of axioms definitions and rules of  
inference. This is what is objective and independent of your  
intuitions, or whatever, and mine. Classical math admits the logical  
axiom 'A or not-A'. You may pars this as an expression of  
omniscience---as did Bishop. But I don't see it that way: Doesn't my  
view get to count? The talk about omniscience is metaphorical and  
perhaps good for pep-talks in favor of constructive math; but what is  
its real content? God is omniscient because It can know that P(n)  
holds for all natural numbers n, and we are not because we can't. But  
constructive mathematics assumes in the same sense that we are able  
to know that P(n) holds for all n up to any arbitrary number N, where  
P is any decidable property, no matter how complex its definition.  
That's still pretty omniscient in my book.

>    0.  If classical math didn't exist, would constructive math
> have to invent it?

Perhaps, in a sense, it did.  Eighteenth century analysis seems quite  
constructive (although not self-consciously so), in the sense that  
existence proofs yielded computations. [But I am out on a limb here:  
Take this as a conjecture about what a competent historian of the  
period would discover.] The first result that I know of for which  
this isn't so is Bolzano's proof of the intermediate value theorem in  
1817.

Of course, his proof was not well-known,  but Cauchy's proof some  
four years later seems to have been widely known. What is surprising,  
looking back at it from here, is how long it took for there to be a  
constructive reaction, namely (as far as I know) by Kronecker. [Here  
again, a historian of that period might have a different view of  
this.] It is also worth mentioning that for him your constructivism  
is too profligate. He rejected objects not representable by integers  
and properties which are not algorithmic. So it wasn't for him a  
matter of rejecting excluded middle; rather mathematics should not be  
concerned with propositions for which EM is not provable.

But constructive math (in your sense and self-conscious) would not  
only not have to, it indeed would not invent classical math as long  
as its aims remained constructive: an existence p[roof should yield  
an algorithm.

>    1. Why is it important to you that a statement about real
> numbers in constructive math mean the same thing as the formally
> identical statement in classical math?

What is important to me is conceptual clarity. I believe that the  
only way to understand the term 'meaning'  (of expressions) is their  
public meaning, to be understood in terms of how they are correctly  
used. (The term 'correctly' here is indeed loaded; but I needn't go  
into this now. )The main point is that the locus of meaning cannot be  
(as you suggested in an earlier posting) in the mind. For the  
question would then be mandatory: Whose mind?

So, its not important to me that a statement about reals mean the  
same thing in constructive as in classical math. What I do hold is  
that the principles of reasoning about reals in constructive math are  
classically valid---once one resolves some conflicts in terminology.

>    2. Why would it be a bad idea for a mathematical community to
> have a paradigm shift in which it replaces its old metaphysics
> with a new one?

I don't care to fish in this pond---or rather ocean.

>    3. Do you believe that classical math provides the big picture
> but that in constructive math we have difficulty seeing the forest
> for the trees?

No.

>    4. Why do you dislike the interpretation of classical math as the
> part of constructive math in which we investigate how it helps to be
> omniscient?

I don't really dislike it; it is amusing.

Now let me ask a question: Why is it so important to you to wage war  
with classical mathematics? Why should its existence (indeed,  
thriving existence) threaten the pursuit of constructive math? The  
bible-thumping seems completely inappropriate to me.

Kind regards,

Bill