Mathematical proof theory in the light of ordinal analysis

Reinhard Kahle

pp. 237-255

in: Benedikt Lowe, Florian Rudolph (eds), Foundations of the formal sciences I, Synthese 133, 2002.

Abstract

We give an overview of recent results in ordinal analysis. Therefore,we discuss the different frameworks used in mathematical proof-theory, namely subsystem of analysis including reversemathematics, Kripke–Platek set theory, explicitmathematics, theories of inductive definitions,constructive set theory, and Martin-Löf’s typetheory.