The undecidability of k-provability

Annals of Pure and Applied Logic 53 (1):75-102 (1991)
  Copy   BIBTEX

Abstract

Buss, S.R., The undecidability of k-provability, Annals of Pure and Applied Logic 53 75-102. The k-provability problem is, given a first-order formula ø and an integer k, to determine if ø has a proof consisting of k or fewer lines. This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula ø and an integer k such that for all n,ø has a proof of k sequents if and only if n ε X.

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(91)90059-u

Links

PhilArchive



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

External links

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

Through your library

My notes

Similar books and articles

The undecidability of k-provability.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.
A unification-theoretic method for investigating the k-provability problem.William M. Farmer - 1991 - Annals of Pure and Applied Logic 51 (3):173-214.
Provability logics with quantifiers on proofs.Rostislav E. Yavorsky - 2001 - Annals of Pure and Applied Logic 113 (1-3):373-387.
Logic of proofs and provability.Tatiana Yavorskaya - 2001 - Annals of Pure and Applied Logic 113 (1-3):345-372.
On strong provability predicates and the associated modal logics.Konstantin N. Ignatiev - 1993 - Journal of Symbolic Logic 58 (1):249-290.
Review: Samuel R. Buss, The Undecidability of $k$-Provability. [REVIEW]Alessandra Carbone - 1997 - Journal of Symbolic Logic 62 (4):1480-1481.
A modal provability logic of explicit and implicit proofs.Evan Goris - 2010 - Annals of Pure and Applied Logic 161 (3):388-403.
Realization of Intuitionistic Logic by Proof Polynomials.Sergei N. Artemov - 1999 - Journal of Applied Non-Classical Logics 9 (2-3):285-301.
ALLEN, B., Arithmetizing Uniform NC BASARAB, SA, Relative elimination of quantifiers for Hen-selian valued fields BUSS, SR, The undecidability of k-provability GALLIER, JH, What's so special about Kruskal's theorem and.A. Nesin, A. Pillay & V. Razenj - 1991 - Annals of Pure and Applied Logic 53:297.
On the provability logic of bounded arithmetic.Rineke Verbrugge & Alessandro Berarducci - 1991 - Annals of Pure and Applied Logic 61 (1-2):75-93.
The provability logic for Σ1-interpolability.Konstantin N. Ignatiev - 1993 - Annals of Pure and Applied Logic 64 (1):1-25.
Proving theorems of the second order Lambek calculus in polynomial time.Erik Aarts - 1994 - Studia Logica 53 (3):373 - 387.
A course on bimodal provability logic.Albert Visser - 1995 - Annals of Pure and Applied Logic 73 (1):109-142.
Provability algebras and proof-theoretic ordinals, I.Lev D. Beklemishev - 2004 - Annals of Pure and Applied Logic 128 (1-3):103-123.
Provability logic in the Gentzen formulation of arithmetic.Paolo Gentilini & P. Gentilini - 1992 - Mathematical Logic Quarterly 38 (1):535-550.

Analytics

Added to PP
2017-02-19

Downloads
5 (#1,544,856)

6 months
1 (#1,478,781)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Why do mathematicians re-prove theorems?John W. Dawson Jr - 2006 - Philosophia Mathematica 14 (3):269-286.
Identity of proofs based on normalization and generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
Models of Deduction.Kosta Dosen - 2006 - Synthese 148 (3):639-657.

View all 24 citations / Add more citations

References found in this work

Sets of theorems with short proofs.Daniel Richardson - 1974 - Journal of Symbolic Logic 39 (2):235-242.
A unification algorithm for second-order monadic terms.William M. Farmer - 1988 - Annals of Pure and Applied Logic 39 (2):131-174.

Add more references