A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity

DOI10.1007/s001530050075zbMath0889.03049OpenAlexW2027585565MaRDI QIDQ1374676

Andreas Weiermann

Publication date: 10 December 1997

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001530050075

zbMATH Keywords

collapsing functiontermination proofsordinal assignmentessentially less than

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) First-order arithmetic and fragments (03F30) Recursive functions and relations, subrecursive hierarchies (03D20) Functionals in proof theory (03F10) Complexity of proofs (03F20)

Related Items

Term rewriting theory for the primitive recursive functions, Continuous normalization for the lambda-calculus and Gödel's T, A Glimpse of $$ \sum_{3} $$-elementarity