Re: Whither "intuitionistic"?

To: christo@nextsolution.co.jp (Frank Christoph)
Subject: Re: Whither "intuitionistic"?
From: "Jonathan P. Seldin" <seldin@alcor.concordia.ca>
Date: Mon, 20 Oct 1997 14:14:43 -0400
Cc: types@cs.indiana.edu
Delivery-Date: Mon, 20 Oct 1997 13:15:21 -0500
In-Reply-To: <199710201340.IAA02842@cs.indiana.edu>

>The formulation of the intuitionistic sequent calculus is due to Gentzen
>but is it also Gentzen who was responsible for coining the term
>'intuitionistic'?

I don't think this is true; I think Gentzen was simply giving a new
formulation to the formal calculus developed by Heyting to represent the
logic used by the Dutch school called "Intuitionism" by its founder,
Brouwer.  I don't think Gentzen has any responsibility for the use of the
term "intuitionistic".

These days, the word "constructive" is probably more in use (except where
the terminology is determined by history).  The "intuitionistic" calculus
is constructive in the sense that if |- (\Exists x)A(x) then there is a
term t (which can be calculated from the proof in a finite number of steps)
such that |- A(t).

Jonathan P. Seldin                                      tel: 514-848-3254
Department of Mathematics                       seldin@alcor.concordia.ca
Concordia University                         seldin@poincare.concordia.ca