What independence between ZFC and P vs NP would imply

Your post doesn't seem to have anything to do with P vs NP, it's just a statement of indignation at Gödel's incompleteness theorems :-)

Here's a simplified example. Imagine you have an axiomatic "model of reality" that describes computers. Then I can write a computer program that successively generates all valid proofs in that axiom system. If the program stumbles upon a valid proof that 1=0, it halts, otherwise it goes on searching. It seems to be a "prima facie substantive question" whether the program will halt or not, but our axiom system cannot settle it because it cannot prove its own consistency by Gödel's second incompleteness theorem, unless it is inconsistent.

The root of the problem, IMO, is our inability to describe integers. By the Löwenheim–Skolem theorem, you cannot have an axiomatization of the integers that rules out nonstandard integers. I wrote several posts about this.

Now suppose that R was shown to be formally independent of ZFC in the sense that for some axiom A0, ZFC+A0 implies P=NP and ZFC+~A implies P!=NP. This would resolve the mathematical question of P versus NP

This is only true if A0 is independent of ZFC. This makes things unnecessarily complicated and obscures how one would usually prove that something is independent. There are a variety of methods of showing that something is independent, but the most common method is to construct two models of the theory, one with the statement and the other with the negation. If both models are contained in your original system then you know that as long as your original system is consistent, your desired statement is independent. A more concrete example that avoids a lot of the subtleties and abstractions is what happened with the parallel postulate in the 19th century. By making slightly other geometries (such as geometries on the surface of a sphere), one could do the exact same process as above.

All this adds up to: The P versus NP problem (and questions like it that can be phrased as definitive questions about reality) must have an answer unless our model of reality is incomplete

I think you may be confusing reality with our models here. Consider for example the possibility that our universe is actually discrete and finite. If that's the case, then a decent model won't answer whether P != NP or not in the abstract sense.

In general, when a specific question is being asked it helps to try to put in the less abstract version and see if anything changes. In this context, what do you think happens if we replace P ! = NP with some more concrete question? Say for example I want to know if 3^^^^^^3 + 1 has an even or odd number of prime factors. This is at least more concrete in that you can specify a specific computation that if you could do it you could then answer this question. I don't know of any easy way to answer this sort of question but it looks really difficult. It may well be that this question is simply unresolvable in our universe because the computational resources to answer it don't exist. But from the perspective of something like ZFC this question is trivial. This suggests to me that there are subtle issues going on here that you aren't quite addressing. P != NP is a particularly tricky question because there are so many options for what could happen that are logically consistent but seem weird (e.g. there's an algorithm that solves 3-SAT in polynomial time but this can't be proven in ZFC. Or the algorithm's correctness can be proven but not a polynomial bound on its run time. Or the run time can be proven but not the correctness of the algorithm. Etc.)

How issues like undecidability and our modeling of reality interact are really tough. It isn't helpful to jump in with them using an example that is itself really abstract.

All of that said, there's an overview by Scott Aaronson on whether P != NP is undecidable that is worth reading(pdf). He does also discuss towards the end some of the issues you are touching on.

The problem (or, according to some posters, one of the problems) with your idea is that the concept of a polynomial-time algorithm is itself a mathematical question and not a question about reality. If I gave you the running times of an algorithm for input sizes from 1 to 3^^^3, this would not tell you whether the algorithm is polynomial. However, it would answer the question as far as reality is concerned, since it's impossible to perform the algorithm on inputs bigger than that (or even remotely close to that size).

For simple algorithms like bubble sort or whatnot, we can look at the algorithm and say, "oh, that's quadratic time" and that lets us make predictions about how long it will take to run (if it takes 10 seconds to sort a 10^9 element array, then it will probably take 1000 seconds to sort a 10^10 element array). But this is not a statement about reality directly -- this is a mathematical statement which describes reality, in this case.

