> I don't think that Godel showed that there were statements that can't be proven in any system.

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.

> 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.

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".

A proposition that cannot be proved in a theory T that

axiomatizes its own provability is the following:

      Theorems of T can be computationally enumerated.

[Church 1934] presented the following simple proof that T

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.

See the following article for additional information:

https://papers.ssrn.com/abstract=3603021

For a theory T in which proof-checking is computationally

decidable that formalizes its own provability, the following

proposition is true but unprovable:

      Theorems of T are computationally enumerable.

There is a proof the above proposition is true but

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.

That's a really good framing. I like it.

Assume consistency. Take the collections of all true statements about the standard model of the natural numbers and make these statements your axioms. Now every true statement about the standard model of the natural numbers is provable. It’s a useless axiomatic system since there is no procedure for knowing if a statement is an axiom of not (that works for every statement). The second order Peano axioms are categorical and assuming consistency every true statement is ‘provable’.

Higher-order Dedekind/Peano axioms are categorical in the

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"

https://papers.ssrn.com/abstract=3459566

So the last sentence I made is false. The rest is correct, right?

Yes, the last statement that you made is indeed false, that is,

it is not the case that every true proposition is provable in

Dededkind's theory.

In math you can prove statements given a set of axioms. But in physics you can just validate things with experiments.

Odd you were downvoted ! I think that this is a good insight because it underlines physics!=math!=physics.