Constructive Set Theories with Restricted Induction

L. Crosilla

Joint work with M. Rathjen.

It is known that in the classical case of Kripke Platek set theory, restricting or omitting the principle of foundation gives rise to much weaker theories from a proof theoretical point of view.

It is then natural to wonder if we may obtain similar results in the case of constructive set theory. We shall show that this is indeed the case. The technique utilized for analyzing the constructive

theories, however, is different from the one used for Kripke Platek set theory. The main tool here being a quite unusual realizability interpretation, which indirectly uses Aczel’s interpretation of constructive set theory in Martin Löf type theory as well as a bisimulation relation.

Address: Dept. of Pure Mathematics, University of Leeds, Leeds LS2 9JT, UK

E-mail: pmtmlcr@amsta.leeds.ac.uk