This topic originated at the turn of the century with Russell's attempt to resolve his paradox through his `vicious Circle Principle' that `no totality can contain members defined in terms of itself'.
The project could trace the history of this idea through the debate with Poincare, Russell and Whitehead's Principia Mathematica with its Theory of Types and the Axiom of Reducibility and the work of Weyl in the first part of the century, through the more recent work of Schutte and Feferman on a precise concept of Predicative Mathematics, to the present day issues in the Foundations of Constructive Mathematics. A more narrowly conceived project could focus on one or other technical aspect of this topic.
Intuitionistic logic is the subsystem of classical logic that was
first axiomatised by Heyting as the correct logic for the
intuitionistic approach to mathematics initiated by Brouwer. Over the
years many styles of complete semantics for intuitionistic logic have
been developed; e.g. algebraic, topological, Beth trees, Kripke
structures, realisability, categorical, type theoretical, etc ... .
The aim of the project is to survey and relate these semantics for
intuitionistic propositional logic
There are several standard approaches to the construction of the
complete ordered field of real numbers, perhaps the two main ones
being Cantor's Cauchy sequence approach and the other being the
Dedekind cut approach. As the theory of complete ordered fields is
categorical (i.e. not only is there a model, but any two models are
isomorphic) all approaches are equivalent.
The constructive approach to mathematics was mainly initiated by
Brouwer in the context of his arguably rather obscure Intuitionistic
Philosophy of Mathematics, but was developed in a more straightforward
way by the American analyst Errett Bishop and his followers. Both
Brouwer and Bishop construct the reals using Cauchy sequences. But
Dedekind cuts can also be used if one is careful. With care the
`complete ordered field' categorical axiom system can be carried over
to constructive mathematics. But the Cauchy sequence and Dedekind cut
approaches give distinct notions of completeness that can only be
shown to agree on the assumption of the countable axiom of
choice. This axiom is usually assumed in constructive mathematics, but
there are good reasons to avoid using it whenever possible and then we
get two consistently distinct categorical axiomatisations of the
reals.
The aim of this project is to present some of the details of the above
ideas. To do this project it will be necessary to get an intuitive
understanding of when an informal mathematical proof is constructive.
A topic arising out of my Types course. The precise topic will be
determined by consultation.
Further project topics may become available over the next few weeks.
Check my web page http://www.cs.man.ac.uk/~petera/index.html
2) A survey of the variety of semantics for intuitionistic
propositional logic.
3) The constructive real numbers
4) Dependent Type Theory