Abstract
This paper discusses a claim made by Gödel in a letter to von Neumann which is closely related to the P versus NP problem. Gödel’s claim is that k-symbol provability in first-order logic can not be decided in o(k) time on a deterministic Turing machine. We prove Gödel’s claim and also prove a conjecture of S. Cook’s that this problem can not be decided in o(k/ log k) time by a nondeterministic Turing machine. In addition, we prove that the k-symbol provability problem is NP-complete, even for provability in propositional logic.
*Supported in part by NSF grants DMS-8902480 and DMS-9205181.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. L. Bonet, Number of symbols in Frege proofs with and without the deduction rule, in Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Krajíček, eds,, Oxford University Press, 1993, pp. 61 – 95.
S. R. Buss, On Gödel’s theorems on lengths of proofs I: Number of lines and speedup for arithmetics. To appear in Journal of Symbolic Logic.
S. R. Buss, The undecidability of k -provability, Annals of Pure and Applied Logic, 53 (1991), pp. 75 – 102.
P. Clote and J. Krajíček, Arithmetic, Proof Theory and Computational Complexity, Oxford University Press, 1993.
S. A. Cook, Computational complexity of higher type functions, in Proceedings of the International Congress of Mathematicians, 1990, pp. 55 – 69.
S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic, 44 (1979), pp. 36 – 50.
M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
J. Hartmanis, Gödel, von Neumann and the P=?NP problem, Bulletin of the European Association for Theoretical Computer Science (EATCS), 38 (1989), pp. 101 – 107.
J. Hopcroft, W. Paul, and L. Valiant, On time versus space, J. Assoc. Comput. Mach., 24 (1977), pp. 332 – 337.
S. C. Kleene, Introduction to Metamathematics, Wolters-Noordhoff and North-Holland, 1971.
R. A. Reckhow, On the Lengths of Proofs in the Propositional Calculus, PhD thesis, Department of Computer Science, University of Toronto, 1976. Technical Report #87.
J. I. Seiferas, M. J. Fisher, and A. R. Meyer, Separating nondeterministic time complexity classes, J. Assoc. Comput. Mach., 25 (1978), pp. 146 – 167.
M. Sipser, The history and status of the P versus NP question, in Proceedings of the 24-th Annual ACM Symposium on the Theory of Computing, 1992, pp. 603–618.
R. Statman, Complexity of derivations from quantifier-free Horn formulae, mechanical introduction of explicit definitions, and refinement of completeness theorems, in Logic Colloquium’76, North-Holland, 1977, pp. 505 – 517.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Birkhäuser Boston
About this paper
Cite this paper
Buss, S.R. (1995). On Gödel’s Theorems on Lengths of Proofs II: Lower Bounds for Recognizing k Symbol Provability. In: Clote, P., Remmel, J.B. (eds) Feasible Mathematics II. Progress in Computer Science and Applied Logic, vol 13. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-2566-9_4
Download citation
DOI: https://doi.org/10.1007/978-1-4612-2566-9_4
Publisher Name: Birkhäuser Boston
Print ISBN: 978-1-4612-7582-4
Online ISBN: 978-1-4612-2566-9
eBook Packages: Springer Book Archive