4
$\begingroup$

Given a deductive system $\Lambda$, and some well-formed-formula S, one can ask the question "Is there a proof S in $\Lambda$ of length n?" If n is presented in base-1 and if all the axioms of $\Lambda$ are polynomial-time verifiable, and if $\Lambda$ is sufficiently powerful to express the verification for some NP-Complete problem like 3-SAT, this problem is known to be NP-Complete. It requires super-polynomial time if n is not.

I know how to prove this, but I am also sure that somebody else has already proven this. Can somebody direct me to an existing published reference?

Improve this question
$\endgroup$
9
  • 2
    $\begingroup$ You cannot prove this as it is false. Under the stated conditions, the problem is in NP, but it is not necessarily NP-complete. This depends on the deductive system. Also, the problem is most likely not in general solvable in deterministic exponential time when n is given in binary. $\endgroup$
    – Emil Jeřábek
    Jan 3, 2015 at 13:22
  • 2
    $\begingroup$ You can found some NP-completeness results for deductive systems in R.Pucella, Deductive Algorithmic Knowledge $\endgroup$
    – Marzio De Biasi
    Jan 3, 2015 at 19:31
  • 1
    $\begingroup$ I still do not quite understand what is the intention of the question. The way it is formulated now, the result is essentially trivial. If you want references for particular classes of systems known to be “sufficiently powerful to express the verification for some NP-complete problem”, it is folklore in proof complexity that this holds for any system of arithmetic strength; see e.g. Theorem 6.1.4 in users.math.cas.cz/~pudlak/length.pdf . $\endgroup$
    – Emil Jeřábek
    Jan 3, 2015 at 19:55
  • 2
    $\begingroup$ It is perhaps relevant to note that the problem is not known to be NP-complete for basic propositional proof systems like resolution or Frege, and while this doesn’t seem terribly interesting per se, much effort has been devoted to study of the closely related canonical disjoint NP-pairs of these systems. The keywords are “automatizable proof system” and “effective interpolation”. $\endgroup$
    – Emil Jeřábek
    Jan 3, 2015 at 20:49
  • 1
    $\begingroup$ See also math.ucsd.edu/~sbuss/ResearchWeb/kproveApprox/index.html for another related result. $\endgroup$
    – Emil Jeřábek
    Jan 3, 2015 at 20:56

1 Answer 1

Reset to default
2
$\begingroup$

See this paper: On Godel’s Theorems on Lengths of Proofs II: Lower Bounds for Recognizing $k$ Symbol Provability by Samuel R. Buss, 1995.

This paper discusses a claim made by Godel in a letter to von Neumann which is closely related to the P versus NP problem. Godel’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 Godel’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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.