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.
I think you may be confusing reality with our models here.
Yeah my claim was a little ambiguous. I meant to claim that either (1) our current model of reality fails to describe some truths about the universe or (2) P=NP is decidable in our model. [I'm only clarifying the claim, I'm now dubious about whether this it is true.] You're right- I should add (3) P=NP cannot be cast as a question about reality.
Suppose we had a model M that we thought described cannons and cannon balls. M consists of a set of mathematical assertions about cannons, and the hypothesis is that these fully describe cannons in the sense that any question about cannons ("what trajectory do cannon balls follow for certain firing angles?", "Which angle should we pick to hit a certain target?") can be answered by deriving statements from M. Suppose further that M is specified in a certain mathematical system called A, consisting of axioms A1...An.
Now there is much to be said about good ways to find out whether M is true of cannons or not, but consider just this particular (strange) outcome: Suppose we discover that a crucial question about cannons - e.g. Q="Do cannon balls always land on the ground, for all firing angles?" - turned out to be not just un-answerable by our model M but 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.
What would this say about our model for cannons? Let's suppose that we can take Q as a prima facie substantive question with a definitive yes or no answer regardless of any model or axiomatization. At the very least it seems that M must be an incomplete model of cannons if the system in which it is specified is insufficient to answer the various questions of interest. It seems to me that
If a question about reality turns out to be logically independent of a model M, then M is not a complete model of reality.
Now we have an axiomatization of mathematics -- let's say it's ZFC for now -- and we have a model of computation in reality, which is M="The unvierse can contain machines that (efficiently) compute F iff there exists a Turing machine that (efficiently) computes F" with appropriate definitions of what exactly a Turing machine is in terms of ZFC. Suppose we want to answer a question like Q="Can the universe contain machines that efficiently solve SAT?"
Under the premise that M is true, the question Q becomes the pure logical question R="Are there Turing machines that efficiently solve SAT?", i.e. the P versus NP problem.
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 but the question Q seems like a prima facie concrete question with a definitive yes or no answer that does not rely for its substance on M or ZFC or any other epistemic construct. It would seem that we must have missed something in our description of reality, M.
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.
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.