[FOM] Haney and Tait on intuitive sources of mathematics
William Tait
wwtx at earthlink.net
Sat Feb 11 14:41:10 EST 2006
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
More information about the FOM
mailing list