Expressing P = NP as a first order formula

I want to express P = NP in a completely formal way. My first try:

There exists an algorithm A and a polynomial bound p such that for all input i, A(i) = true iff i is a satisfiable formula and the running time of A on i is bounded by p(|i|).

My goal is to reach a first order formula. Then come the problems: How do I express an algorithm? How to express "algorithm A accepts input i in p(|i|) steps"? How to express "input i is a satisfiable formula"?

So my question is

Please give a first order formula expressing the statement P = NP.

-
First-order formula in what language? – Yuval Filmus Jul 16 '11 at 6:47
To add on Yuval's comment: Let $\mathcal L$ be our language with relations $P,NP,\in$. Here is the formulation of $P=NP$ in first order: $\forall x(P(x)\leftrightarrow NP(x))$. – Asaf Karagila Jul 16 '11 at 7:54
@Raphael: one can quantify over algorithms by quantifying over natural numbers. – Carl Mummert Jul 16 '11 at 11:33
@Raphael: you don't need actual "functions" just to say that a certain algorithm halts on a certain input in a certain number of steps. That question is, essentially, syntactic: it can be checked by writing the computation history for the algorithm for a certain number of steps and then checking whether the algorithm halted at the end of the history. The history itself can be coded as a finite sequence of natural numbers, and in arithmetic there are ways to quantify over finite sequences of numbers. – Carl Mummert Jul 16 '11 at 12:52
So which language? I'm mainly interested in the complexity of the statement, i.e. whether it's $\Pi_2$ or $\Sigma_2$ or others. I'm reading Thomas Jech's Set Theory, so I want to know whether the statement is absolute, i.e. whether it's $\Delta_0$. I'm not sure if a formula of the form $\forall x\in\mathbb N[P(x)]$ is $\Delta_0$. – Zirui Wang Jul 17 '11 at 6:34

The question is which language you want to use to express it. It can be expressed in the language of Peano arithmetic, and hence in other theories that interpret Peano arithmetic, such as ZFC.

The key is to use techniques like the ones for Kleene's $T$ predicate to formalize computability in arithmetic. Using these coding techniques, it is straightforward but long to write formulas of arithmetic that define each of the predicates:

• $\Phi(e,s,i,j)$ which says that that Turing machine with index $e$ halts in $s$ steps on input $i$ without output $j$

• $\Psi(e,s,i,j)$ which says that the nondeterministic Turing machine with index $e$ has at least one halting computation with $s$ steps on input $i$ without output $j$

• $\Theta(a, s, i)$ which says that if $a$ is read as a code for a polynomial $p(x)$ over $\mathbb{N}$ then $s < p(i)$. For example, we might factor $a$ into prime powers, $a = 2^{a_0}3^{a_1}\cdots r^{a_n}$, and let $p(x) = a_0 + a_1 x + a_2x^2 + \cdots + a_nx^n$.

To express $P = NP$, you can use these formulas to directly express the statement "If $e$ is a nondeterministic Turing machine that runs with some polynomial time bound, then there is a deterministic Turing machine $e'$ that runs in polynomial time and computes the same values as $e$."

It is also possible, using the same methods, to write a formula $\Sigma(a)$ which says that if $a$ is viewed as a code for a propositional formula then this formula is satisfiable (remember that an interpretation of a propositional formula is just a finite list of truth values for its variables). Then you can use $\Sigma$ to express "There is a Turing machine which solves the satisfiability problem in polynomial time".

-
My only remaining question is: How is this T defined? – Zirui Wang Jul 18 '11 at 8:13
@Zirui Wang: the definition of $\Phi$ says: there is a finite sequence of natural numbers of length $s$, each of element which is the code for a particular state of a computation of Turing machine $e$, such that the first element of the sequence codes the machine in its starting state on input $i$, each succeeding element of the sequence is obtained by running the machine one step from the previous element, and the final element of the sequence shows the machine halting with output $j$. All these predicates can be defined in the language of arithmetic. – Carl Mummert Jul 18 '11 at 14:51