vamvam wrote: ↑Wed Mar 05, 2025 10:08 pm
G <=> not provable(G) is true.
Yes, the expression is true because the diagonal lemma guarantees that it is true for at least one G.
However, we do not need to know for which G exactly this expression is true.
The expression is equivalent to:
(G and not provable(%G)) or (not G and provable(%G))
This means:
G is true and G is not provable, or
G is false and G is provable
This means that there exists:
A sentence that is true but not provable, or
A sentence that is false and provable.
If we assume that first-order arithmetic does not prove false sentences, it means that there exist a sentence that is true but not provable ("incompleteness theorem").
The hard part of the proof is to prove the diagonal lemma. This proof is quite short but generally considered incomprehensible:
https://proofwiki.org/wiki/Diagonal_Lemma
I personally never manage to remember this proof for longer than an hour.
Godel's incompleteness theorem follows trivially from the diagonal lemma (predicate at hand is "provable(n)"). Tarski's undefinability of the truth also follows trivially (predicate at hand is "true(n)").
vamvam wrote: ↑Wed Mar 05, 2025 10:08 pm
G is truth value of the sentence and G is false.
No, G is an unknown sentence of which do not know whether it is true or false. We just know that G exists, and that the following is true about G:
G <=> not provable(%G)
What exactly G says, is unknown. What its truth value is, is unknown. But then again, it is irrelevant what exactly G says or what its truth value is. Godel's incompleteness theorem still necessarily follows from the simple fact that it exists.
The sentence "This is not provable" means "This
unknown sentence is not provable".
Note that this is the classical version of the proof for Godel's incompleteness theorem. It is considered objectionable in terms of constructivism:
(1) It shamelessly makes use of the law of the excluded middle (LEM).
(2) It does not properly construct a witness, i.e. example, for its claim, because witness G is essentially unknown.
Note that G is obtained by diagonalization, which can somehow be considered to be constructive. However, there is no mention of any algorithm to actually locate such G. Therefore, it is not "properly" constructive.
ChatGPT: Is diagonalization a constructive algorithm?
Diagonalization, as a mathematical technique, is generally not considered a constructive algorithm in the sense of constructive mathematics or computability theory.
In the meanwhile, there are alternative versions available of the proof that are constructivistically acceptable, but they are also harder to explain than the proof in plain classical logic.