Book contents
- Frontmatter
- Contents
- Preface
- Part I Invited Papers
- Part II Contributed Papers
- Gödel's Ontological Proof Revisited
- A Uniform Theorem Proving Tableau Method for Modal Logic
- Decidability of the Class in the Membership Theory NWL
- A Logical Approach to Complexity Bounds for Subtype Inequalities
- How to characterize provably total functions
- Completeness has to be restricted: Gödel's interpretation of the parameter t
- A Bounded Arithmetic Theory for Constant Depth Threshold Circuits
- Information content and computational complexity of recursive sets
- Kurt Gödel and the Consistency of R##
- Best possible answer is computable for fuzzy SLD-resolution
- The finite stages of inductive definitions
- Gödel and the Theory of Everything
- References
How to characterize provably total functions
from Part II - Contributed Papers
Published online by Cambridge University Press: 23 March 2017
- Frontmatter
- Contents
- Preface
- Part I Invited Papers
- Part II Contributed Papers
- Gödel's Ontological Proof Revisited
- A Uniform Theorem Proving Tableau Method for Modal Logic
- Decidability of the Class in the Membership Theory NWL
- A Logical Approach to Complexity Bounds for Subtype Inequalities
- How to characterize provably total functions
- Completeness has to be restricted: Gödel's interpretation of the parameter t
- A Bounded Arithmetic Theory for Constant Depth Threshold Circuits
- Information content and computational complexity of recursive sets
- Kurt Gödel and the Consistency of R##
- Best possible answer is computable for fuzzy SLD-resolution
- The finite stages of inductive definitions
- Gödel and the Theory of Everything
- References
Summary
Summary. lnspired by Buchholz’ technique of operator controlled derivations (which were introduced for simplifying Pohlers’ method of local predicativity) a straightforward, perspicuous and conceptually simple method for characterizing the provably recursive functions of Peano arithmetic in terms of Kreisel's ordinal recursive functions is given. Since only amazingly little proof and hierarchy theory is used, the paper is intended to make the field of ordinally informative proof theory accessible even to non-prooftheorists whose knowledge in mathematical logic does not exceed a first graduate level course.
Introduction and Motivation
A fascinating result of ordinally informative proof theory due to Kreisel (1952) is as follows:
Theorem: (*)
The provably recursive functions of Peano arithmetic are exactly the ordinal recursive functions.
Folklore (proof-theoretic) proofs for (*) [cf., for example, Schwichtenberg (1977), Takeuti (1987), Buchholz (1991) or Friedman and Sheard (1995) for such proofs] rely on non trivial metamathematical evaluations of the Gentzenor Schütte-style proof-theoretic analyses of Peano arithmetic. Alternatively a proof- and recursion-theoretic analysis of Gödel's 1958 functional interpretation of Heyting arithmetic can be employed for proving (*), cf. for example [Tait (1965), Buchholz (1980), Weiermann (1995)]. A proof of (*) which does not rely on metamathematical considerations - like primitive recursive stipulations of codes of infinite proof-trees - has been given in [Buchholz (1987), Buchholz and Wainer (1987)]. A proof of (*) using the slow growing hierarchy is given in [Arai (1991)]. A local predicativity style proof - which generalizes uniformly to theories of proof-theoretic strength less than or equal to K PM, cf. [Rathjen (1991)] - of (*) has been given in [Weiermann (1993), Blankertz and Weiermann (1995)]. Other proofs for (*) which are based on model theory can be found, for example, in [Hajek and Pudlak (1993)]. Buchholz (1992) introduced the technique of operator controlled derivations which allows a simplified and conceptually improved exposition of Pohlers’ local predicativity. One aim of the present paper is to give a contribution to the following question (Buchholz, private communication, 1993): Is it possible to use operator controlled derivations to give a proof for (*) - and generalizations of (*) - which is technically smooth?
- Type
- Chapter
- Information
- Gödel '96Logical Foundations of Mathematics, Computer Science and Physics - Kurt Gödel's Legacy, pp. 205 - 213Publisher: Cambridge University PressPrint publication year: 2017
References
- 1
- Cited by