Does Tarski Undefinability apply to HOL ? The video about the liar paradox and incompleteness is atrocious, ignorant, lying disinformation.
(1) The video, in its juvenile way, dishonestly mocks people who have studied the subject. It says about the incompleteness theorem, "What exactly does [incompleteness] mean is often something ["incompleteness experts"] have difficulty expressing" while showing a picture of a man in front of a blackboard thinking, "Um..."
First, what exactly is "exactly" supposed to mean there? What form of exactitude is being asked for? Incompleteness is a mathematical theorem that is provable in finitistic arithmetic. It is utterly exact in that way. And the theorem itself is exact, even put in English mathematical terminology: There is no consistent, formal system that proves all the true statements about arithmetic. If one knows what 'consistent', 'formal', 'prove', 'true statement' and 'arithmetic' mean, then the meaning of the theorem is easily understood.
The main question that incompleteness answers is natural and not at all nebulous or "esoteric": If the logic we use obeys the principal of non-contradiction, then are there formal, consistent mathematical axioms that prove all the true statements of arithmetic? The incompleteness theorem tells us that the answer is "no". And that implies there is no algorithm to decide of statements of arithmetic whether they are true. Again, that answers a natural question that may occur to anyone who has a modicum of intellectual curiosity, even to a high school student who might wonder whether there is an algorithm that would answer all of his or her math homework questions.
Moreover there are numerous books and articles that present the proof and discuss the mathematical import of incompleteness.
And the use of scare quotes with "expert" is sophomoric. There are people who are experts on the subject.
Then he says, "And usually you'll get a regurgitation of the aforementioned statement, that is that there are additional statements in the system that are not provable".
First, there is the gratuitously pejorative "regurgitation". Second, it is utterly reasonable to say again exactly what the theorem states, which is straightforward: There is no consistent, formal system that proves all the true statements of arithmetic. To ask that that itself be explained, is to ask the meanings of 'consistent', 'formal system', 'true statement' and 'arithmetic. And anyone familiar with the subject can supply those definitions too. Rather than mathematicians being stuck to explain the subject, mathematicians are prepared to define and explain the terminology used to explicate the the theorem and its proof; there is nothing the least bit esoteric or ineffable about it, notwithstanding that the author of the video (in his egregious ignorance and will to mock what he hasn't bothered to study) postures that there is.
(2) Then the video mentions that Godel mentions that the theorem has a close relation to the liar paradox. It needs to be stressed that the liar paradox is not actually part of the theorem or its proof, but rather that the idea for the theorem and proof are suggested, by analogy only, by the liar paradox. It does not discredit the theorem or its proof one iota that an idea outside of the theorem and proof provided an insight on how to use that idea in its main outline but in a variation that, unlike the paradox, is utterly formally correct and not mathematically nor philosophically problematic. Or one can just as easily mock the invention of the airplane on the basis that it was inspired by observing the flight of birds while everyone knows that humans can't fly in the way of birds; just as anyone who has studied the subject knows that in the relevant languages, the liar sentence is not formalizable but the unprovability sentence is.
* Then, "So when Godel says that his theorem and the liar paradox are closely related, he's indicating that they are literally the same thing but with the word 'untrue' swapped for the word 'unprovable".
This sentence is false.
This sentence is unprovable.
Different by one word. The first is not formalizable in the interpreted language in question and the second is.
The fact that they are different in only one word doesn't diminish that they are vastly different in meaning. Godel never said that they are the same thing except using a different word.
This sentence has only six words.
This sentence has only six syllables.
Different by only one word. The first is true and the second is false.
The author of the video is a liar.
The author of the video is a truth-teller.
Different by only one word. The first is true and the second is false.
(3) Then this brazen flat out lie: "[...] as Godel writes in the closing lines of his introduction, it's the liar statement itself and the contradiction that it furnishes that allows him to reach his famous conclusion regarding the existence of undecidable statements in mathematics."
Godel wrote no such thing.
And while the video says that he did, it shows a supposed translation on screen of those supposed remarks; but the translation shown on screen says no such thing.
The intent must be that people not informed about the subject and not thinking critically about the video and not looking carefully at the quick jump cut text snippets on screen will nod along thinking that Godel must have wrote it because the video says he did and shows it on screen too.
It's a lie that Godel wrote it. And it's a lie that Godel's proof relies on any contradiction derived from the liar sentence, and it's additionally dishonest to purport to support that he did say it by flashing snippets that do not at all support that he said it.
For the benefit of the truth:
* The idea of the proof is heuristically suggested by the liar paradox. A heuristic notion is very different from an actual mathematical argument. And Godel' proof itself invokes only mathematical argument and stands mathematically, independent of the heuristic notions.
* The liar sentence does not appear in any step of the proof.
* The proof shows that the system can formalize "this sentence is not provable". That is very different from "This sentence is not true", and we prove that the the predicate 'is true' (not formalizable in the system itself) and the predicate 'is provable' (formalizable in the system itself) are not coextensive since there are true sentences that are not provable.
(4) Then, "If common sense tells us that the liar paradox isn't anything significant in everyday language, why the heck does it suddenly become so significant when it's translated into a mathematical, computable, or logical language?"
The answer is simple: As mentioned above, the incompleteness proof does not translate the liar paradox. The incompleteness proof adduces a mathematical formula that happens to be true if and only if it is not provable in the system. As mentioned above, that "I am not provable" is similar with "I am not true" doesn't entail that they are the same nor that the implications of formalizing them are the same. The formalization of "I am not provable" is significant even at the most basic level that it leads to answering the question even a middle school student could ask, "Isn't there surefire, step by step method I could follow that would answer every math homework question I have to answer?"
But the author says that one approach is to "assert a significant distinction between the everyday notion of truth versus the mathematical notion of provability."
* We provide a mathematical definition of truth and a mathematical definition of provability. We don't merely assert that they are not coextensive, but rather we prove that they are not.
* The mathematical definition of truth is not claimed to adhere to all the everyday senses of truth, but it does capture the important aspects in context of mathematics.
Then, "To us, such a distinction is superficial and doesn't hold up to deeper analysis."
* Who, pray tell, is "us"?
* What, pray tell, "deeper analysis" is claimed to have been performed?
* The ignoramus author of this video should get a book on symbolic logic then one on mathematical logic to learn how the definitions are formulated and the ensuing theorems.
Then, "One can easily recast the liar paradox in terms that don't invoke the concept of true and false. [...] Indicating that we can't attribute the significance of incompleteness solely to the distinction between true and provable."
* That's a strawman, red herring and non sequitur all in one:
Strawman: No one said that the significance of incompleteness is solely in the distinction between true and provable. Indeed, incompleteness can be stated and proved even without mentioning truth; we can prove the purely syntactical version of the theorem that involves only provability, without having to add the result that the Godel sentence is true.
Red herring: Yes, there are paradoxes similar to the liar paradox but not involving the notion of truth, but in the video that fact is mentioned only as a distraction from the fact that the incompleteness theorem is rigorously proven and that it is significant even at a glance.
Non sequitur: That there are paradoxes similar to the liar paradox but not involving the notion of truth doesn't entail that the incompleteness theorem lacks significance.
Then, "we recognize that Godel's incompleteness theorem was a reaction to the Hilbert program of the early 20th century. A program that basically treated math like a religion and assumed that all mathematical truths could be constructed out of a few simple ones".
* Hilbert's program was the opposite of religion. The program was to regard finitistic calculation as safe and then to prove the consistency of infinitistic mathematics by use of only finitistic calculation. Also, unless someone can adduce otherwise, Hilbert did not regard the axioms as given by a kind of divine revelation. And he did not assume that all the mathematical truths could be derived from a few simple axioms, but rather he proposed seeking a way to do it.
* Moreover, formal axiomatics is the complete opposite of subjective belief. Nothing could be more public and objective than the machine-checkability of formal proofs.
* Godel did not first set out to take down Hilbert's program. The opposite. Godel started by trying to prove the consistency of analysis by finitistic means, but his efforts gave clues that it could not be done, so he switched to proving that it could not be done, which led to the incompleteness work.
Then, "By showing that an absurd self-referential statement could be constructed in wholly mathematical terms, one could argue that Godel was cleverly demonstrating that mathematics was merely a language like any other and therefore subject to all its usual foibles."
* The Godel sentence is not absurd. It's a true arithmetical sentence. A true arithmetical statement cannot be an absurdity. But it also happens that the sentence is true if and only if it is not provable in the system. That still does not make it absurd.
* Mathematics is not merely a language. Various mathematical systems are put in various mathematical languages, but they also have formation rules, inference rules, axioms, proofs and theorems.
* Mathematical languages are not just like other languages. Mathematical languages are formalized while ordinary languages are not.
* Mathematical languages are not subject to all the foibles of ordinary languages. Most saliently, for example, the language of first order arithmetic doesn't have the ambiguities of a natural language such as English.
* Incompleteness is not about languages but rather about systems.
Then, "in order to conclude that mathematics is incomplete [...]"
* The incompleteness theorem doesn't say "mathematics is incomplete". Rather, it says that certain kinds of systems are incomplete. For that matter, for any interpreted language, there is the complete and consistent theory of all the true sentences per that interpreted language. It's complete and consistent. It's just that its not axiomatizable in a way that we can mechanically decide of a given sentence whether it is an axiom.
Continuing, "we have to first believe that the sentence 'this statement is unprovable' is truly paradoxical and not simply a gibberish nonsensical statement disguised as a well formed one".
Wow, that guy is such a self-confused ignoramus.
* He has it exactly backwards. We definitely do not believe that the sentence is paradoxical. Again, back to the earlier central point: The liar sentence is paradoxical, but the Godel sentence is not paradoxical.
* That the Godel sentence is well formed is proven by Godel in the proof itself. And we can mechanically confirm that it is well formed.
* And the sentence is not gibberish as it is well formed in the language of arithmetic.
Then, "Tarski [concluded that] the liar's paradox was something extremely significant".
* It is significant in Tarski's work as it leads to showing the need for our mathematical contexts to not allow such paradoxes. That led to Tarski proving a truth predicate is not formalizable in certain kinds of interpreted languages since such a predicate would yield a liar sentence and its contradiction.
And, "[Tarski's] undefinability theorem hinges on the liar paradox"
* Again, Internet ignoramuses have it backwards. Tarski does not claim that the liar sentence is formalized in the languages, but rather Tarski shows that if a truth predicate is formalizable then the liar sentence would be formalizable, which would yield a contradiction, thus a truth predicate is not formalizable.
Then, the video author shows a picture of Tarski with a text bubble, "I AM the logic". The video author is juvenile as well as a liar and an ignoramus.
At the end of the day, the best we can do is paraphrase the sad resignation in the movie, "Forget it, Jake. It's the Internet."