Re: Whither "intuitionistic"?
Subject: Re: Whither "intuitionistic"?
From: "Jose Manuel E. Valenca" <firstname.lastname@example.org>
Date: Mon, 20 Oct 1997 18:43:51 +0100
Delivery-Date: Mon, 20 Oct 1997 12:40:43 -0500
In-Reply-To: Your message of "Mon, 20 Oct 1997 13:05:17 +0900" <199710201340.IAA02842@cs.indiana.edu>
>>>>> "Frank" == Frank Christoph <email@example.com> writes:
Frank> [------- The Types Forum ------
Frank> http://www.cs.indiana.edu/types -------] The formulation of
Frank> the intuitionistic sequent calculus is due to Gentzen but
Frank> is it also Gentzen who was responsible for coining the term
No; the term comes from Brower's Intutionistic Mathematics introduced
in his thesis "On the foundations of mathematics" in 1907. Brower
did not believe in Logic which he saw as a pure linguistic process
not essential to the foundations of the mathematical thought.
According to Ewald, the conclusion of Browers's thesis contained
"Mathematics can deal with no other matter that which it has itself
constructed. In the preceding pages it has been shown for the
fundamental parts of mathematics how they can be build by units
of perception .... while at every stage in the process complete
systems which have been constructed before can be take as new units.
...... it will be explained why no mathematics can exist which
has not been intuitively build up in this way, why consequently
the only possible foundation of mathematics must be sought
in this construction under the obligation carefully to watch
which constructions intuition allows and which not, and why any
other attempt of such foundation is condemned to failure."
(Brower "On the foundations of mathematics", 1907)
Later, in 30's Heyting and Kolmogorov introduced what is now called
"Intuitionist Logic" under Brower's guidance leading to the well
known BHK-interpretation of first order sentences.