"This sentence is not true" is not a truth bearer thus not a proposition thus cannot be included in any Boolean logic system. — PL Olcott

A physical analog would be a digital logic inverter (NOT gate) with its output connected back to its input. Such a circuit forms an oscillator, with the output continually swinging back and forth between 0 and 1.

This seems your source of misunderstanding. In propositional logic, you would day "This sentence is not true." But in predicate logic, it can be translated into "Some sentence is not true."
In FOL it can be translated into "X is not true." which are all perfectly true or false depending on the truth criteria of the quantifiers and variables. — Corvus

The Variables of propositional logic and every other order of bivalent logic must have a Boolean value. Any variables that cannot possibly be true or false must be excluded from every bivalent logic system. https://en.wikipedia.org/wiki/Three-valued_logic can have the values {True, False, Nonsense}.
"This sentence is not true" has the semantic value of {nonsense}.

The predicate Is_Not_True(X) summarize by the operator "~" is fine unless
X is defined as X := ~True(X). Then it is the oscillator that wonderer1 referred to.

A physical analog would be a digital logic inverter (NOT gate) with its output connected back to its input. Such a circuit forms an oscillator, with the output continually swinging back and forth between 0 and 1. — wonderer1

Good job that is a perfect analogy!

The Variables of propositional logic and every other order of bivalent logic must have a Boolean value. — PL Olcott

Variables in propositional logic is for the whole sentence, not the elements in the sentence, hence its limitation. You are still talking under the propositional logic domain only.

When you widen the scope into predicate logic, FOL and HOL, the concept of truth and falsity has multifaceted nature. FOL enables you employ the variables for the individuals and subjects. HOL can deal with the variables for the relations, operators and properties within the sentence.

When you widen the scope into predicate logic, FOL and HOL, the concept of truth and falsity has multifaceted nature. FOL enables you employ the variables for the individuals and subjects. HOL can deal with the variables for the relations, operators and properties within the sentence. — Corvus

None-the-less in every bivalent system of logic we must be able to reduce every variable to a Boolean value. Your reply did not seem to understand that. Your reply merely stated that variables in higher orders of logic represent more complex things than in Propositional logic.

It seems that you are simply failing to understand this:
In logic, a three-valued logic (also trinary logic, trivalent, ternary, or trilean,[1] sometimes abbreviated 3VL) is any of several many-valued logic systems in which there are three truth values indicating true, false, and some third value. This is contrasted with the more commonly known bivalent logics (such as classical sentential or Boolean logic) which provide only for true and false.
https://en.wikipedia.org/wiki/Three-valued_logic

A three-valued logic system that can easily handle self-contradictory expressions would have the values of: {True, False, Nonsense}.

None-the-less in every bivalent system of logic we must be able to reduce every variable to a Boolean value. Your reply did not seem to understand that. — PL Olcott

Your reply merely stated that variables in higher orders of logic represent more complex things than in Propositional logic. — PL Olcott

You are still under confusion, or don't want to see the real point. We have not been only talking about bivalent system of logic here. If you can recall the OP is about HOL. Not 2000 year old propositional logic. Hence it was necessary and relevant considering and looking into the multifaceted nature of truth, which are in the domains of FOL and HOL.

This is contrasted with the more commonly known bivalent logics (such as classical sentential or Boolean logic) which provide only for true and false.
https://en.wikipedia.org/wiki/Three-valued_logic — PL Olcott

You have been reading too much Wiki pages, and they can lead you to the wrong places unfortunately.

A three-valued logic system that can easily handle self-contradictory expressions would have the values of: {True, False, Nonsense}. — PL Olcott

If some thing is Nonsense, then it is equivalent to False. In FOL HOL, truth values can be far more than just 3 above you listed. : {True, False, Unknown, Neutral, Contradiction}

You have been reading too much Wiki pages, and they can lead you to the wrong places unfortunately. — Corvus

I always verify that the essential reasoning is correct.
The key elements of my system come straight from me figuring them out and
no one ever wrote them down before.

If some thing is Nonsense, then it is equivalent to False. In FOL HOL, truth values can be far more than just 3 above you listed. : {True, False, Unknown, Neutral, Contradiction} — Corvus

