Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, September 27, 2004 - 4:30pm

Dirk van Dalen

Utrecht University

Location

University of Pennsylvania

DRL 4C8

The basic tenet of intuitionism is that the objects of mathematics are mental creations of human beings. In 1907 Brouwer put forward the ur-intuition of mathematics as the common origin of discrete and continuous mathematics. After his first topological period Brouwer introduced a refined set of notions for intuitionistic (constructive) mathematics. The key-notion of choice sequence provided a basis for the traditional parts of mathematics (algebra, analysis, topology, measure theory, etc.). Brouwer introduced certain principles that exploit the character of choice objects, e.g. the continuity principle, transfinite induction. We will look into the justification of these principles. Somewhat later he searched for means to describe the differences between the algorithmic universe and the choice universe (the 'reduced continuum' versus the 'full continuum'). The tool he found was the 'creating subject', conveniently formulated as Kripke's Schema. We will show that the principle is not just a curiosity, but also has its role in analyzing the continuum. Brouwer's view of logic was never made explicit, but from his dissertation it appears that he had an early `proof interpretation in mind. It is likely that his requirements at the time were a bit too strong. The combination of intuitionistic logic and intuitionistic objects yields a mathematical universe that differs considerably from the traditional (Cantorian) Universe.