FOM: more on intuitionism

[Colin McLarty]

Reply to message from neilt at mercutio.cohums.ohio-state.edu of Tue, 08 Sep
>
>I think Colin might have been missing my point here. I had no problem
>with the original verb "create", and would have no problem with his
>suggested replacement verb "construct". The problem I was raising was
>with the allegedly Brouwerian analysis of 
>
>	"knowing that A" 
>as
>	"creating/constructing an *intuition of* A". 
>
>It was the latter phrase with which I was taking issue.  I wrote

	I take it the issue here is constrasting "of" and "that", in the phrases
"intuition of" and "knowledge that". And I certainly agree with your claim
(a few lines farther down in your post) that Brouwer deals with "intuitions
of" rather than "intuitions that".

	What I am saying here is quite analogous to this: John says "I know that
ducks have feathers". Bill asks "how do you know". John says "When I see
ducks, I see their feathers". John knows *that* ducks have feathers, by having
intuitions (in this case sensuous) *of* the feathers of ducks.

	I take this as a common view of how we best know that ducks
have feathers. And I take it that, for Brouwer, the only way to know a 
mathematical fact A is to construct an intuition of the objects involved
showing the inevitability of A.
	

>First, there is absolutely no mention of "sin" in Brouwer's article
>"The unreliability of the logical principles".

	In your follow-up post you note that the essay does indeed
mention sin. Thank you. 

>Colin, what do *you* think Heyting was up to when he developed the
>formal intuitionistic logic of constructions? Was he "explicating"
>something to be found (albeit only seminally) in Brouwer's thought? Or
>was Heyting simply way off-mark in his attempted exegesis and
>reconstruction of Brouwerian thinking? 

	Evidently this is an inclusive "Or". I believe Heyting
was explicating something he found in Brouwer's thought, and which
Brouwer insisted was not there. The explication is pretty far off
the mark of Brouwer's thinking.

>with what justification
>would anyone nowadays regard modern, post-Heyting intuitionism as a
>school of thought that Brouwer *founded*?

	Well, Brouwer was Heyting's teacher, and helped Heyting in his career.
Brouwer got people wondering what math would be like without the law of
excluded middle and the comprehension axiom. Things like that.

>Turning to the paper that Colin cites, we find Brouwer posing
>the following question: 
>
>BEGIN QUOTE
>'Is it allowed, in purely mathematical constructions and
>transformations, to neglect for some time the idea of the mathematical
>system under construction and to operate in the corresponding
>linguistic structure, following the princ[i]ples of *syllogism*, of
>*contradiction* and of *tertium exclusum*, and can we then have
>confidence that each part of the argument can be justified by
>recalling to mind the corresponding mathematical construction?'
>	Here it will be shown that this confidence is well-founded
>for the first two principle, but not for the third.
>END QUOTE
>
>Thus Brouwer is saying that "operations in the linguistic structure"
>(i.e., the steps of inference within arguments or proofs couched in
>language) CAN proceed by means of the principles of "syllogism" and
>"contradiction". "Each part" of such an argument would enable one, he
>says, to "[recall] to mind the corresponding mathematical
>construction", and it is THIS that would JUSTIFY it!

	Yes, "operations in the linguistic structure" are, according to Browuer,
the ersatz that people persistently try to palm off in place of real,
intuitive mathematics. Unlike constructions, they proceed by rules of
inference such as the syllogism. 

	According to Brouwer these linguistic considerations cannot themselves
JUSTIFY a mathematical claim. If we could bring to mind a "corresponding
mathematical construction", then the claim would be justified by that
construction--a construction in intuition.

>So I stand firmly by my earlier suggestion as to how modern
>intuitionistic proof theory explicates Brouwer's thought on these
>matters. Not to concede this would be to deprive Brouwer of his
>historical status as the founding father of intuitionist
>mathematics. If Colin can't appreciate the conceptual explication
>involved, then he will be left wth Brouwer's deviant mathematics and
>esoteric philosophy, on the one hand, completely divorced from modern
>intuitionistic mathematics and its re-vamped foundation in a
>neo-Wittgensteinian theory of meaning, on the other.

	I will be barred from attributing certain ideas to Brouwer, ideas
that he derided. This will not prevent me learning those ideas.

        Modern intuitionistic mathematics begins with Heyting's
formalization of intuitionistic logic. And Heyting tells us what Brouwer
thought of that: "He always maintained that formalization is unproductive, a
sterile exercise. He never changed his mind about that" (Heyting said this
and similar things several times in interviews in 1967 and 1976, quoted in
van Stigt 1990, _Brouwer's Intuitionism_, p.290). 

 In such a
>situation, the history of twentieth century mathematical thought would
>have to be rewritten so that Dummett figured as the real founding
>father of modern intuitionism, despite the fact that Dummett was not
>just being modest in taking himself to be explicating the thought of
>Brouwer!

        Dummett says Brouwer founds intuitionism on time intuition, which
need not be invoked at all for Dummett's version. (_Elements of
intuitionism_ Oxford:Clarendon Press, 1977, p.32). Dummett substitutes a
more proof-theoretic intuition, which is how this thread got started--Tait
said that founding intuitionism on proofs suits Dummett but not Brouwer.
Tait was right.

	As to the "founding father of modern intuitionism" I might name a few
others before Dummett. Troelstra comes to mind. Erret Bishop. Many proof
theorists. Dummett has been very important among philosophers drawn towards
intuitionism, but I don't think of him as founding the modern mathematical
work on the subject.

Colin McLarty