The Computational Content of Arithmetical Proofs

Notre Dame Journal of Formal Logic 53 (3):289-296 (2012)
  Copy   BIBTEX


For any extension $T$ of $I\Sigma_{1}$ having a cut-elimination property extending that of $I\Sigma_{1}$ , the number of different proofs that can be obtained by cut elimination from a single $T$ -proof cannot be bound by a function which is provably total in $T$.



    Upload a copy of this work     Papers currently archived: 92,197

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

41 (#390,173)

6 months
7 (#438,648)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Untersuchungen über das logische Schließen. I.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 35:176–210.
Die Widerspruchsfreiheit der reinen Zahlentheorie.Gerhard Gentzen - 1936 - Journal of Symbolic Logic 1 (2):75-75.
On the interpretation of intuitionistic number theory.S. C. Kleene - 1945 - Journal of Symbolic Logic 10 (4):109-124.
On the interpretation of non-finitist proofs–Part II.G. Kreisel - 1952 - Journal of Symbolic Logic 17 (1):43-58.

View all 8 references / Add more references