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
- intuitionistic/constructive type theory.
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
Until about the 1850s (?) neither
-significant set theoretical ideas
-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?
- It admits of far reaching abstractions such as that of the `actual
infinity' of ``completed'' infinite collections of simultaneously
- It admits of the free application of the usual rules of traditional
logic in arguments about infinite collections.
and Some of Cantor's papers
- (Discussion of infinite sets)
- (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
- 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.)
- (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)
Further papers of Cantor on transfinite numbers (cardinal numbers and
- 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.
- 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
Some possible principles for constructive mathematics
Not all of these principles are accepted in all forms of constructive
- Constructive Existence
- Constructions as Algorithms
- Vicious Circle
1. The Concreteness Principle
Only concretely given finite objects should be dealt with in
Some versions of constructivism accept this principle:-
Functions and classes have to be given in finite terms by
formulae/algorithms. e.g. Kronecker (1886):-
- Kronecker's mathematics
Russian constructivism (The Markov school)
But other versions of constructivism do not accept the principle. For
example they allow abstract objects such as arbitrary (but
`.... even the general concept of an infinite series ... is
... allowable only with the proviso that in each particular case
... because of the arithmetical laws governing the formation of the
(successive) terms ... certain prerequisite conditions can be
satisfied which allow the series to be considered as a finite
expression and therefore make it strictly speaking unnecessary to go
beyond the concept of a finite series.'
Brouwer's Intuitionism (Allows free choice sequences)
American constructivism (The Bishop school)
Martin-Lof's Type Theory (Essentially a formal, philosophically
motivated framework for American constructivism)
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
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.
Draft. Last Revised: 5th May, 1998.