1
$\begingroup$

I am studying computational complexity using Papadimitrious's book: "Computational Complexity". I am trying to solve the final statement of Problem 8.4.9, but I am stuck and would like some hint on how to proceed.

Problem 8.4.9:

"Let $f(n)$ be a function from integers to integers. An $f(n)$-prover is an algorithm which, given any valid expression in first-order logic that has a proof in the axiomatic system in Figure 5.4 of length $l$, will find this proof in time $f(l)$. If the expression is not valid, the algorithm may either report so, or diverge (so the undecidability of validity is not contradicted).

(a) - Show that there is a $k^n$ prover, for some $k > 1$.

In a letter to John von Neumann in 1965, Kurt Gödel hypothesized that an $n^k$ prover exists, for some $k \geq 1$. For a full translation of this remarkable text, as well as for a discussion of modern-day complexity theory with many interesting historical references, see:

  • M.Sipser "The history and status of the P versus NP problem" Proc. of the 24th Annual ACM Symposium on the Theory of Computing, pp.603-618, 1992.

Problem: Show that there is an $n^k$ prover, for some $k > 1$, if and only if $P = NP$."

Figure 5.4 that he mentions contains the standard logical axioms for first-order logic (I can post the picture here, if you like).

I tried reading the mentioned article, and although it is very interesting from the historical point of view, it didn't help me figure out the solution. My first attempt was to use the result that a formula $\phi$ is valid if and only if its negation $\neg \phi$ is not satisfiable and try to connect this problem to $SAT$, which we know is $NP$-complete. However, using this result I obtain something about a formula NOT being satisfiable, while $SAT$ is about satisfiability.

Can anyone help me with this statement? Thanks in advance.

PS: Not closely related to what I am asking, but I think I was able to solve letter (a) by noticing that if a formula is valid, then we can apply the logic axioms (and the number of logic axioms is constant) without worrying about how we instantiate variables since a valid formula is true under all possible interpretations.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Given a CNF $\varphi$ over the variables $x_1,...x_n$ what's wrong with the first order formula $\exists x_1,...,x_n: \varphi$? $\endgroup$
    – Ariel
    Apr 28, 2021 at 19:19
  • 2
    $\begingroup$ Thanks, @Ariel. The formula $\exists x_1, \ldots, x_n: \phi$ is valid if and only if the formula $\phi$ is satisfiable? Is it that simple? $\endgroup$
    – Gabriel F. Silva
    Apr 28, 2021 at 20:24

1 Answer 1

Reset to default
3
$\begingroup$

An $n^k$ prover implies that the set $\{\left(\varphi,1^n\right)|\text{$\varphi$ has a proof of length $\le n$}\}$ is in $P$, since we can simply run the prover for $n^k$ steps and check whether it yields a valid proof.

It remains to show that this language is NP complete. This follows from a straightforward reduction from SAT. Given a CNF $\varphi$ over the variables $x_1,...,x_n$ return the pair $\left(\exists x_1,...,x_n: \varphi, 1^k\right)$ where $k=k(|\varphi|)$ is some upper bound on the length of the satisfiability proof for satisfiable formulas of length $|\varphi|$.

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.