I need some help from people with logic superpowers
In the Wikipedia page for Turing's Halting problem, they mention that you can prove Gödel's First Incompleteness theorem from it.
That is superb because the proof for Turing's Halting problem is really easy to understand. So, it is a great starting point for any downstream proof. This is the relevant quote:
[i]Assume that we have a sound (and hence consistent) and complete
axiomatization of all true first-order logic statements about natural
numbers. Then we can build an algorithm that enumerates all these
statements. This means that there is an algorithm N(n) that, given a
natural number n, computes a true first-order logic statement about
natural numbers, and that for all true statements, there is at least
one n such that N(n) yields that statement. Now suppose we want to
decide if the algorithm with representation a halts on input i. We
know that this statement can be expressed with a first-order logic
statement, say H(a, i). Since the axiomatization is complete it
follows that either there is an n such that N(n) = H(a, i) or there is
an n' such that N(n') = ¬ H(a, i). So if we iterate over all n until
we either find H(a, i) or its negation, we will always halt, and
furthermore, the answer it gives us will be true (by soundness). This
means that this gives us an algorithm to decide the halting problem.
Since we know that there cannot be such an algorithm, it follows that
the assumption that there is a consistent and complete axiomatization
of all true first-order logic statements about natural numbers must be
false.[/i]
After reading this proof, I wondered if a very similar proof by contradiction could also prove Tarski's Undefinability theorem? I was thinking of something along the following lines:
Imagine that a truth predicate isTrue([math]\ulcorner s \urcorner[/math]) for any arbitrary logic sentence s were computable. In that case, this predicate would also be able to compute the truth status for any arbitrary H(a,i). Therefore, we would be able to compute isTrue([math]\ulcorner H(a,i) \urcorner[/math]) for any possible H(a,i). Consequently, such isTrue([math]\ulcorner s \urcorner[/math]) predicate would solve Turing's Halting problem, while we already know that it is fundamentally unsolvable. Therefore, such truth predicate is not computable.
Is there a flaw or a problem with this proof strategy?
The fact that the Wikipedia page mentions this proof strategy for Gödel's First Incompleteness but not for Tarski's Undefinability got me wondering. Maybe it does not work for Tarski after all? What's the catch?
That is superb because the proof for Turing's Halting problem is really easy to understand. So, it is a great starting point for any downstream proof. This is the relevant quote:
[i]Assume that we have a sound (and hence consistent) and complete
axiomatization of all true first-order logic statements about natural
numbers. Then we can build an algorithm that enumerates all these
statements. This means that there is an algorithm N(n) that, given a
natural number n, computes a true first-order logic statement about
natural numbers, and that for all true statements, there is at least
one n such that N(n) yields that statement. Now suppose we want to
decide if the algorithm with representation a halts on input i. We
know that this statement can be expressed with a first-order logic
statement, say H(a, i). Since the axiomatization is complete it
follows that either there is an n such that N(n) = H(a, i) or there is
an n' such that N(n') = ¬ H(a, i). So if we iterate over all n until
we either find H(a, i) or its negation, we will always halt, and
furthermore, the answer it gives us will be true (by soundness). This
means that this gives us an algorithm to decide the halting problem.
Since we know that there cannot be such an algorithm, it follows that
the assumption that there is a consistent and complete axiomatization
of all true first-order logic statements about natural numbers must be
false.[/i]
After reading this proof, I wondered if a very similar proof by contradiction could also prove Tarski's Undefinability theorem? I was thinking of something along the following lines:
Imagine that a truth predicate isTrue([math]\ulcorner s \urcorner[/math]) for any arbitrary logic sentence s were computable. In that case, this predicate would also be able to compute the truth status for any arbitrary H(a,i). Therefore, we would be able to compute isTrue([math]\ulcorner H(a,i) \urcorner[/math]) for any possible H(a,i). Consequently, such isTrue([math]\ulcorner s \urcorner[/math]) predicate would solve Turing's Halting problem, while we already know that it is fundamentally unsolvable. Therefore, such truth predicate is not computable.
Is there a flaw or a problem with this proof strategy?
The fact that the Wikipedia page mentions this proof strategy for Gödel's First Incompleteness but not for Tarski's Undefinability got me wondering. Maybe it does not work for Tarski after all? What's the catch?
Comments (5)
Yes, there is. I don't understand a word of it. That's a HUGE problem. (The strategy may be solid, though. I am no judge of that.)
Concerning the proof strategy for Gödel's incompleteness theory, the Wikipedia page makes the following remark:
At the same time, I have found the following academic publication by Jeremy Avigad, "Incompleteness via the halting problem". Apparently, the Wikipedia page editors do not allow to list this particular publication as a source for the section.
The page history does not clarify why this decision was made.
In the following math stackexchange discussion I have found the following damning criticism:
The page itself says:
I suppose that the weaker system is not pressured to disprove false statements (only to prove true ones).
Hence, this proof strategy is deemed a bit controversial for Gödel's incompleteness theorem, let alone, for Tarski's undefinability. I personally like it, however, because it is much easier to understand than the alternatives.
What is the undecidability of the halting problem? What is the halting problem? This is factual knowledge to gain before anyone can contribute to your thread in any meaningful way.
If it has to do something with the fact that the axioms of math are dependent in some way on the workings of math, yet they are the basic underlying principles of math, then I say that's true, but can't be proven without introducing some OTHER logical systems (such as what language is and how it works) that also suffer, so to speak, of the woes of the first, second, third, ... and nth incompleteness theorem.
In fact, the whole universe, if it indeed exists, can't be proven to exist, because the proof would need to pull in some systems that are built on axioms that are pulled from the physical universe, and used in the proof of the universe's existence.
In fact, this applies to any physical or other empirically observed phenomenon.