INSTITUTE of CYBERNETICS at TTU
Spring Lectures in Mathematical Logic
| Speaker: | Prof. Michael RATHJEN, University of Leeds, England |
| Place: | Room B 216, Institute of Cybernetics, Akadeemia tee 21, Tallinn, Estonia |
| Time: | Friday, May 11, 2001, 14:00 |
CONSTRUCTIVE SET THEORY
Abstract
Constructive set theory grew out of Myhill's endeavours to discover a simple formalism that relates to Bishop's constructive mathematics as ZFC relates to classical Cantorian mathematics. The novel ideas were to replace Powerset by the (classically equivalent) Exponentiation Axiom and discard full Comprehension while strengthening Collection to Full Collection. Later on Aczel modified Myhill's set theory to a system which he called Constructive Zermelo-Fraenkel set theory, CZF, and showed its constructiveness by interpreting it in Martin-Loef's type theory. The latter interpretation is in many ways canonical and can be seen as providing CZF with a standard model in type theory. Aczel then began a broad investigation of further set-theoretic principles that hold in this model.
The first part of the talk will introduce CZF and its extensions and will gauge the proof-theoretic strengths of various systems.
The second part of the talk will be concerned with large set axioms on the basis of CZF. Classically these large set axioms are equivalent to large cardinal axioms. CZF allows for a sensible theory of large sets in that many their classically known properties can be proved on the basis of CZF. On the second hand, extensions of CZF by large set axioms have comparatively little consistency strength and bear interesting relations to (classical) recursively large ordinals via realizability interpretations.
The third part will focus on recent work on constructive set theories without epsilon-induction and constructive set theories with the anti-foundation axiom.
About the Speaker
Michael Rathjen is one of the leading experts in modern proof theory. His most outstanding achievements belong to ordinal analysis, the most complicated and technically advanced area of the field, where exciting interplay with set theory, recursion theory and model theory comes into place. He also has made significant contributions to constructive set theory, explicit mathematics and Martin-Loef's type theory.
M. Rathjen is an editor for the Journal of Symbolic Logic.
Dr. Sergei Tupailo
Institute of Cybernetics at TTU
Akadeemia tee 21, 12618 Tallinn, Estonia
email: sergei@cs.ioc.ee