Lectures on Constructive Set Theory

(Padua, Spring 1998)

Lecture 1: 29th April (16.30 - 18.00): Introduction, first part

These notes are a rather rough summary of the lecture!

Constructive Set Theory is a theory of sets that is founded on a particular version of constructive mathematics - the version that has been developed by Per Martin-Lof over nearly 30 years and has been called

Warning: This introduction and the rest of part I of these lectures is not intended to be either fully rigorous or historically accurate, but may be somewhat superficial about historical facts, as I have not always consulted the primary literature. The main purpose of Part I is to provide sufficient background to Part II, which will be more rigorous and will be concerned with an axiomatic approach to constructive set theory.

Can there be a constructive theory of sets?

Until the 1960s it was thought that the essential features of classical set theory were necessarily incompatible with constructive mathematics.

Until about the 1850s (?) neither

-significant set theoretical ideas

nor

-significant constructivist ideas

can be distinguished in the mathematical literature.

In some sense all of mathematics was constructive. (But perhaps not in any of the modern senses of `constructive'. It would be interesting to make a historical investigation to work out in what sense pre 1850s mathematics was constructive.)

The Set Theoretic way of thinking

What is the essence of the `set theoretic' way of thinking that seems to have originated in the second half of the 19th century? Some dates:-
Galileo(1638)
(Discussion of infinite sets)
Bolzano(1851)
(Discussion of infinite sets and the fact that they can be in one-one corrspondence with a proper part of themselves. A set was defined to be a collection, given by a property consisting of `parts' (i.e. elements) whose `ordering' is irrelevent. (i.e. sets are extensional))
Dedekind(1872)
Continuity and Irrationals. (Defines real numbers as `Dedekind cuts'. The ideas for this started in 1858. Uses the words `system'/`domain' for the set of rational numbers. A cut is a pair of `classes' of rational numbers, the left and right parts of the cut, satisfying the standard conditions.)
Cantor(1874)
(The paper that can be said to start `set theory'. - Cantor defines the notion of a countable set and shows that the set of real numbers is uncountable while the set of algebraic reals is countable)
Cantor(...)
Further papers of Cantor on transfinite numbers (cardinal numbers and ordinal numbers)
Dedekind(187?) Dedekind invents his notion of ideal as an improvement for Kummer's notion of an ideal number. See Dedekind(1887). Kummer invented his notion in order to get a good theory of unique factorisation for certain rings where unique factorisation in the normal sense does not hold. Dedekind replaces Kummer's more concrete, but morer obscure and clumsy notion by a simple set theoretic one.
Dedekind(1888)
The Nature and Meaning of Numbers. (Introduced the Dedekind-Peano axiomatisation of the natural numbers. Again uses the word `system'. An object of our thought is called a thing. Whenever different things a,b,c,... can, for some reason, be associated in the mind then they form the elements of a system. A system is itself a thing. Symbols, such as a,b,c, ..., are used to designate things. `(a=b)' expresses that the symbols a,b designate the same things. A system is defined to be infinite if it is in one-one correspondence with a proper part of itself.)
Peano 1888
(Introduced many of the standard concepts and notations of set theory)
See References and Some of Cantor's papers

Some possible principles for constructive mathematics

Not all of these principles are accepted in all forms of constructive mathematics.
  1. Concreteness
  2. Constructive Existence
  3. Constructions as Algorithms
  4. Vicious Circle
  5. Disjunction
  6. ...

1. The Concreteness Principle

Only concretely given finite objects should be dealt with in mathematics.

Some versions of constructivism accept this principle:-

Functions and classes have to be given in finite terms by formulae/algorithms. e.g. Kronecker (1886):- But other versions of constructivism do not accept the principle. For example they allow abstract objects such as arbitrary (but constructive) functions.

2. Constructive Existence Principle

To show that an object satisfying some property exists it is necessary to give a construction of an object and show that the object has the property.

But what is a construction?

Note That `construction' can refer both to a process and also to the result of carrying out a process.

Brouwer views a construction as something in the mind - `mental construction'. Others focus on a syntactic representation; i.e. a definition or algorithm.

References

Lecture 2

Draft. Last Revised: 5th May, 1998.