[FOM] Haney and Tait on intuitive sources of mathematics

[William Tait]

Dear Gabriel,

You are too fast for me, so let me reply at the same time to the two  
messages in which you address my remark about circularity in my paper  
"LEM and AC".

First, let me thank you for reading it: That makes two of us. (I've  
been counting.)

An aside: Actually, Gregory Moore seems to have read at least a  
footnote in it, where I criticize him for his rather slighting  
treatment of Bolzano in his book on Zermelo's AC. He responded quite  
cruelly in a paper in *The History and Philosophy of Logic*, 20  
(2000):169-180: He called me a philosopher. A philosopher is  
apparently someone who believes that, if you have proved that if, for  
an upper bounded set M of reals, there is some real c such that x is  
in M for all x < c, then there is a greatest such c (proved by  
Bolzano in 1817 using [for the first time?] an iterated dichotomy  
argument to construct a Cauchy sequence for the greatest such c---he  
applied it to prove the intermediate value theorem), then you have  
done more than just give the "rudiments of" a proof of the Bolzano- 
Weierstrass theorem that, if N is an infinite subset of [c, d]^n,  
then it has a limit point. A philosopher would likely blunder so  
badly as to say that you have given the guts of the proof of BW---The  
one-dimensional case is an immediate consequence, obtained by taking  
M to be the set of reals x such that either x< c or N intersect [c,  
x) is finite. A historian, on the contrary, would apparently know  
enough not to believe such a thing: he would know for example that,  
since the notion of a limit point hadn't been invented in 1817,  
Bolzano couldn't possibly be credited with a proof of BW. Poor  
Pythagoras or whoever has thereby lost his title to the discovery of  
irrational numbers, since the Greeks didn't then have the concept of  
rational or irrational number. (Of course, Weierstrass did extend the  
BW theorem to arbitrary finite dimensions.)

Now that I have that off my chest, on to your remarks.

> I admire
> Brouwer but if I had invented the concept of a free choice
> sequence, I probably would apologize.

If one drops the subjectivist element in Brouwer's thought, then  
thinking of the continuum or Baire space as a spread S of choice  
sequences amounts merely to requiring that the unsecured sequences of  
a function from S into N be well-founded. But this corresponds to  
Bishop's definition of continuity of a function as local uniform  
continuity: For simplicity, think of Baire space S and let F map S to  
S. F' maps SxN to N, where F'(g, n) = F(g)(n). Then I expect it is  
well-known that F is locally uniformly continuous iff F' is a Brouwer  
function.  Still, Bishop's treatment is more elegant and fits better  
the historical development of analysis. Also, alas, the subjectivist  
element was there in Brouwer and is there in some of his contemporary  
disciples.

>    Re "the unique source of mathematics is the intuition,"
> I recommend looking carefully at the learning process, the
> training.  Once the mathematics is codified, the training
> creates "the intuition."  And different trainings sometimes
> create different intuitions.

There are two notions of intuition that float/flounder around in  
discussions of philosophy of mathematics. Or rather, there is one  
relatively clear one on the one hand and a constellation of  
relatively unclear ones on the other. (Poincare, in an essay entitles  
"Mathematics and intuition", I think, discussed this.) In the first  
sense, one could say intuition takes over where logic can't go. It is  
in this sense that Brouwer and (in his intuitionistic phase) Weyl  
spoke of intuition---and I believe (following Michael Friedman) that  
their conception derives from Kant's notion of inner intuition and  
the schema of quantity. Brouwer spoke of two 'acts of intuition', one  
leading to the creation of  two things out of one (the intuition of  
'two-ity') and the second leading to the generation of spreads. Weyl,  
who was a better philosopher than Brouwer, understood that the  
successor operation was not the issue, but rather that then basis of  
arithmetic is the notion of a finite iteration of *any* operation,  
and he took that notion of finite iteration as what is given in  
intuition.

For those who accept classical mathematics, finite iteration does not  
escape the bounds of logic and so is not founded on intuition in this  
sense: Frege and Dedekind showed that it can be analyzed logically,  
providing we admit classical (impredicative) second-order logic. But  
Gabriel, as a constructivist, you cannot accept this analysis, and so  
shouldn't be so dismissive of intuition. Proof by math induction and  
(more generally) definition by iteration is primitive from a  
constructive point of view. This is not the sense of 'intuition' that  
you had in mind in your posting, but it at least should have been the  
sense that Haney had in mind. As you say:

>    But Haney may be thinking in terms of an intuitive source
> that preceded the codification.

