Talk: Ryota Akiyoshi (Waseda University/Keio University, Japan)
Takeuti’s argument of the well-foundedness of ordinals up to the epsilon_0
Gaisi Takeuti (1926-2017) is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. In 1950—60’s, he provided several partial solutions to his conjecture that the cut-elimination theorem holds for it. For the crucial part of the proof, he invented a new system of ordinals called “ordinal diagrams” and presented several proofs of the well-foundedness of it. From a philosophical point of view, such proofs of the well-foundedness must be examined carefully since this is exactly the point which must be beyond Hilbert’s finitism.
In this talk, we focus on his argument of the well-foundedness of ordinals up to the epsilon_0 in his well-known book “Proof Theory” (1975, 1987) as a starting point. The structure of the argument is deserved to be examined even though Takeuti says his argument is more clear than Gentzen’s well-known argument in 1943 since some parts of it lack precise formulations. Hence, we address this issue in the detail and try to specify a suitable meta-theory for it.
This is joint work with Andrew Arana.