How to formulate the P v.s. NP problem as a formal statement inside the language of set theory?

I've read a lot that some computer scientists believe that P v.s. NP could turn out to be independent of ZFC. The thing that puzzled me is how to formulate this inside the language of set theory? I was unable to find such a formulation anywhere so I'd be grateful to be pointed out where I can find it?

Solution 1:

In fact, $\mathbf{P}=\mathbf{NP}$ is an arithmetical statement. What logicians mean by that is that it can be expressed (or, more precisely, a statement "fairly trivially" equivalent to it can be expressed) using only the language of first-order arithmetic, that is, as a formal statement built from {atoms of the form $s=t$ where $s$ and $t$ are expressions built from variables (intended to range over the natural numbers) and the constant $0$ using the binary operations $+$ and $\times$} using boolean connectors and quantifiers over the natural numbers.

For example, $$ \forall p\, \forall q\, ((p\times p = 2\times q\times q) \;\Rightarrow\; (q = 0)) $$ is an arithmetical statement (expressing, essentially, the irrationality of $\sqrt{2}$).

So now there are two distinct questions:

• Why is $\mathbf{P}=\mathbf{NP}$ (easily equivalent to) an arithmetical statement?

• Why is every arithmetical statement formally expressible in the language of set theory?

Concerning the first, the key fact is that natural numbers can be used to encode finite sequences of natural numbers (there are various ways to do this, e.g. using the Chinese remainder theorem), so we can encode as arithmetical statements those that speak about (and quantify over) not only natural numbers but also finite sequences thereof. Then we can use this to encode the behavior of Turing machines (e.g., encode a Turing machine, or a partial state or partial execution trace of a Turing machine, as finite sequences of integers), polynomials over the integers, and so on: essentially anything which is "finistic", i.e., encodable using finite data, can be translated using natural numbers using enough coding.

Then we can express the statement: "for any nondeterministic Turing machine $T$ and any polynomial $f$ such that: {for any finite input $x$, either (a) there exists a valid execution trace of $T$ starting on $x$ with time length than $f(|x|)$ (where $|x|$ is the length of $x$) terminating in the result value $1$, or else (b) all execution traces of $T$ starting on $x$ have time length than $f(|x|)$ and terminate in the result value $0$}, there exists a deterministic Turing machine $T'$ and a polynomial $f'$ such that: {for any finite input $x$, the execution trace of $T$ starting on $x$ has time length less than $f'(|x|)$ and terminates in the result value $1$ in case (a) and $0$ in case (b)}". Everything in there is finistic, therefore arithmetical.

(Of course, we can simplify the above statement once we know that there exists an $\mathbf{NP}$-complete problem. But that would beg the question of why this quetion is, itself, arithmetical.)

Concerning the question of why every arithmetical statement is expressible in the language of set theory, the thing is that the set $\omega$ of natural numbers (which is identified with the smallest infinite ordinal in the orthodox view of mathematics) can be defined inside $\mathsf{ZFC}$, and so can addition and multiplication over the integers. So any arithmetical statement can be rewritten as a statement about those sets definable within $\mathsf{ZFC}$. Again, it's a matter of coding.

Of course, I'm making matters harder by going through the "arithmetical" route: you can encode Turing machines (and their execution traces, and so on) and polynomials and everything of the sort, within set theory. In fact, the orthodoxy of mathematics is that (barring exotic things from set theory itself) every mathematical object whatsoever can be "encoded" as a set, and therefore, any formalizable statement made by mathematicians, can be translated into a statement of set theory (or, for the ultra-orthodox, that it "is" a statement of set theory in the first place, and that all of mathematics is done within $\mathsf{ZFC}$).

It should be viewed as a question of encoding: much like everything a computer handles is "encoded" as a finite binary string, everything a mathematician handles is "encoded" as a set. Some (but not all) of these things can, additionally, be "encoded" as a natural number, because they are finistic in nature. So many mathematical statements are arithmetical, but all are set-theoretic. (An example of a statement with is set-theoretic but not arithmetical is the continuum hypothesis: it is not equivalent to any arithmetical statement.)

Now decidability is something different. There is a formal system for dealing with arithmetical statements, namely $\mathsf{PA}$ (:= first-order Peano arithmetic), just like there is one for dealing with set-theoretic statements, namely $\mathsf{ZFC}$. The latter is stronger than the former, in two respects: first, it can talk about more things, because not all set-theoretic statements are arithmetical; second, even among the arithmetical statements, there are some that $\mathsf{ZFC}$ can prove and that $\mathsf{PA}$ cannot (the simplest example being "$\mathsf{PA}$ does not prove $0=1$", a statement that is arithmetical because it says essentially that a Turing machine that searches for a proof of $0=1$ within $\mathsf{PA}$ never terminates, and unprovable in $\mathsf{PA}$ whereas it is provable in $\mathsf{ZFC}$).

But in real life (i.e., outside of mathematical logic), arithmetical statements that are provable in $\mathsf{ZFC}$ but not in $\mathsf{PA}$ are rare (one example is Kruskal's tree theorem; there are occasional debates on whether, for example, Fermat's last theorem is provable within $\mathsf{PA}$, but I don't think anyone seriously doubts it, even if prima facie, Wiles's proof uses techniques that goes beyond $\mathsf{PA}$).

And arithmetical statement (as opposed to general set-theoretic statements) that are unprovable in $\mathsf{ZFC}$ but still known/believed to be true because they follow from stronger systems like the addition of large cardinals, are pretty much unheard-of (I mean, there's no doubt that they exist: "$\mathsf{ZFC}$ does not prove $0=1$" is an arithmetical statement that $\mathsf{ZFC}$ does not prove and which is still known/believed to be true because it follows from the existence of inaccessible cardinals; but it is often thought that such statements simply do not occur in ordinary mathematical work unless you actively look for them).

So it is logically conceivable that neither (the arithmetical statement) $\mathbf{P}=\mathbf{NP}$ nor its negation follow from $\mathsf{ZFC}$, but I don't think anyone really believes this seriously. (Even if it does happen, it could be because $\mathbf{P}=\mathbf{NP}$ is true, there exists an algorithm solving an $\mathbf{NP}$-complete problem but $\mathsf{ZFC}$ cannot prove that; or it could be because $\mathbf{P}\neq\mathbf{NP}$ is true and $\mathsf{ZFC}$ cannot prove that.)