First Steps into Metapredicativity in Explicit Mathematics

Summary

Abstract

The system EMU of explicit mathematics incorporates the uniform construction of universes. In this paper we give a proof-theoretic treatment of EMU and show that it corresponds to transfinite hierarchies of fixed points of positive arithmetic operators, where the length of these fixed point hierarchies is bounded by ε₀.

Introduction

Metapredicativity is a new general term in proof theory which describes the analysis and study of formal systems whose proof-theoretic strength is beyond the Feferman-Schütte ordinal Γ₀ but which are nevertheless amenable to purely predicative methods. Typical examples of formal systems which are apt for scaling the initial gart of metapredicativity are the transfinitely iterated fixed point theories ID_α whose detailed proof-theoretic analysis is given by Jäger, Kahle, Setzer and Strahm in [18]. In this paper we assume familiarity with [18]. For natural extensions of Friedman's ATR that can be measured against transfinitely iterated fixed point theories the reader is referred to Jäger and Strahm [20].

In the mid seventies, Feferman [3, 4] introduced systems of explicit mathematics in order to provide an alternative foundation of constructive mathematics. More precisely, the origin of Feferman's program lay in giving a logical account of Bishop-style constructive mathematics.