There is an $n^k$ prover if and only if $P = NP$
I am studying computational complexity using <PERSON>'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 <PERSON> in 1965, <PERSON> hypothesized that an $n^k$ prover exists, for some $k \geq 1$. 603
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:
* <PERSON> "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. 330