How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study

DOI10.2307/2586654zbMath0928.03066OpenAlexW2025478275MaRDI QIDQ4254685

Andreas Weiermann

Publication date: 9 September 1999

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2586654

zbMATH Keywords

strong normalizationsubsystems of analysiscollapsing functionsassignment of ordinalsGödel's system \(T\) of primitive recursive functionals of finite type

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35)

Related Items (8)

Combinatory logic with polymorphic types ⋮ Term extraction and Ramsey's theorem for pairs ⋮ On the Computational Content of Termination Proofs ⋮ Size-based termination of higher-order rewriting ⋮ Complexity of Gödel’s T in λ-Formulation ⋮ Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results ⋮ Finite notations for infinite terms ⋮ A Glimpse of $$ \sum_{3} $$-elementarity

Cites Work

• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Term rewriting theory for the primitive recursive functions
• A new system of proof-theoretic ordinal functions
• Consistency proof via pointwise induction
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• A new recursion-theoretic characterization of the polytime functions
• Proof-theoretic investigations on Kruskal's theorem
• Bounding derivation lengths with functions from the slow growing hierarchy
• Elementary descent recursion and proof theory
• A term rewriting characterization of the polytime functions and related complexity classes
• Proof-theoretic analysis of termination proofs
• Notation systems for infinitary derivations
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Π12-logic, Part 1: Dilators
• A Uniform Approach to Fundamental Sequences and Hierarchies
• Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa
• A system of abstract constructive ordinals
• On n-quantifier induction
• On the interpretation of non-finitist proofs–Part II

This page was built for publication: How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study