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

Until about the 1850s (?) neither

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

- It admits of far reaching abstractions such as that of the `actual infinity' of ``completed'' infinite collections of simultaneously existing objects.
- It admits of the free application of the usual rules of traditional logic in arguments about infinite collections.

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

- Concreteness
- Constructive Existence
- Constructions as Algorithms
- Vicious Circle
- Disjunction
- ...

Some versions of constructivism accept this principle:-

- Kronecker's mathematics
- Hilbert's Finitism
- Russian constructivism (The Markov school)

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

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.