Re:Hawking Hawking
by ProfHewitt on Saturday April 10, 2021 @02:49PM
(#26763947)
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.
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.
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".