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.