2
$\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?

$\endgroup$
  • 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 '15 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 '15 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 '15 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 '15 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 '15 at 20:56
0
$\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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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