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:

• "$L$ proves $[A \in \mathsf{P}]$" implies $A \in \mathsf{P}$

• "$L$ proves $[A \in \mathsf{NP}]$" implies $A \in \mathsf{NP}$

• "$L$ proves $[\mathrm{SAT} \in \mathsf{NP}]$"

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

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

• $[\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}$.

StackExchange Computer Science Q#93885, answer score: 3