The Computational Content of Arithmetical Proofs
Notre Dame Journal of Formal Logic 53 (3):289-296 (2012)
| Abstract | 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$ | |||||||||
| Keywords | computational content cut elimination first-order arithmetic | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,672 |
| External links |
  Try with proxy. Try with proxy. |
| Through your library | Configure |
Similar books and articlesGilles Dowek & Olivier Hermant (2012). A Simple Proof That Super-Consistency Implies Cut Elimination. Notre Dame Journal of Formal Logic 53 (4):439-456.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Andreas Weiermann (2006). Classifying the Provably Total Functions of Pa. Bulletin of Symbolic Logic 12 (2):177-190.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Grigori Mints (2012). Effective Cut-Elimination for a Fragment of Modal Mu-Calculus. Studia Logica 100 (1-2):279-287.
G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.
George Tourlakis (2010). On the Proof-Theory of Two Formalisations of Modal First-Order Logic. Studia Logica 96 (3):349-373.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the IGPL 8:733-750.
Agata Ciabattoni & Kazushige Terui (2006). Towards a Semantic Characterization of Cut-Elimination. Studia Logica 82 (1):95 - 119.
Francesco Belardinelli, Peter Jipsen & Hiroakira Ono (2004). Algebraic Aspects of Cut Elimination. Studia Logica 77 (2):209 - 240.
Analytics
Monthly downloads |
Added to index2012-09-25Total downloads5 ( #160,284 of 549,065 )Recent downloads (6 months)1 ( #63,185 of 549,065 )How can I increase my downloads? |
My notes
Discussion
