An Introduction To Finitary Analyses Of Proof Figures

Summary

Abstract

In this paper we expound the approach to proof theory due to Gentzen-Takeuti: the finitary analysis of proof figures using ordinal diagrams. As an example we take up theories of strength measured by the Howard ordinal. First we recall Takeuti's consistency proof for a subsystem BI of second order arithmetic in a retrospective analysis of the genesis of ordinal diagrams. Second a theory of Π₂-reflecting ordinals is analysed in the spirit of Gentzen-Takeuti. This paper is intended to be an introduction to an ongoing project of the author's, in which a proof theory for theories of recursively large ordinals is developed.

G. Gentzen published his new version of a consistency proof for first order number theory in 1938 [26]. He had already given two consistency proofs [24] and [25]. The first used a constructive but rather abstract notion of Junctionals. In the second he had first introduced transfinite ordinals in proof theory. Although he formulated the result as a consistency proof, his interest seems to involve a divergence from Hilbert's program. Concerning this development G. Kreisel [28] p. 262 wrote:

…, by introducing a quantitative ordinal measure he (=Gentzen) forces us to pay attention to combinatorial complexity and thereby makes it at least more difficult for us to slip into an abstract reading.