5 added 61 characters in body

I think the source of the confusion here is the idea that all models of ZFC have the same notion of what a "natural number" (and hence, by an appropriate encoding, an "algorithm") is. Unfortunately, Godel's incompleteness theorem tells us that no recursively enumerable axiom system (of which ZFC is an example) can precisely pin down the theory of the true natural numbers (i.e. true arithmetic), which can thus only be fully described in the metatheory rather than in any formal system. As such, there exist statements G about natural numbers which are true in some models of ZFC and false in others, because these two models have genuinely different interpretations of the natural number system.

It is a proiri conceivable (though, in my opinion, unlikely), that P=NP is one of these statements. Specifically, it is conceivable that SAT is not solvable in polynomial time in the standard model of the natural numbers, but is solvable in polynomial time in an exotic model of the natural numbers, even if both models of the natural numbers are part of respective models of set theory obeying ZFC. The point here is that the exotic algorithm could have a length which is an exotic natural number, which could be larger than every standard natural number; similarly, the constants in the polynomial run time for this exotic algorithm could also be larger than every standard number. So there is no obvious way to convert the exotic polynomial time SAT solver into a standardly polynomial time SAT solver; it may even be that the exotic algorithm cannot be described at all in the standard model, let alone have a polynomial run time.

[Edit: actually, with Levin's trick, if SAT is solvable, it is always solvable with a bounded-length algorithm (namely, "run all possible algorithms in parallel in a carefully chosen manner"), so exotic length is not a genuine issue. However, this still does not exclude the possibility of exotic run time constants.]

It is even conceivable (though, again, I believe it to be unlikely) that the reverse is true: SAT is solvable in polynomial time in the standard model, but not in a exotic model. Here, the standard algorithm has a length which is a standard natural number, so the algorithm can at least be described in the exotic world. But just because it has a polynomial run time in the standard model, this does not necessarily imply a polynomial run time in the exotic model (unless one has a transfer principle, as is the case in the models coming from nonstandard analysis, but not all exotic models are of this type); the algorithm may solve all standard SAT problems in a polynomial amount of time, but require super-polynomial time to solve an exotic SAT problem. [In this scenario, ZFC + P!=NP would be $\omega$-inconsistent, but could still be consistent.]

4 added 29 characters in body

I think the source of the confusion here is the idea that all models of ZFC have the same notion of what a "natural number" (and hence, by an appropriate encoding, an "algorithm") is. Unfortunately, Godel's incompleteness theorem tells us that no recursively enumerable axiom system (of which ZFC is an example) can precisely pin down the theory of the true natural numbers (i.e. true arithmetic), which can thus only be fully described in the metatheory rather than in any formal system. As such, there exist statements G about natural numbers which are true in some models of ZFC and false in others, because these two models have genuinely different interpretations of the natural number system.

It is a proiri conceivable (though, in my opinion, unlikely), that P=NP is one of these statements. Specifically, it is conceivable that SAT is not solvable in polynomial time in the standard model of the natural numbers, but is solvable in polynomial time in an exotic model of the natural numbers, even if both models of the natural numbers are part of respective models of set theory obeying ZFC. The point here is that the exotic algorithm could have a length which is an exotic natural number, which could be larger than every standard natural number; similarly, the constants in the polynomial run time for this exotic algorithm could also be larger than every standard number. So there is no obvious way to convert the exotic polynomial time SAT solver into a standardly polynomial time SAT solver; it may even be that the exotic algorithm cannot be described at all in the standard model, let alone have a polynomial run time.

[Edit: actually, with Levin's trick, if SAT is solvable, it is always solvable with a bounded-length algorithm (namely, "run all possible algorithms in parallel")parallel in a carefully chosen manner"), so exotic length is not a genuine issue. However, this still does not exclude the possibility of exotic run time constants.]

It is even conceivable (though, again, I believe it to be unlikely) that the reverse is true: SAT is solvable in polynomial time in the standard model, but not in a exotic model. Here, the standard algorithm has a length which is a standard natural number, so the algorithm can at least be described in the exotic world. But just because it has a polynomial run time in the standard model, this does not necessarily imply a polynomial run time in the exotic model (unless one has a transfer principle, as is the case in the models coming from nonstandard analysis, but not all exotic models are of this type); the algorithm may solve all standard SAT problems in a polynomial amount of time, but require super-polynomial time to solve an exotic SAT problem. [In this scenario, ZFC + P!=NP would be $\omega$-inconsistent, but could still be consistent.]

It is even conceivable (though, again, I believe it to be unlikely) that the reverse is true: SAT is solvable in polynomial time in the standard model, but not in a exotic model. Here, the standard algorithm has a length which is a standard natural number, so the algorithm can at least be described in the exotic world. But just because it has a polynomial run time in the standard model, this does not necessarily imply a polynomial run time in the exotic model (unless one has a transfer principle, as is the case in the models coming from nonstandard analysis, but not all exotic models are of this type); the algorithm may solve all standard SAT problems in a polynomial amount of time, but require super-polynomial time to solve an exotic SAT problem. [In this scenario, ZFC + P!=NP would be $\omega$-inconsistent, but could still be consistent.]