A proof of strongly uniform termination for Gödel's T by methods from local predicativity |
| |
Authors: | Andreas Weiermann |
| |
Institution: | Institut für Mathematische Logik und Grundlagenforschung der Westf?lischen Wilhelms-Universit?t Münster, Einsteinstrasse 62, D-48149 Münster, Germany, DE
|
| |
Abstract: | We estimate the derivation lengths of functionals in G?del's system of primitive recursive functionals of finite type by a purely recursion-theoretic analysis of Schütte's 1977 exposition of
Howard's weak normalization proof for . By using collapsing techniques from Pohlers' local predicativity approach to proof theory and based on the Buchholz-Cichon
and Weiermann 1994 approach to subrecursive hierarchies we define a collapsing f
unction
so that for (closed) terms of G?del's we have: If reduces to then By one uniform proof we obtain as corollaries: A derivation lengths classification for functionals in , hence new proof of strongly uniform termination of . A new proof of the Kreisel's classific
ation of the number-theoretic functions which can be defined in , hence a classification of the provably total functions of Peano Arithmetic. A new proof of Tait's results on weak normalization
for . A new proof of Troelstra's result on strong normalization for . Additionally, a slow growing analysis of G?del's is obtained via Girard's hierarchy comparison theorem. This analyis yields a contribution to two open pro
blems posed by Girard in part two of his book on proof theory. For the sake of completeness we also mention the Howard Schütte
bound on derivation lengths for the simple typed -calculus.
Received August 4, 1995 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|