Metapredicative and Explicit Mahlo: a Proof-theoretic Perspective

Gerhard Jäger

Mahlo cardinals and their recursive analogues have played an important role in several areas of traditional logic, most prominently in set theory and recursion theory. The least recursive Mahlo ordinal, for example, is the least ordinal not recursive in Gandy’s superjump, it is the closure ordinal of several interesting nonmonotone inductive definitions, and the inital segment of the constuctible hierarchy up to this ordinal provides for the least standard model of Π_{2} reflection on admissibles.

The proof-theoretic treatment of Mahloness is more recent. First a theory for admissible sets formalizing a Mahlo universe and a corresponding subsystem of analysis were analyzed by Rathjen. Later Mahlo axioms were brought into the context of Martin-Löf type theory by Setzer. Research about Mahloness in the framework of Feferman’s explicit mathematics is based on the work by Jäger, Strahm and Studer.

In this talk we discuss several new aspects of Mahloness, in particular from the point of view of explicit mathematics. However, related principles in subsystems of second order artihmetic will also be mentioned. In doing so we will also shed some new light on metapredicativity, an interesting area of formal systems couched between what is predicative and properly impredicative.

Address: Institut für Informatik und angewandte Mathematik, Universität Bern, Neubrueckstrasse 10, CH-3012 Bern, Switzerland

E-mail: jaeger@iam.unibe.ch