As a part of our Theory Seminars, today we welcomed Ryota Akiyoshi from Waseda University, who gave a talk on Takeuti’s finitism.

Abstract: In this talk, we address several mathematical and philosophical issues of Gaisi Takeuti’s proof theory, who is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. He furthered the realization of Hilbert’s program by formulating Gentzen’s sequent calculus for higher-oder logics, conjecturing that the cut-elimination holds for it (Takeuti’s conjecture), and obtaining several stunning results in the 1950-60’s towards the solution of his conjecture.

This talk consists of two parts. (1) To summarize Takeuti’s background and the argument of the well-ordering proof of ordinals up to ε0 , (2) To evaluate it on philosophical grounds. Also, we will explain several mathematical and philosophical issues to be solved. This is joint work with Andrew Arana.

Ryota Akiyoshi

My research fields are philosophy of mathematics and logic, mathematical logic (proof theory), and theoretical computer science (type theory). The main philosophical question in my research is "what is a proof ?".