On predicative fragments of System F

  (Kazushige Terui)


It is well known that certain predicative systems, such as Goedel's T,
can be embedded into impredicative ones, such as Girard's F. This
raises a natural question concerning the converse direction: which
part of impredicativity can be reduced to predicativity (in the sense
of Martin-Loef)? While this question has been very well studied in
traditional proof theory, it is relatively recently that an analogous
problem is addressed in computer science. We here only refer to
(Aehlig 2008), which introduces a parameter-free fragment of System F
and shows that the representable functions in it are precisely the
provably total functions in an extension of Peano Arithmetic with
finitely iterated inductive definitions. This implies that the
parameter-free fragment of System F can be reduced to an iterated
version of System T.

To establish the above result, one somehow has to prove a
normalization theorem for an impredicative system inside a predicative
one. In (Akiyoshi and Terui 2016) we improved Aehlig's result in
several respects. In particular, we gave a direct predicative proof of
strong normalization by combining a simple normalization argument of
(Joachimski and Matthes 2003) with the "Omega-rule" of (Buchholz
1981), a well-known technique in ordinal analysis.

In this talk I will review the above materials and then discuss its
potential extensions.