A currently unknown Boolean value is still a Boolean value.
No such thing as a neutral Boolean value. "What time is it?" has no Boolean value.
Contradiction proves False.

"This sentence is not true"
(a) If it was false that would make it true and
(b) If it was true that would make it false,
thus it takes on the third value of nonsense.
{Nonsense} is reserved for expressions that cannot be true or false.

A currently unknown Boolean value is still a Boolean value.
No such thing as a neutral Boolean value. — PL Olcott

Boolean values are applicable up to FOL, but FOL cannot express the full complexities in the world. Hence you are going up to HOL, which has the extended truth values, and can describe more complex states of the real world.

"What time is it?" has no Boolean value.
Contradiction proves False. — PL Olcott

In HOL, "What time is it?" would be translated into computable format, and can be processed for the proper truth values.

{Nonsense} is reserved for expressions that cannot be true or false. — PL Olcott

Nonsense is not a logic world. It is an ordinary linguistic expression to mean False with added stupidity and foolishness connotation.

Boolean values are applicable up to FOL, but FOL cannot express the full complexities in the world. Hence you are going up to HOL, which has the extended truth values, and can describe more complex states of the real world. — Corvus

Boolean values are properties of every Proposition
A proposition is a central concept in the philosophy of language, semantics, logic, and related fields, often characterized as the primary bearer of truth or falsity. Propositions are also often characterized as being the kind of thing that declarative sentences denote. https://en.wikipedia.org/wiki/Proposition

In HOL, "What time is it?" would be translated into computable format, and can be processed for the proper truth values. — Corvus

No not at all. When I ask you is this sentence true or false: "What time is it?"
you have no correct answer because the question has a type mismatch error

Nonsense is not a logic world. It is an ordinary linguistic expression to mean False with added stupidity and foolishness connotation. — Corvus

{Nonsense} is a stipulated term of the art of my formal three-valued formal system of logic
having values of {True, False, Nonsense} that only applies to expressions such as this:

...14 Every epistemological antinomy can likewise be used for a similar
undecidability proof...(Gödel 1931:43-44)

epistemological antinomy AKA self-contradictory expression that cannot possibly be true or false.
This guy seems to sum up my exact same position much more clearly.

The Strengthened Liar and Paradoxes of Incompleteness
https://www.youtube.com/watch?v=5LWQPGjAs3M

duplicate

Boolean values are properties of every Proposition
A proposition is a central concept in the philosophy of language, semantics, logic, and related fields, often characterized as the primary bearer of truth or falsity. Propositions are also often characterized as being the kind of thing that declarative sentences denote. — PL Olcott

A truck load of strawmen here. I didn't deny Boolean values, but I was simply saying that in FOL and HOL, you have the extended truth values including Boolean.

{Nonsense} is a stipulated term of the art of my formal three-valued formal system of logic
having values of {True, False, Nonsense} that only applies to expressions such as this: — PL Olcott

Nonsense !! Nonsense is just a colloquial expression saying, no you are bloody wrong mate.

The Strengthened Liar and Paradoxes of Incompleteness
https://www.youtube.com/watch?v=5LWQPGjAs3M — PL Olcott

Many Wiki pages and Youtube videos are rubbish. Don't trust and worship them as if they are the bible. Think with your own mind, and if it doesn't make sense, then you should be able to say "Nonsense mate. This is what I think, because of this and that." As I said before, they may slag you for saying what you think is true, but at least you know you have been thinking with your own mind, rather than parroting what the Wiki pages and Youtubers said, or joined the herd of the inauthentic comedians seeking pleasure out of attacking the authentic self thinking man.

A truck load of strawmen here. I didn't deny Boolean values, but I was simply saying that in FOL and HOL, you have the extended truth values including Boolean. — Corvus

I don't think that you can find any source that ever says anything like that for bivalent systems of logic. I don't think you can find any sources that say anything like that for (a) propositional logic (b) FOL, (c) SOL, (d) HOL.

https://en.wikipedia.org/wiki/Law_of_excluded_middle only works in bivalent logic.

