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: 91,322

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

Review: Samuel R. Buss, The Undecidability of $k$-Provability. [REVIEW]Alessandra Carbone - 1997 - Journal of Symbolic Logic 62 (4):1480-1481.
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 strong provability predicates and the associated modal logics.Konstantin N. Ignatiev - 1993 - Journal of Symbolic Logic 58 (1):249-290.
Undecidable theories.Alfred Tarski - 1953 - Amsterdam,: North-Holland Pub. Co.. Edited by Andrzej Mostowski & Raphael M. Robinson.
On the provability logic of bounded arithmetic.Rineke Verbrugge & Alessandro Berarducci - 1991 - Annals of Pure and Applied Logic 61 (1-2):75-93.
What is Absolute Undecidability?†.Justin Clarke-Doane - 2012 - Noûs 47 (3):467-481.
Jacques Derrida and Alain Badiou: Is there a relation between politics and time?Antonio Calcagno - 2004 - Philosophy and Social Criticism 30 (7):799-815.
On Provability Logics with Linearly Ordered Modalities.Lev D. Beklemishev, David Fernández-Duque & Joost J. Joosten - 2014 - Studia Logica 102 (3):541-566.
Four views of arithmetical truth.Charles Sayward - 1990 - Philosophical Quarterly 40 (159):155-168.
Rosser-Type Undecidable Sentences Based on Yablo’s Paradox.Taishi Kurahashi - 2014 - Journal of Philosophical Logic 43 (5):999-1017.
The decision problem of provability logic with only one atom.Vítězslav Švejdar - 2003 - Archive for Mathematical Logic 42 (8):763-768.
On predicate provability logics and binumerations of fragments of Peano arithmetic.Taishi Kurahashi - 2013 - Archive for Mathematical Logic 52 (7-8):871-880.
On first-order theories with provability operator.Sergei Artëmov & Franco Montagna - 1994 - Journal of Symbolic Logic 59 (4):1139-1153.
The modal logic of pure provability.Samuel R. Buss - 1990 - Notre Dame Journal of Formal Logic 31 (2):225-231.
Undecidability of the Real-Algebraic Structure of Scott's Model.Miklós Erdélyi-Szabó - 1998 - Mathematical Logic Quarterly 44 (3):344-348.

Analytics

Added to PP
2014-01-16

Downloads
23 (#661,981)

6 months
12 (#203,353)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

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.
Some remarks on lengths of propositional proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.

View all 15 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