FOM: intuitionistic and classical truth
neilt at mercutio.cohums.ohio-state.edu
Fri Sep 4 16:31:06 EDT 1998
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? 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.
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. But, with
the advent of non-Euclidean geometries, one can no longer accept the Kantian
doctrine for geometry. The form of intuition of time, however, is left
untouched by the non-Euclidean developments; and, since Descartes had shown
how to arithmetize geometry, the way was open, Brouwer believed, to base
arithmetic (and hence geometry) on the Kantian form of temporal intuition.
(All this is laid out in Brouwer's inaugural lecture at Amsterdam titled
'Intuitionisme en Formalisme', 1912.)
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). 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*.
The point about methods of construction (i.e. of forming proofs) being
answerable to intuitions is underscored by Brouwer's criticism of Poincare's
view of mathematical induction. (Oops--typo--for "Poincare" read "Hilbert"!)
See, for example, his piece 'Mathematics and Logic', at pp.93-4 in vol.1
of his collected works.
More information about the FOM