Nonsense !! Nonsense is just a colloquial expression saying, no you are bloody wrong mate. — Corvus

I have found that line of reasoning ineffective so I switched. We have to resolve my prior reply before you can begin to understand my updated reasoning.

I don't think that you can find any source that ever says anything like that for bivalent systems of logic. I don't think you can find any sources that say anything like that for (a) propositional logic (b) FOL, (c) SOL, (d) HOL.

https://en.wikipedia.org/wiki/Law_of_excluded_middle only works in bivalent logic. — PL Olcott

You should read some good Mathematical Logic books, not the Wiki pages.
But think about it even with your common sense. The world contains more problems, structures, events and objects than things that are just True or False.

For simplest example, when you see a formula, X > 3, that is not true or false until you know the value of X. Until that moment, X > 3 remains unknown.

If you say, "It is raining now." then it could be True in your town, but it could be false for someone living in some other part of the world, because it could be sunny. So your statement is contradictory when looking from both areas of the world.

Some statements or formula depicting the real world structure, events or objects can be unknown, neutral or contradictory. You don't simply reject that as nonsense. You accept them as true, false, unknown, neutral or contradictory depending on the given formula, statements, and analysis.

I have found that line of reasoning ineffective so I switched. We have to resolve my prior reply before you can begin to understand my updated reasoning. — PL Olcott

Please reread my post above.

You should read some good Mathematical Logic books, not the Wiki pages.
But think about it even with your common sense. The world contains more problems, structures, events and objects than things that are just True or False. — Corvus

It is a Boolean valued system. When epistemological antinomies are involved they must be rejected
as a type mismatch error because that have no Boolean values.

For simplest example, when you see a formula, X > 3, that is not true or false until you know the value of X. Until that moment, X > 3 remains unknown. — Corvus

It is resolved to true or false on the basis of the value of X.
Epistemological antinomies cannot possibly ever be resolved to a value of true or false.

If you say, "It is raining now." then it could be True in your town, but it could be false for someone living in some other part of the world, because it could be sunny. So your statement is contradictory when looking from both areas of the world. — Corvus

Yet again can possibly be resolved to a value of true or false depending on location.

Some statements or formula depicting the real world structure, events or objects can be unknown, neutral or contradictory. You don't simply reject that as nonsense. You accept them as true, false, unknown, neutral or contradictory depending on the given formula, statements, and analysis. — Corvus

Only well formed declarative sentences of natural language can be true or false. Any expression of language that is not a proposition must be rejected as a type mismatch error for any formal bivalent system of logic.

A proposition is a central concept in the philosophy of language, semantics, logic, and related fields, often characterized as the primary bearer of truth or falsity. Propositions are also often characterized as being the kind of thing that declarative sentences denote. https://en.wikipedia.org/wiki/Proposition

I have found that line of reasoning ineffective so I switched. We have to resolve my prior reply before you can begin to understand my updated reasoning.
— PL Olcott

Please reread my post above. — Corvus

Instead of a three values system with {True, False and Nonsense} I have bivalent systems of logic that derive a type mismatch error for any expression that is not a proposition.

A proposition is a central concept in the philosophy of language, semantics, logic, and related fields, often characterized as the primary bearer of truth or falsity. Propositions are also often characterized as being the kind of thing that declarative sentences denote. https://en.wikipedia.org/wiki/Proposition

Instead of a three values system with {True, False and Nonsense} I have bivalent systems of logic that derive a type mismatch error for any expression that is not a proposition. — PL Olcott

It is a Boolean valued system. When epistemological antinomies are involved they must be rejected
as a type mismatch error because that have no Boolean values. — PL Olcott

You are confusing between HOL and Computer Programming. In HOL, there is no such things as Boolean values. There are {Truth, False, Unknown, Contradiction, Neutral}, and they are the values of logical interpretation.

Boolean is a type of data in programming language. Boolean type value is not True or False, but "1" or "0", and certainly never have anything to do with "Nonsense".

You are confusing between HOL and Computer Programming. In HOL, there is no such things as Boolean values. There are {Truth, False, Unknown, Contradiction, Neutral}, and they are the values of logical interpretation. — Corvus

