Re: Whither "intuitionistic"?

To: christo@nextsolution.co.jp, types@cs.indiana.edu
Subject: Re: Whither "intuitionistic"?
From: scpsg@matrix.cc.uottawa.ca (P. Scott)
Date: Mon, 20 Oct 1997 15:16:17 -0400
Delivery-Date: Mon, 20 Oct 1997 14:16:30 -0500

The word "intuitionistic" refers to L. E. J. Brouwer's Intuitionism,
an important approach to the foundations of mathematics. Although
Brouwer himself was not a supporter of formal systems, it was his
student Heyting who first gave a logical formalism for Brouwer's 
theories (with important historical precedents in work of the 
mathematician Kolmogorov).  Gentzen developed both Natural Deduction
as well as the sequent calculus, and realized in both cases that
intuitionistic logic could be easily accomodated in these formalisms
by appropriately simple restrictions.  

More information can be obtained from any recent book on proof theory
and intuitionistic mathematics, e.g. Troelstra and van Dalen's books,
or Girard-Lafont-Taylor.

			Philip Scott
			Dept. of Mathematics
			University of Ottawa