[Maxatar]

Assume that P = NP is undecidable, then it would not be possible to present an algorithm that is NP-complete and in P, since such an algorithm would imply that P = NP is decidable which contradicts the assumption that P = NP is undecidable.

A simpler way to think about this concept in general would be, assume that it's undecidable in ZFC whether every even natural number greater than 2 is the sum of two primes.

Well if it's undecidable in ZFC then it must be true. If it weren't true then it would be possible to present an even number that isn't the sum of two primes, but presenting such a number would be a proof and hence contradict the assumption that it's undecidable. Hence the only way for it to be undecidable in ZFC is if there isn't any such even number, but ZFC is not powerful enough to prove that no such number exists.

This is the subtle difference between decidability and truth. For certain classes of statements (not all), especially ones involving existence, if they are undecidable within ZFC then they must be true.

Another subtlety is that one can never state categorically that a statement is undecidable, a statement can only be undecidable with respect to a formal system, and being undecidable with respect to a formal system does not mean that we can't ever know if that statement is actually true or false, it just means that said formal system is not powerful enough of proving from within that system whether it's true or false.

[drdeca]

What if you had an algorithm which could e.g. solve 3SAT in polynomial time, but couldn’t be proven (in ZFC) to always produce the correct answer?

[Maxatar]

If you can prove in ZFC that the algorithm always halts for every input but it's undecidable in ZFC whether the algorithm is correct for every input, then it follows that the algorithm is correct for every input and hence P = NP. If you can't prove in ZFC that the algorithm halts for every input then you can't deduce anything further. Let's break it down and get an understanding of why this is.

Assume an algorithm X halts for every input and it's undecidable in ZFC whether X is correct for all inputs. Well if X were incorrect for some input Q, then since X halts for every input, Q could be used to prove in ZFC that X is incorrect. Since we assumed that X's correctness is undecidable in ZFC, it follows that no such X exists.

To better understand the nature of this issue, it boils down to the fact that ZFC can not unambiguously define the natural numbers. For every definition of the natural numbers in ZFC, there are at least two possible interpretations, one interpretation is the actual natural numbers 0, 1, 2, ... where every single natural number consists of a finite sequence of digits. But ZFC will also have another interpretation of the natural numbers which are not the ACTUAL natural numbers but a kind of mutation of the natural numbers, these natural numbers can have an infinite sequence of digits.

In situations where the correctness of an algorithm is undecidable in ZFC, it means that there is some interpretation of the natural numbers, some mutated system of numbers where the algorithm would give the wrong answer. The algorithm gives the correct answer for all ACTUAL natural numbers, but will give an incorrect answer for some mutated "natural number" consisting of an infinite sequence of digits. Because ZFC is not powerful enough to distinguish between the actual natural numbers and the mutated natural numbers, ZFC is not powerful enough to prove that the algorithm is correct for the actual natural numbers.

You can read more about these mutations here:

https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...

Now you might think that 3SAT isn't about natural numbers, the input for 3SAT is a boolean formula, not a number. Well that's a minor detail since for every single boolean formula, there is a 1-to-1 correspondence to a natural number. So this hypothetical algorithm would be correct for every formula that has a correspondence to an actual natural number, and each of these formulas would consist of a finite sequence of symbols, ∨, ∧, ¬. However, there would also be mutated versions of these formulas that don't correspond to a natural number but do correspond to a mutated natural number. These formulas would consist of an infinite sequence of symbols, ∨, ∧, ¬. Since the algorithm is undecidable in ZFC, then there is some mutated formula for which the algorithm gives an incorrect answer and since ZFC can not distinguish between mutated formulas and actual real formulas, that's where the undecidability lies.

And finally, you may be tempted to think that you can just define the natural numbers in such a way that they must consist of a finite sequence of digits and this whole issue will go away, surely there must be some way we can define the natural numbers so that they consist only of a finite sequence of digits and rid ourselves of these infinite sequence mutations. And well what we know from Godel's incompleteness theorem is that there is a way to do that, but it involves making your system inconsistent.

[drdeca]

If X runs in polynomial time, then there is of course some X' which produces the same outputs on the same inputs, and provably (in PA, I'm pretty sure, certainly in ZFC) runs in polynomial time. So, if there exists an algorithm X which solves 3SAT in polynomial time, then there is an algorithm X' that provably runs in polynomial time, and solves 3SAT. If ZFC cannot prove that X' always produces the right answer, then, I suppose that implies (By Godel's completeness theorem) that there is a model of ZFC in which it doesn't...

uhh... huh.

Does the standard construction of the natural numbers in ZFC, if considered in a non-standard model of ZFC, produce a nonstandard model of PA? That's not what I had expected.

err... I guess there isn't necessarily a thing which is considered "the standard model of ZFC", so I guess I mean, "is there a model of ZFC in which the usual construction of the natural numbers, isn't the standard model of the natural numbers?" (where the model of ZFC is I guess a model within another ZFC or some other set theory, and asking whether the set of natural numbers in that model, is the standard one, is asking about how it compares to the model of the natural numbers in the outer set theory)