[Prev][Next][Index][Thread]

Re: Whither "intuitionistic"?

>>>>> "Frank" == Frank Christoph <christo@nextsolution.co.jp> 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
    Frank> 'intuitionistic'?

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.

jmv