Does Provable P equal Provable NP?

My question is a very basic one. It seems feasible to believe that $\mathsf{P = NP}$, because there is some "pathological" good algorithm for SAT, yet it is impossible to prove that the algorithm is actually correct and/or that it runs in polynomial time, in a standard axiomatic system like ZFC.

Let's fix a logic $L$ that is strong enough to encode statements about Turing machines. (Edit: I should have clarified that by this I mean the same requirements as Godel's second incompleteness theorem. For the purposes of this question, assume that $L$ proves the peano axioms PA.)

Then define \begin{align*} \mathsf{ProvableP} &:= \{A \mid L \text{ proves } [A \in P]\} \\ \mathsf{ProvableNP} &:= \{A \mid L \text{ proves } [A \in NP] \} \end{align*}

Now we have that $\mathsf{ProvableP} \subseteq \mathsf{ProvableNP} \subseteq \mathsf{NP}$. But does $\mathsf{ProvableP} = \mathsf{ProvableNP}$? How does this relate to the original P vs NP question?

Partial answer: The SAT problem is $\mathsf{ProvableNP}$-complete, but $\mathsf{ProvableNP}$ is closed only under provably polynomial-time reductions, not necessarily all polynomial-time reductions. However, this does seem to show that if $\mathsf{ProvableP} = \mathsf{ProvableNP}$, then since SAT is in $\mathsf{ProvableNP}$, $\mathsf{P} = \mathsf{NP}$.

So what is remaining is the converse: if $\mathsf{P} = \mathsf{NP}$, does $\mathsf{ProvableP} = \mathsf{ProvableNP}$?

I picked the P vs. NP question because it's the "canonical" unsolved problem in complexity. But, a similar question could be asked about any two complexity classes.

You need to define $L$ carefully. Currently, you seem to require only these properties:

1. "$L$ proves $[A \in \mathsf{P}]$" implies $A \in \mathsf{P}$
2. "$L$ proves $[A \in \mathsf{NP}]$" implies $A \in \mathsf{NP}$
3. "$L$ proves $[\mathrm{SAT} \in \mathsf{NP}]$"

Let $L$ be such that it ever proves only these two statements:

1. $[\mathrm{ONE} \in \mathsf{P}]$, where $\mathrm{ONE}$ is a dummy problem like "always accept", which is clearly in $\mathsf{P}$.
2. $[\mathrm{SAT} \in \mathsf{NP}]$

Then $\mathsf{ProvableP} = \{\mathrm{ONE}\}$ and $\mathsf{ProvableNP} = \{\mathrm{SAT}\}$, which are different even if $\mathsf{P}=\mathsf{NP}$. Note also that $\mathsf{ProvableP} \nsubseteq \mathsf{ProvableNP}$.

• I thought that "strong enough to encode statements about Turing machines" has a fairly standard meaning. I mean the same requirements for Godel's 2nd incompleteness theorem. I'm not sure if it has to be as strong as PA, I seem to remember that slightly weaker is enough. – 6005 Jul 6 '18 at 17:34
• Thanks for the answer and I'm sorry I didn't make that sentence more clear, is it clear now? – 6005 Jul 6 '18 at 17:36

One issue that was overlooked in the question is how to encode languages $A$ (of which there are uncountably many) as finite objects in order for the logic $\mathcal{L}$ to have something to say about them (in particular, how to encode formulas for $[A \in \mathsf{P}]$ and $[A \in \mathsf{NP}]$. Let us assume that languages are subsets of the natural numbers $\mathbb{N}$, and that any $A$ in $\mathsf{ProvableP}$ or $\mathsf{ProvableNP}$ must be given by an arbitrary formula of the symbols of $\mathcal{L}$, i.e. it is any definable subset of $\mathbb{N}$. We are also assuming that:

• $\mathcal{L}$ is consistent;

• $\mathcal{L}$ implies the Peano Arithmetic axioms of $\mathbb{N}$ (PA).

With these assumptions, we now argue that $$\boxed{\mathsf{ProvableP} = \mathsf{ProvableNP} \;\;\text{ if and only if }\;\;\mathsf{P} = \mathsf{NP}.}$$

For the forward direction, assume $\mathsf{ProvableP} = \mathsf{ProvableNP}$, and now consider any language $A$ in $\mathsf{NP}$. Note that $A$ is accepted by a nondeterministic Turing machine $N$, such that there exists a polynomial $p(n)$ which bounds the longest execution branch of $N$ on input a string of length $n$. Then let $N'$ be a nondeterministic Turing machine with the following description: first, count the input length $n$; second, calculate $p(n)$; and finally, run $N$ for at most $p(n)$ steps nondeterministically. If $N$ doesn't halt (this never actually occurs, but $N'$ doesn't know that for sure), $N'$ rejects.

Now observe that $\mathcal{L}$ (more specifically, PA) proves that $N'$ runs in time $p(n)$. Moreover, $\mathcal{L}$ can describe "the language of strings accepted by $N'$" by a formula (roughly, "there exists an sequence of configurations such that the sequence is a run of $N'$ and ends in an accept state"). Then we have that $\mathcal{L}$ proves $[L(N') \in \mathsf{NP}]$. Therefore, $L(N') \in \mathsf{ProvableNP}$. But we know (even if $\mathcal{L}$ doesn't) that $L(N') = L(N) = A$ by construction. So $A \in \mathsf{ProvableNP}$. But $\mathsf{ProvableNP} = \mathsf{ProvableP} \subseteq \mathsf{P}$, so $A \in \mathsf{P}$.

The backward direction is a similar trick. Assume $\mathsf{P} = \mathsf{NP}$ and that $A \in \mathsf{ProvableNP}$. Then $\mathsf{ProvableNP} \subseteq \mathsf{NP} = \mathsf{P}$, so $A \in \mathsf{P}$. From here, we know there is some Turing machine $M$ and polynomial $p(n)$ such that $M$ runs in time $p(n)$ and $L(M) = A$. Let $M'$ be a deterministic Turing machine which, on input of length $n$, first calculates $p(n)$, and then runs $M$ for at most $p(n)$ steps. If $M$ doesn't halt, $M'$ returns a default value, say it rejects.

Then similarly to before, $\mathcal{L}$ proves that $M'$ halts in time $p(n)$ and therefore that $[L(M') \in \mathsf{P}].$ It follows that $L(M') \in \mathsf{ProvableP}$, but we know (even if $\mathcal{L}$ doesn't) that $L(M') = L(M) = A$, thus $A \in \mathsf{ProvableP}$. Thus, $\mathsf{ProvableNP} = \mathsf{ProvableP}$. $\quad \square$