<p>See this paper: <a href="https://www.math.ucsd.edu/~sbuss/ResearchWeb/godeltwo/godeltwoBIRK.pdf" rel="nofollow noreferrer">On Godel’s Theorems on Lengths of Proofs II:
Lower Bounds for Recognizing <span class="math-container">$k$</span> Symbol Provability</a> by Samuel R. Buss, 1995.</p>

<blockquote>
  <p>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 <span class="math-container">$k$</span>-symbol provability in first-order logic can
  not be decided in <span class="math-container">$o(k)$</span> 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 <span class="math-container">$o(k/ \log k)$</span> time by a
  nondeterministic Turing machine. In addition, we prove that the
  <span class="math-container">$k$</span>-symbol provability problem is NP-complete, even for provability
  in propositional logic.</p>
</blockquote>

CC BY-SA 4.0
2019-05-26T05:47:20.250Z
2019-05-26T06:01:48.913Z
2019-05-26T06:01:48.913Z
hengxin
<p>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.</p>

<p>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?</p>

CC BY-SA 3.0
2015-01-03T13:22:46.523Z
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.
Emil Jeřábek
CC BY-SA 3.0
2015-01-03T19:20:50.213Z
@EmilJeřábek: Updated description to address your feedback.
Bill Province
CC BY-SA 3.0
2015-01-03T19:31:15.583Z
You can found some NP-completeness results for deductive systems in [R.Pucella, Deductive Algorithmic Knowledge](http://arxiv.org/abs/cs/0405038)
Marzio De Biasi
CC BY-SA 3.0
2015-01-03T19:55:44.573Z
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 http://users.math.cas.cz/~pudlak/length.pdf .
Emil Jeřábek
CC BY-SA 3.0
2015-01-03T20:05:07.957Z
@MarzioDeBiasi: These are NP-completeness results for *satisfiability* problems (just like the original Cook’s theorem), this has nothing to do with the length of proofs.
Emil Jeřábek
CC BY-SA 3.0
2015-01-03T20:49:03.363Z
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”.
Emil Jeřábek
CC BY-SA 3.0
2015-01-03T20:56:02.360Z
See also http://www.math.ucsd.edu/~sbuss/ResearchWeb/kproveApprox/index.html for another related result.
Emil Jeřábek
CC BY-SA 3.0
2015-01-04T00:27:54.380Z
@EmilJeřábek: The purpose was indeed to find a viable reference stating as much.  The statement, as written, is indeed rather obvious, but I did not find this problem listed in Karp's 21 initial NP-Complete problems or elsewhere immediately.  The text by Pudlak is sufficient -- particularly since I can follow its bibliography for more references.  Thanks.
Bill Province
CC BY-SA 3.0
2015-08-13T02:18:00.750Z
reminds me of [fagins thm](https://en.m.wikipedia.org/wiki/Fagin%27s_theorem)
vzn
<reference-request><np-complete><automated-theorem-proving>
Looking for reference on NP-Completeness of proofs of length n
Bill Province
# Looking for reference on NP-Completeness of proofs of length n

(Asked by: username_0 on 2015-01-03)

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?

**Tags:** reference-request, np-complete, automated-theorem-proving

> **Comments:**
> **username_1**: 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.  
> **username_0**: @EmilJeřábek: Updated description to address your feedback.  
> **username_2**: You can found some NP-completeness results for deductive systems in [R.Pucella, Deductive Algorithmic Knowledge](http://arxiv.org/abs/cs/0405038)  
> **username_1**: 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 http://users.math.cas.cz/~pudlak/length.pdf .  
> **username_1**: @MarzioDeBiasi: These are NP-completeness results for *satisfiability* problems (just like the original Cook’s theorem), this has nothing to do with the length of proofs.  
> **username_1**: 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”.  
> **username_1**: See also http://www.math.ucsd.edu/~sbuss/ResearchWeb/kproveApprox/index.html for another related result.  
> **username_0**: @EmilJeřábek: The purpose was indeed to find a viable reference stating as much.  The statement, as written, is indeed rather obvious, but I did not find this problem listed in Karp's 21 initial NP-Complete problems or elsewhere immediately.  The text by Pudlak is sufficient -- particularly since I can follow its bibliography for more references.  Thanks.  
> **username_3**: reminds me of [fagins thm](https://en.m.wikipedia.org/wiki/Fagin%27s_theorem)  

---

## 1 answers

### Answer by username_4 on 2019-05-26. Score: 2

See this paper: [On Godel’s Theorems on Lengths of Proofs II:
Lower Bounds for Recognizing $k$ Symbol Provability](https://www.math.ucsd.edu/~sbuss/ResearchWeb/godeltwo/godeltwoBIRK.pdf) 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.


---

