Re: Whither "intuitionistic"?
>The formulation of the intuitionistic sequent calculus is due to Gentzen
>but is it also Gentzen who was responsible for coining the term
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
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 firstname.lastname@example.org
Concordia University email@example.com