FOM: intuitionistic and classical truth

[Colin Mclarty]

Reply to message from neilt at mercutio.cohums.ohio-state.edu of Fri, 04 Sep
>
>Colin McLarty writes that "Any...person knows [that] A, according to Brouwer,
>when that person has created an intuition of A."
>I cannot find any textual hint of this in the more philosophical pieces in
>the first volume of Brouwer's collected works. Could Colin perhaps supply
>some exact quotations?

	I used "create" as a colloquial equivalent to "construct". 
If you object to "create" as synonym for "construct" then you may
want to argue with things I say towards the end of this reply.


>  It would be extraordinary if Brouwer really did regard
>his own rather long proofs (as, for example, of the fundamental theorem of
>algebra) merely as "an intuition of" the theorem thereby proved.

	As I said in my post, Brouwer believed that we rely on
language, due to our sinful weakness, in mathematics where really
language has no place. Much of this, including the theme of sin,
is in "The unreliability of the logical principles". Van Dalen's
article "Brouwer's ideal of language-free mathematics" is also
helpful. But I am at home for the weekend and won't have further
references till next week.

	Brouwer regarded his proofs as attempts to communicate
(already a dubious project for him, as communication is an
attempt to dominate others) suggestions enabling others to make
certain constructions in intuition.

>Brouwer is very explicit that the notion of intuition tht is involved in his
>intuitionism derives from Kant's doctrine of arithmetic and geometry as based
>on the pure forms of intuition of time and of space, respectively.

	Precisely. For Kant, mathematics is knowledge through pure
intuition. Reason has no role in giving us mathematical knowledge,
according to Kant. Reason lets us tautologically re-arrange truths
we already know. But synthetic mathematical knowledge comes from 
finding the possibility of constructions in intuition.

	I take it that "proof" is something done by reasoning.
"Proof" in that sense has no role in discovering, or warranting, 
mathematical knowledge according to Kant. Of course Archimedes
can show you how to superscribe a chiliagon to a circle, and you
can see how some of the angles work out, and he even uses some
logical reasoning to calculate the resulting approximation to pi.
Bu the synthetic steps here come from intuition, according to Kant.
They have no premises. They take no logical steps. And so I think
they cannot well be called "proof" in a FOM sense.


>Brouwer makes it clear that the truth of a given theorem depends on
>*constructions*; and that these constructions are in turn justified by
>basic intuition(s). 

	Yes, certainly.

>Hence he is open (appropriately, in my view) to
>Heyting's explication of constructions as proofs built up by means of rules
>whose validity can be *intuited*.

	Here is our disagreement. Actually, I am not sure what you 
mean by saying Brouwer is open to an explication. If you mean that
perhaps Brouwer actually had such a thing in mind, then it's wrong.
Brouwer did not view a construction as a proof built by rules of
inference.