Re: Whence "intuitionistic"?

To: Frank Christoph <christo@nextsolution.co.jp>
Subject: Re: Whence "intuitionistic"?
From: Jamie Andrews <andrews@csd.uwo.ca>
Date: Mon, 20 Oct 1997 15:32:17 -0400 (EDT)
Cc: types@cs.indiana.edu
Delivery-Date: Mon, 20 Oct 1997 14:33:01 -0500

> The formulation of the intuitionistic sequent calculus is due to Gentzen
> but is it also Gentzen who was responsible for coining the term
> 'intuitionistic'?...
> What was the motivation for the choice of term?...
 
     Brouwer was the first person to talk about the intuitionistic
point of view in detail (about 30 years before Gentzen), and was
responsible for coining the term; it was probably originally in
Dutch.  He found the idea of proving something via excluded
middle "anti-intuitive", because it implied that you could prove
the existence of a mathematical object with property P without
ever actually constructing a mathematical object with property P.

     Brouwer never gave explicit proof systems, since he also
rejected Hilbert's "formula game" idea, the idea that you could
do mathematics by manipulating symbols using rules.  Later,
several workers, including Heyting and Gentzen, gave proof
systems characterizing the intuitionistic point of view.
I agree with the common opinion that Gentzen's are the most
clear and elegant.

--Jamie Andrews.
` andrews at csd.uwo.ca