Gödel demonstrated that mathematics is limited in scope, who's to say that physics is in that scope?
He definitely didn't, since we know of systems that are capable of proving any statement. It's sufficient for the system to be internally inconsistent.
Outside of that, we'd need to be a little more clear about what we mean by "there are statements that can't be proven in any system". I would bet that it is not the case that there is a single special statement with a fixed meaning which all consistent systems are incapable of proving. In the general case, I would expect that a statement, taken by itself, would constitute a consistent (if uninteresting) system. That system would be easily able to prove its only axiom.
In my mind, the incompleteness theorem says that a consistent system of "sufficient power" cannot prove its own consistency. We could reify that into a statement that looks like "This system is consistent"; that's what I'm trying to rule out above by referring to "a statement with a fixed meaning". "This system" would refer to different things within different systems.
Wikipedia says this:
> The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers.
> For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.
> The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency.
This allows for a single statement (say, a result about the natural numbers) that no sufficiently powerful consistent system can prove, but it doesn't require it. The sets of true-but-unprovable statements might be disjoint between two particular systems.
A typical example -- now that I think about it, the only example I have seen -- is the statement "this statement cannot be proved".
Technically, it is not a single statement, because for different axiomatic systems A1, A2... you get different statements "this statement cannot be proved in A1", "this statement cannot be proved in A2" etc.
For any given axiomatic system A, if the system can prove "this statement cannot be proved in A", it contains a contradiction: it just proved something that is not true. But if the system cannot prove "this statement cannot be proved in A", we have an example of a statement that is true but unprovable (in A).
Gödel's trick was inventing a way how a statement can talk about itself. Like, if you say "it is forbidden for a statement to talk about itself", Gödel asks "but surely it is okay for a statement to talk about another statement that it can define unambiguously?" and then creates a statement that sounds like "the statement you get by unpacking the binary string 7461287618276312876873 is not provable in A", but when you actually unpack "7461287618276312876873", you get "the statement you get by unpacking the binary string 7461287618276312876873 is not provable in A" again. So it talks about itself without actually using the words "this statement".
What exactly this all means... I wish I would grok, but I don't. But I am pretty sure it means none of the usual "human brain has mystical magical quantum powers beyond mere computation".
axiomatizes its own provability is the following:
Theorems of T can be computationally enumerated.
cannot computationally enumerate its own theorems:
In order to obtain a contradiction, hypothesize theorems
of a foundational theory T are computationally enumerable.
Then procedures that are provably total in T are
computationally by a procedure that is provably total in
T. Consider the Boolean procedure Diagonal defined on
natural number input n to be the result of the complement
of the result of the ith provably total procedure on input
i. The procedure Diagonal differs from every procedure in
the enumeration of provably total procedures in T.
However, by construction, diagonal is a provably total
procedure in T, which is a contradiction.
decidable that formalizes its own provability, the following
proposition is true but unprovable:
Theorems of T are computationally enumerable.
unprovable here:
https://papers.ssrn.com/abstract=3603021
Note that the above result is more powerful than the one
quoted in the post above because theorems of T might not
computationally enumerable, which is the case for the
Dedekind axiomatization of Natural Numbers.
sense that they characterize Natural Numbers up to a unique
isomorphism. However, there is still a proposition about
Natural Numbers that true but unprovable using the
Dedekind/Peano axioms. Further information can be found here:
"Physical Indeterminacy in Digital Computation"
it is not the case that every true proposition is provable in
Dededkind's theory.
no standard models :-)
isomorphism, which is indeed the standard model. However,
Gödel's incompleteness proofs do not work for Dedekind's theory
because there are uncountable axiom instances. (Dedekind's
theory is nevertheless effective because proof checking is
algorithmically decidable.)
Consequently, the first incompleteness result (inferentially
undecidable) has been proved by other means. See the
following for a proof:
https://papers.ssrn.com/abstract=3603021
The above article explains that Gödel's second
incompleteness result is false because the theory can prove
its own consistency.