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

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.

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.

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.

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).

**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]

[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'.

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)

or

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]

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

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.

Draft. Last Revised: 18th May, 1998.