But what follows this passage is not to the point concerning Haney's  
sources: the intuitionists Brouwer and (perhaps) Weyl  (e.g. Weyl's  
intuitionism rejected logic entirely). Rather, it concerns Bishop.

About my LEM and AC:

>    Hence, this something (which we call "a procedure" or "a
> computation") is not something that can serve as an arbiter
> for what in the mathematics is true and what is not.  If it
> were being asked to fulfill such a role, it could not.  But
> it is not being asked to do that.
>
>    At least, so say I.  However, on my reading, the following
> statement from Tait's "The law of excluded middle and the axiom
> of choice" implies that what I say above about the constructive
> mathematical mindset (in particular, mine) is false.  He writes,
>
>       "The circle is ineliminable in constructive mathematics,
>        because whatever principles of logic are given, they
>        must answer the challenge of whether they really yield
>        'constructive objects.'  For the notion of being
>        constructive is intended as a measure of correctness
>        for any particular principle considered."
>
>     Nevertheless, this claim about the intentions of people like
> me is mistaken.  We break the apparent circle of which Tait speaks
> (I call it a regress) the same way he does; indeed, I congratulate
> him for having seen that it is the right thing to do.

I was/am not concerned with mindsets or intentions; and If I had  
mentioned them in LEM and AC in an essential way, then---borrowing a  
sentiment from one of my favorite mathematician/philosophers---I  
probably would apologize. I was concerned with definitions.  Let me  
quote from the bible:

"An operation from a set A to a set B is a rule f which assigns an  
element f(a) of B to each element a of A.  The rule must afford an  
explicit finite , mechanical reduction of the procedure for  
constructing f(a) to the procedure for constructing a." [Bishop,  
*Foundations of Constructive Analysis* p. 14.]

A function is defined there to be an extensional operation. A rule f  
is an operation from A to B if it satisfies a forall x in A exists y  
in B condition. Constructively that is understood as a exists z in (A  
-->C) forall x in A statement, where C is the domain of reductions.  
The definition is therefore circular in that the notion of an  
operation from A to C is contained in the definition of the notion of  
an operation from A to C. (There is an infinite regress of witnesses:  
g to witness the fact that rule f is an operation, h to witness that  
g is, etc.)

>     In the same vein (in the same paper), when Tait says,
>
>    "I truly wish that the term 'constructive' had been reserved
>     for just [constructing an object of a given type and a proof
>     of a proposition] since it seems most appropriately applied
>     to the view that the basic notion of mathematics is that of
>     construction, without further specification of what kinds of
>     construction are to be permitted,"
>
> I can reply that, provided only that he and I are reading the
> ambiguous last clause ("without further specification...") the
> same way, in my constructive mathematics and, for all I know,
> in everyone's, the term 'constructive' is, in fact, reserved
> for just what Tait rightly wishes it to be.

We are probably *not* reading it in the same way.  My concern at that  
point was to reject an argument of Michael Dummett, more recently  
taken up by Neil Tennant, that what I will roughly call 'proof- 
theoretical semantics' is possible for constructive mathematics, but  
not for classical math---whose only alternative is 'truth-functional  
semantics', which in fact cannot be coherently spelled out. My point  
was that the same semantics is possible in the classical case. One  
need only to admit the construction of 'ideal' objects f of type not- 
not-A --> A (depending also on the free variables in A). [I like this  
way of understanding Hilbert's ideal objects.]

I did/do not like the move to see constructive mathematics as  
something alien to classical mathematics. [It also seemed to me an  
irony that the machinery that Gentzen invented in the aid of  
obtaining constructive meaning for classical mathematics should have  
been used to attempt their separation.] Of course, there are surface  
differences, for example  because constructive mathematics has to  
build properties into definitions that classical math gets free (e.g.  
local uniform continuity from continuity). But I wanted to reject the  
idea that there was a different subject matter.

My ultimate point there was that what we mean by 'function' for  
example  is displayed solely in the means we admit for defining  
functions. And the rest of it is so much hot air. (Of course, I do  
not deny that hot air can motivate: I read the political news.)

So in this I think I am in agreement with what you wrote in the  
subsequent posting on February 9:

>    No, neither language nor reasoning works that way.  Instead,
> at most what we do is to view such "explanations" as suggestive
> remarks, not definitions.  (Fred Richman does not do even this.
> For him, talk of "a procedure for constructing" merely points
> to one model of the mathematics, one that doesn't interest him
> very much.)  And in place of the latter, we work with the formal
> ones given by the mathematics, which are not really definitions
> at all.  But then what is?

Kind regards,

Bill