Lectures on Constructive Set Theory

(Padua, Spring 1998)

Lecture 2: 6th May (16.30 - 18.00): Introduction, continued

We continue with our list of possible principles for constructive mathematics.

3. Constructions as Algorithms Principle

A construction of an object must provide an algorithm for producing the object.

This principle links constructive mathematics with computability. The Russian school use Church's Thesis so that they identify constructions with programs in a suitable programming language.

The following supplementary principle should perhaps have its own heading.

3a. Determinateness of Constructions

A construction must be determinate.

So, for example, a construction of an object in {0,1} must, in principle, determine which object, 0 or 1, it is. If we define b=0, if A and b=1 otherwise, where A is a mathematical proposition, then we do not have a construction until either A has been proved or A has been refuted.

4. Vicious Circle Principle

Impredicative definitions should not be used; i.e. an object d should not be defined in terms of a set D which has among its elements the object d.

In particular a set A of natural numbers should not be defined using quantifiers, (for all sets X of natural numbers) or (for some set X of natural numbers), which quantify a variable X that ranges over all sets of natural numbers. (Here d is the set A and D is the `set' of all sets of natural numbers.)

Such definitions have been thought to give rise to semantic paradoxes. The concept of impredicativity was first considered in the early parts of this century by Poincare, Russell, Weyl and others. In the 1960s a precise characterisation of `classical predicative mathematics' was formulated by Feferman and Schutte.

Constructive mathematicians have often been ambiguous about this principle. Martin-Lof's approach to constructive mathematics takes the principle very seriously.

5. Disjunction Principle

In order to show that a disjunction [A or B] of two mathematical propositions A,B it is necessary to choose one of them and show the proposition that was chosen.

This principle can be viewed as a consequence of the constructive existence principle and the determinateness of constructions (as described after the statement of the constructions as algorithms principle), using the following equivalence.

[A or B] <-> (exists x in {0,1})[ ((x=0) -> A) & ((x=1) -> B)]

As a consequence of the disjunction principle we can only show that [A or not A], for a mathematical proposition A, by either showing that A or showing that not A. As there are many mathematical propositions that have not been decided we do not have the general validity of the law of excluded middle, one of the fundamental principles of traditional logic that, until this century, has been accepted as one of the correct logical laws for use in mathematical reasoning.

It was Brouwer who first realised that in constructive mathematics some traditional methods of reasoning are suspect. Eventually a new non-classical logic, Intuitionistic Logic, was formulated (not by Brouwer, but by his student Heyting).

The constructive approach to Dedekind Cuts

We follow chapter 1 of Rudin(1964).

Rudin(1964) Principles of Mathematical Analysis, McGraw-Hill, 2nd edition.

Definition 1.4: If A is a set of rational numbers then A is a cut if

(I): (exists s)(s:A) & (exists t)( not t:A)
(II): [p:A & q < p] => [q:A]
(III): [p:A] => (exists q:A)[p < q]

We also need to consider a classically equivalent definition obtained by replacing (II) by (II').

(II'): [q < p] => [q:A or not p:A]

We will call A a cut' if the conditions (I), (II') and (III) hold. That (II)<=>(II') uses the classically correct logical law

[B or not C] <==> [B => C]

While the implication from left to right is constructive the implication from right to left is not. So, constructively, while every cut' is a cut, we are not able to assert that every cut is a cut'.

Project

Work through chapters 1 and 2 of Rudin(1964) determining to what extent the results are constructive or can be made constructive.

The first non-constructive step in Rudin(1964) is the following result.

Theorem 1.10 Let A and B be cuts. Then

[A=B or A< B or B < A].

Classical Proof: If not [A=B] then either

there is p:A such that not(p:B)

there is p:B such that not(p:A).

In the first case [B < A] and in the second case [A < B]. The result follows.

This argument uses the following non-constructive laws of classical logic.

not[A & B] ==> [(not A) or (not B)]
not (for all x)[P(x) => Q(x)] ==> (exists x)[P(x) & (not Q(x))]
[(not A) => B] ==> [A or B]

Note that, for cuts A,B

[A=B] <==> (for all r)[r:A <=> r:B]
[A < B] <==> (exists r:B)[ not r:A]

Exercise: Make explicit the use of the above logical laws in the classical proof.

The next place where classical reasoning is used in Rudin(1964) is in Theorem 1.15.Here is a minor rephrasing of this.

Theorem 1.15 Let A be a cut. Then

(for all r>0)(exists p:A)(exists q < p+r)[not q:A]

The following dates should be included in lecture 1 in the list of dates concerning the set theoretic way of thinking.

Dedekind(1857): Dedekind introduces congruence classes in place of specific residues.
Dedekind(1877): Dedekind introduces ideals as certain sets of algebraic integers instead of Kummer's ideal numbers. The ideal numbers were invented in Kummer(1844).
Kronecker(1882): Kronecker presents his own theory of fields and algebraic integers, which he had been developing for decades. His theory included an equivalent approach to the unique prime factorisation problem to that of Kummer and Dedekind.

See Lecture 3

Draft. Last Revised: 18th May, 1998.