Semianrio: “‘Proofs as Programs’ Revisited”

Mercoledì 7 Febbraio 2018, ore 16:00 - Aula 1BC45 - Ryota Akiyoshi


Mercoledì 7 Febbraio 2018 alle ore 16:00 in Aula 1BC45, Ryota Akiyoshi (Waseda University) terrà un seminario dal titolo “‘Proofs as Programs’ Revisited”.

Schwichtenberg has developed the program called “Proofs as Programs" by measuring the “complexity as programs” of proofs in an arithmetical system (with recursion). Technically, he used a slow growing hierarchy to “clime down” tree ordinals, which are introduced by Buchholz. This observation is due to Arai and is going back to Girard’s “Hierarchy comparison theorem”.
In this talk, we sketch another approach to this program by focusing on parameter-free subsystems of Girard’s F. There are at least two advantages in this approach. (i) Our approach is simpler and smoother than the original one. (ii) It is relatively easy and uniform to extend our results to stronger fragments (corresponding to iterated inductive definitions) though the theory analysed by Schwichtenberg has the strength of Peano Arithmetic.