4 ms·

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

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

ProfHewitt 6y ago
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 https://papers.ssrn.com/abstract=3603021

ProfHewitt 6y ago

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 https://papers.ssrn.com/abstract=3603021