They call functions of the Boolean type predicates in all orders of predicate logic. Functions of any other type are called functions. Predicate: >(5,2)==TRUE Function: +(5,2)==7

They call functions of the Boolean type predicates in all orders of predicate logic. Functions of any other type are called functions. Predicate: >(5,2)==TRUE Function: +(5,2)==7 — PL Olcott

For some unknown reasons, you changed the subject to Functions. There are differences in functions of math, and functions in computer programming. Can you explain the difference?

Predicate: >(5,2)==TRUE Function: +(5,2)==7 — PL Olcott

Could you please explain that in plain English? And how is it related to our discussion?

Could you please explain that in plain English? And how is it related to our discussion? — Corvus

All bivalent systems of predicate logic only have (by definition of bivalent) two
Boolean values of True or False with nothing in between. What you have been
saying is the same as saying 2 == 5.

All bivalent systems of predicate logic only have (by definition of bivalent) two
Boolean values of True or False with nothing in between. What you have been
saying is the same as saying 2 == 5. — PL Olcott

I never said that. You keep misinterpreting me.

Anyhow it shows you that bivalent logic is not useful and incapable for the real world uses in describing the complexities of the structures, events and objects.

Not sure if your previous post was about the function call in Prolog, but it didn't look like the standard way of using function calls in the other PLs, hence I asked you about the difference between math functions and programming functions.

Anyhow it shows you that bivalent logic is not useful and incapable for the real world uses in describing the complexities of the structures, events and objects. — Corvus

Not at all every declarative sentence is {True, False} or incorrect.

Not sure if your previous post was about the function call in Prolog, but it didn't look like the standard way of using function calls in the other PLs, hence I asked you about the difference between math functions and programming functions. — Corvus

Prolog does not simply assume that every statement is True or False, thus can screen
out epistemological antinomies that are simply incorrect.

(1) The proof on pages 275-276 of the Tarski paper is not a proof of undefinability, but rather it is a proof of undecidability, specifically that there is a true sentence such that neither it nor its negation are provable in the system.

(2) The proof on pages 275-276 of the Tarski paper does not rely on the liar sentence in any step. Rather, the liar sentence is the reductio ad absurdum in different proofs - those of the undefinability - such that the liar sentence is not assumed but rather from the assumption of definability we derive the liar sentence thus refuting definability. So the situation is the exact opposite of what the poster claims. Again, we don't assume that we can formulate the liar paradox, but rather, toward a contradiction, we assume definability from which we derive that we can formulate a liar sentence, from which we would have a contradiction, thus we refute the assumption of definability.

Saying it another way, since this point continues to be misrepresented by the poster: Tarski shows that the existence of a liar sentence in certain interpreted languages would imply a contradiction, thus in those languages, a liar sentence does not exist.

(3) The passage that begins "In accordance" explicitly is not a statement of a liar sentence but rather it explicitly is a statement about provability. Tarski explicitly says that we don't use a truth predicate there but rather a provability predicate. It is the very point that in the languages under consideration, we cannot form an "I am not true in the interpretation" sentence but that we can form an "I am not provable in the system" sentence.

The poster's gravamen is a brazen straw man based on brazenly reversing what Tarski and mathematicians say.

(1) Higher order logics are usually 2-valued, especially the most famous and most studied ones. One may devise other valuations, but ordinary higher order logics are 2-valued. Being 2-valued is not unique to 0-order and first order logics.

(2) The distinction between 'true vs false' and '1 vs 0' is not essential in the context of ordinary mathematical logic. They both can be understood as the two Boolean values and similar in the substantive senses in which they are used that way.

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

The problem with higher than first order logic, is that they don't have a complete proof theory.
https://en.wikipedia.org/wiki/Second-order_logic
(under MetaLogical results).

The problem with higher than first order logic, is that they don't have a complete proof theory.
https://en.wikipedia.org/wiki/Second-order_logic
(under MetaLogical results). — A Realist

Could you demonstrate your point with some example proofs?

Holy necro batman, I'm closing it.