Furthermore, it is impossible to make this sort of statement in general. Just as we can't tell if an arbitrary program halts or not, we cannot in general say if an arbitrary algorithm runs in polynomial time. In fact, I'd bet that one can construct an algorithm such that the question whether the algorithm runs in polynomial time is independent of ZFC. This is not a question of ZFC failing to describe reality, because it's not a question about reality whether the algorithm is polynomial, to begin with.

As for P=NP... there's actually an interesting exercise that I'd expect anyone in a good theoretical CS class to see. Right now, without doing cutting-edge research, I can write down an algorithm for solving 3SAT with the following property: if P=NP, then the algorithm I write down will run in polynomial time (and obviously the converse also holds). Thus, deciding whether P=NP is isomorphic to determining the running time of this algorithm (which has a very simple description!) As I've stated earlier, it would not be too surprising if this question turned out to be independent of ZFC.

Edit: it appears that my last paragraph has been preempted.

Also: upvoted for an interesting question.

Perhaps more controversially, I claim: Under the correct model M' it seems that it's impossible for a substantive question (such as Q) to be unanswerable.

Have you heard of Gödel's incompleteness theorems?

Whether a Turing Machine ever halts is a concrete question with a definite yes or no answer; but, if we could construct an axiomatic system with a recursively enumerable set of theorems such that for each Turing machine a theorem existed stating whether the machine halted or not, then we could build a decider for whether any Turing machine halts.

All this adds up to: The P versus NP problem (and questions like it that can be phrased as definitive questions about reality) must have an answer unless our model of reality is incomplete.

Then all possible models of reality are incomplete.

also see: http://en.wikipedia.org/wiki/David_Hilbert#Formalism

Please don't confuse math with "reality". Math as about axioms and proofs (well-formed finite strings), and is often a useful tool in mapping the territory, but it is just that, one of the tools.

If a question about reality turns out to be logically independent of a model M, then M is not a complete model of reality.

Quantum Mechanics is a classic counterexample, as far as we know, in a sense that there is no deeper underlying theory that would predict an outcome of a measurement when QM says it cannot be determined.

Suppose we had a model M that we thought described cannons and cannon balls. M consists of a set of mathematical assertions about cannons

In logic, the technical terms 'theory' and 'model' have rather precise meanings. If M is a collection of mathematical assertions then it's a theory rather than a model.

formally independent of the mathematical system A in the sense that the addition of some axiom A0 implies Q, while the addition of its negation, ~A0, implies ~Q.

Here you need to specify that adding A0 or ~A0 doesn't make the theory inconsistent, which is equivalent to just saying: "Neither Q nor ~Q can be deduced from A."

Note: if by M you had actually meant a model, in the sense of model theory, then for every well-formed sentence s, either M satisfies s or M satisfies ~s. But then models are abstract mathematical objects (like 'the integers'), and there's usually no way to know which sentences a model satisfies.

Scott Aaronson (a well-known complexity theorist) has written a survey article about exactly this question.

Is there anything that suggests that this is the case for P vs. NP?

If ZFC and P vs NP are independent, this means that it's impossible to give a proof that P=NP with ZFC. Since an example of a polynomial-time algorithm that can solve an NP problem would be such a proof, any such algorithm must be impossible to state in ZFC. Any algorithm we can actually run can be stated in ZFC. As such, this would mean that P!=NP. You'd just have to prove it in ZFC+1, which is ZFC with the additional axiom that ZFC (the original, not ZFC+1) is consistent.

It is not clear that our universe has infinite computing power. If it is finite, then there is a finite complete description of it. Maybe that finite description even fits in the universe. But we can't, in the universe, compute all the consequences of the description. If the universe is infinite and able to simulate infinite Turing machines, such as Conway's game of Life, then Gödel's theorem applies, as others explain. There are also intermediate possibilities, such as the universe is infinite, but we are not able to exploit it for computation, but a positivist might classify that as finite. I think that the state of the art is that this is the case, due to the cosmological constant.