Does Tarski Undefinability apply to HOL ?
Higher-order logic is the union of first-, second-, third-, ..., nth-order logic; i.e., higher-order logic admits quantification over sets that are nested arbitrarily deeply.
https://en.wikipedia.org/wiki/Higher-order_logic
All orders of logic in one formal system.
There are many ways to further extend second-order logic. The most obvious is third, fourth, and so on order logic. The general principle, already recognized by Tarski (1933 [1956]), is that in higher order logic one can formalize the semanticsdefine truthof lower order logic.
https://plato.stanford.edu/entries/logic-higher-order/
"Simple type theory, also known as higher-order logic"
The seven virtues of simple type theory
https://www.sciencedirect.com/science/article/pii/S157086830700081X
All orders of logic in one formal system.
Thus a single formal system have every order of logic giving every expression of language in this formal system its own Truth() predicate at the next higher order of logic.
https://en.wikipedia.org/wiki/Higher-order_logic
All orders of logic in one formal system.
There are many ways to further extend second-order logic. The most obvious is third, fourth, and so on order logic. The general principle, already recognized by Tarski (1933 [1956]), is that in higher order logic one can formalize the semanticsdefine truthof lower order logic.
https://plato.stanford.edu/entries/logic-higher-order/
"Simple type theory, also known as higher-order logic"
The seven virtues of simple type theory
https://www.sciencedirect.com/science/article/pii/S157086830700081X
All orders of logic in one formal system.
Thus a single formal system have every order of logic giving every expression of language in this formal system its own Truth() predicate at the next higher order of logic.
Comments (240)
I don't understand this.
It has always seemed to me that Tarski's Undefinability theorem fails when applied to a knowledge ontology inheritance hierarchy (KOIH). It has only occurred to me recently that KOIH is essentially type theory which is essentially HOL. https://en.wikipedia.org/wiki/Ontology_(information_science)
It seems that all of the formal systems that these two apply to only have a single order of logic. When we define a formal system that simultaneously has an unlimited number of orders of logic then there is always one more order of logic as needed.
That a formal system can be defined with a single order of logic seems isomorphic to an encyclopedia defined with only the "C" volume. Of course such a system would be incomplete, yet it is a little silly to define systems or encyclopedias this way.
I cannot give a rigorous answer, but I agree with this. If Tarski's undefinability theorem is basically that "arithmetical truth cannot be defined in arithmetic", or that true Gödel numbers are not definable arithmetically, meaning theres no first-order formula for this, I think it does go for higher order logics. For those higher order logics there is their own true but unprovable Gödel number.
But I'm the amateur here, so don't quote me.
(PS, why two threads?)
There is always an unprovable expression in one order of logic that is provable in the next order. When all orders of logic are included in the same formal system then such a system cannot be incomplete. I posted this in two forums because the more appropriate forum has hardly any views.
Anything that can't be proved in one order of logical can be proved or refuted in the next. A formal system having every order of logic cannot be incomplete. A formal system having only one order of logic is like the "C" volume of an encyclopedia only having articles that begin with the letter "C".
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44) Epistemological antinomies (AKA self-contradictory expressions) must be excluded from every formal system of logic because they are not truth bearers. I can't follow your other proof, yet it seems to follow the principle that every simple idea can be made convoluted enough that it can no longer be understood.
I don't think this is true.
Every theorem of 0th order logic has a corresponding theorem in 1st order logic. Like P=>Q goes to For all X P ( X ) implies Q ( X )
Every theorem of 1st order logic has a corresponding theorem in 2nd order logic.
I'm fairly certain that generalises, but haven't come up with a proof sketch. i.e. nth order logic lets you express and prove all the things that are in (n-1)th order logic and more.
Now consider that you're taking the set of all provable statements of all logics up to the nth order. That will then be the set of provable statements of the nth order logic, due to the hierarchy.
You've stipulated that n>2, so your logic is strictly more expressive than 2nd order logic.
Incompleteness results apply to 2nd order logic, since you can axiomatise the natural numbers with + and * in it. That's more than enough arithmetic for Tarski and Godel.
So your big union of logics is one logic - of the highest order you designate. And so long as it contains 2nd order logic, you can derive incompleteness results for it.
Moreover, I think you're claiming that you end up axiomatising the (n-1)th's logic's metalanguage in the nth logic's syntax? But when you end up having such a tower of logics and take their the union, it isn't quite that you'd be taking the union of their metalanguages as well, there'd need to be a single unifying metalanguage in which the formulae of all the levels could be expressed. The truth and provability symbols in the metalanguage would thus apply for theorems applying to the big union logic, rather than having a plethora of distinct symbols in different metalanguages - though concepts like 1st order derivable could maybe be phrased in that expansive metalanguage for the union of the logics.
Similarly, there would need to be one type of object which would model all the formulas. I'd conjecture set theory would work for all of them. Reason being you can think of quantification of order n as ranging over a set which allows quantification over collections of sets (n-1) recursions deep. Like 0th order logic allows no quantification. 1st allows quantification within a set, 2nd allows.... quantification over sets. 3rd allows... quantification over sets of sets, which is kinda just quantification over sets.
So it would surprise me if this giant logic wasn't a version of "set theory in disguise" (like second order logic was called by Quine), to which incompleteness results already apply.
When we envision the inherent structure of the set of all knowledge that can be expressed using language then we can see that "incompleteness" and "undecidability" are mere errors in disguise.
For every nth order logic that can be shown to be incomplete there is an n+1 order logic that completes it.
Yes, definitely.
Quoting fdrake
One metalanguage that can refer to one of more elements at any level within the type hierarchy.
It would seem that for every n order or logic there would necessarily be an n+1 order of logic provability predicate for this N order of logic.
Do we need more than first and second order logic in practical uses?
A knowledge ontology inheritance hierarchy capable of formalizing the entire body of human knowledge that can be expressed using language need not be incomplete in the Gödel sense. Such a system would essentially be a type hierarchy from type theory thus isomorphic to HOL.
https://en.wikipedia.org/wiki/Ontology_(information_science)
For formalizing the entire body of human knowledge that can be expressed using language we need this:
There seems to be a finite limit to the number of orders of logic needed.
There is a great debate about whether an expression of language
can be true without a truth maker.
Truthmaker Maximalism defended GONZALO RODRIGUEZ-PEREYRA
https://philarchive.org/archive/RODTMD
A truth without a truthmaker is like a cake without a baker,
non-existent.
True and unprovable is self-contradictory once one understands
how true really works the way that I and Wittgenstein do.
https://www.liarparadox.org/Wittgenstein.pdf
Analytic TRUE is a constant property of some expressions of language defined in terms of its relation to other expressions of language. An expression of language is TRUE if and only if it is (a) stipulated to be true, or (b) semantically derived from expressions of language that are stipulated to be true.
High-Order Logic seems to be more flexible and powerful for the real world cases due to its expanded variables availability for the properties and relations.
I was under impression that higher than 3rd-order logic would be for the multiple set theories and advanced calculus applications, therefore they wouldn't be used for describing the empirical world cases.
A knowledge ontology https://en.wikipedia.org/wiki/Ontology_(information_science) is essentially an inheritance hierarchy of types from type theory which is apparently the same thing as HOL.
Great link with much useful info to learn. Thank you PL.
I am trying to see whether or not HOL actually defeats Tarski Undefinability.
One can formalize the semanticsdefine truthof lower order logic in high-order logic. Under that fact, isn't it the case HOL defeats Tarsky Undefinability in the formalization, because TU only applies to the domain of Algebraic statements?
The Liar Paradox basis of the proof: https://liarparadox.org/Tarski_247_248.pdf
The full actual proof: https://liarparadox.org/Tarski_275_276.pdf
It seems that the Tarski proof concludes this:
This sentence is not true: "This sentence is not true" is true.
It is true that it is provable in meta-F that G is unprovable in F. "G is unprovable in F" has its truth-maker in Meta-F.
"Tarski's indefinability theorem states that arithmetical truth cannot be defined in arithmetic - that is, there is no predicate definable in arithmetic that holds of exactly the Godel numbers of the truths of arithmetic. The indefinability theorem is closely related to Godel's incompleteness theorems, and is also at the heart of much research on the Liar paradox." -pp. 285-286
It sounds like Tarski's indefinability theorem is only applicable to arithmetical truths according to the dictionary.
What is the meaning of the word arithmetical?
/??r??.m?.t?k/ uk. /?ær.???met.?k/) involving adding, subtracting (= removing a number or amount), multiplying, or dividing numbers: arithmetical problems. Figuring the amount is a simple arithmetical calculation.
Is the Indefinability theorem in the dictionary same as "undefinability" in the OP?
You have to look at his actual proof to see otherwise:
It would
then be possible to reconstruct the antinomy of the liar in the
metalanguage, by forming in the language itself a sentence x
such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
The full actual proof: https://liarparadox.org/Tarski_275_276.pdf
Is the actual Liar Paradox in PA ?
https://andrew-bacon.github.io/papers/Front%20matter.pdf
That's the book.
Quoting tim wood
Downloaded and saved into my iPad, thanks. Great reading material. :up: :pray:
What is PA?
Quoting PL Olcott
Strange, the book doesn't say anything about Godel, Tarski, undefinability, or Paradox in the whole content. It talks a lot about Labmda Calculus, Frege, Hilbert and High-Order Model Theory.
https://en.wikipedia.org/wiki/Peano_axioms PA = (Peano Arithmetic)
Ok, Peano. :up:
The HOL book by Bacon must be an introduction to the subject, and doesn't seem to discuss anything about Liars paradox or Tarski's truth. I will try to finish it first, and then look at the Tarski's truth and Godel numbers.
I have been working on self-referential paradox for two decades. I have understood that a
https://en.wikipedia.org/wiki/Ontology_(information_science) knowledge ontology would correct these issues for about five years. No one else that understands the math of the things has the slightest clue what a knowledge ontology is. It just occurred to me much more recently that HOL is isomorphic to a knowledge ontology.
That's cool Olcott.
Quoting PL Olcott
This sounds a very interesting topic. I was reading on HOL recently, and it seems to be heavily mathematical arithmetic stuff. My question arose with the Liars paradox. How do you convert the Liars paradox sentence into HOL formula?
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y,
which appears within it. As a result, Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
:up: :pray: I have not used Prolog, but it gives a rough idea to go about and trying it in the other PLs such as C, C++ or Java. Thanks Olcott.
From your coding, it seems no problem for HOL dealing with the Liars paradox and also Tarksi's undefinability.
Tarski only proved that a truth predicate cannot be applied to a non-truth bearer. He got confused when This sentence is not true: "This sentence is not true" is true. The inner sentence is his theory and the outer one is in his metatheory. The smarter thing to do would be to reject the inner sentence as not a truth bearer.
Sounds good idea. Only problem with the PLs handling the paradox cases could be the program crash, when the contradicting variables with TF values were encountered during the execution. But being HOL with the expanded variable availabilities, the inner sentence could be assigned to the next variable for the different boolean values. HOL being arithmetic oriented structure, not sure how they would be in handling the text or sentence based data handling. It would be great help in understanding the operational side of it if the real program testing sessions would be available to see with the paradox cases.
HOL is simply a bridge so that people that don't have a clue what knowledge ontologies are can think of them using the simpler isomorphism of what they do know. As I already showed Prolog can detect and reject such expressions. A system based on knowledge ontologies could be equivalent to an actual human mind.
Isn't HOL the expanded logical system from the other simpler ones with the relation and operation variables in the formulas? Most modern programming languages seem to be based on HOL. How about Prolog? My computer logic book has a chapter on Prolog with its syntax. It says it is a declarative language rather than procedural like PASCAL, and it always has to refer to a database for the facts and rules.
HOL applies to set of things at the next lower order of logic. Prolog works the way that analytic truth really works. If an expression can be proven from facts using rules then it is true. If it cannot be proven from facts using rules then it is untrue. An expression is only actually false when its negation can be proven from facts using rules.
This eliminates this terrible mistake by Gödel:
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44)
And eliminates the Liar Paradox basis of the Tarski Undefinability Theorem.
Wittgenstein agreed with the above:
https://www.liarparadox.org/Wittgenstein.pdf
Yes, it would be good if you could present the Tarski's and Godel's theorems in connection with HOL with your own explanations (the proofs and refutations) in clear English with added formulas too (if needed).
An epistemological antinomy is really just a self-contradictory expression that has no truth value. He might as well of have because "What time is it?" cannot be proved true or false mathematics is incomplete.
This sentence is not true: "This sentence is not true" is true. The inner sentence is in Tarski's theory and the outer sentence is in his meta-theory (the next higher order of logic). Tarski never noticed that "This sentence is not true" is not a truth bearer thus the same ask asking is this sentence true or false: "What time is it?"
I am not sure how Prolog works in Boolean value settings and execution operations. I have ordered a couple cheap Prolog books by the way. But in Pascal, C and other HLPLs, they have no problems dealing with the paradox cases in the sentence for the operations due to ability to assign the sentences into either Constants or variables. Then the constants or variables can be initialised with boolean values at the start-up of procedures or functions, which sets the variable or constant values to either True or False.
And then operations for checking the constants or variables with the input data or external condition or states, which generate further TF values, in which case then further process of operations could be written depending on the TF values of the checked out variable or constants.
The paradox problems were only problem or paradox because the TF values were reflected from the semantic values in the word "true" or "false" in the sentence rather than the TF values on the whole sentence.
In PASCAL or C, "What time is it?" can be set as True or False in a variable, and can be used to check the condition of the input data for comparing and generating another TF value from the checking operation. I presumed that was what HOL was all about. Being able to assign any sentence or type of data into the vast different type of variables, and manipulate the TF conditions by controlling them. I am not sure how Prolog would do it, yet.
I am not talking about anything like that. I am referring to the (non-existent truth value of the) actual semantic meaning of the English sentence: What time is it?
It is easer for people to see that sentence has no truth value.
On the other hand it should not have taken humanity 2000 years
to continue to fail to understand that self-contradictory sentences
have no truth value.
The Liar Paradox in C++
int main()
{
bool Liar_Paradox = (Liar_Paradox == true);
}
I see. But my point was, isn't the main point of using HOL (as also mentioned in the OP title) is being able to set TF values to the non-existent truth value sentences or word such as "What time is it?", and make use of them in the real world applications?
For example, in algorithmic language
Set S = "What time is it?"
Read External Data Q
If Q = S then
S = True
If S = True then Read Time from the System Clock
Write{"Time is 09:00.")
If Q <> S then
S = False
If S = False then
Write("Please type your question again."
End. => Can be translated into any other PL such as C, C++, java, Python or Pascal ..etc
Saying "What time is it?" has no TF value sounds like ignoring the flexibility and applicability of the program languages and also armchair linguistic philosophy of 1950s. :D
No, not at all. Nothing like that. I am only talking about HOL because everyone seems to be totally clueless about knowledge ontologies so I am using HOL as the closest analogy that people are familiar with. We can stipulate that {dogs are animals} as an axiom of our model of the actual world. We cannot stipulate that {dogs are fifteen story office buildings} as an axiom of the model of the actual world.
To create a formal system that never gets stuck in any paradox we have the Prolog/Wittgenstein notion of truth. Provable from Facts makes true. The opposite is provable from Facts makes false. Everything else is not a truth bearer.
I am waiting for a couple of cheap old Prolog books which are on my way. Prolog seems to be the system for Logic programming. It seems to be a PL which has a long history, but seems to be still very much popular even now especially for AI applications.
I have the classic Clocksin and Mellish. https://www.amazon.com/Programming-Prolog-Using-ISO-Standard/dp/3540006788
The ones I ordered are,
PROLOG ++: The Power of Object-oriented and Logic Programming" by C. Moss.
Prolog Programming for Artificial Intelligence by Bratko.
All my Computer Programming Logic books have a chapter or two on ProLog.
Untrue unless provable from Facts does seem to be the correct model for the entire body of analytic truth. Analytic truth seems to be essentially nothing more than relations between finite strings.
Analytic truth can be true, but wrong. Can "wrong" be "true", and "right" be "false"?
Saying that analytic truth can be wrong it like saying that kittens can be 15 story office buildings it cannot possibly ever happen. The closest thing to analytic truth being wrong is when we changed our mind on calling Pluto a Planet. Pluto was a planet until we changed the definition of the term: "Planet".
Analytic truth can be wrong, when it contradicts the reality. The reality has potential possibility to be otherwise from status quo at any moment of time. Therefore AT has potential possibility of being wrong.
I am stipulating that analytic truth are only those expressions of language that are a correct model of the actual world. It seems a little nutty to define it any other way.
SUBTOPIC: Undefinability and Truth
??.et al,
All "Orders of" logic have a necessity in the concepts and characteristics being defined. That applies to the elemental "quantifiers" in the Tarski Theorem.
As our Friend PL Olcott points out: "mathematics is incomplete." And that presumption profoundly affects the symbolic language (syntax) of logic in the First and Second Orders. Higher-order logic (HOL) is another animal altogether.
Remember, once you begin to apply the various forms of syntax and semantics (algorithms, guidelines, notation rules, or heuristics) to any attempt to solve a question or inquiry, there is no room for a eureka moment that is dependent on the human intellect. A eureka moment is undefined by any equation and in many cases is incomprehensible.
Most Respectfully,
R
I hypothesize that mathematics is only construed as "incomplete" based on a nonsense meaning of complete. When provable from axioms means true and the opposite is provable from axioms means false then everything else is simply untrue without any {incomplete} in-between.
Analytic truth can be wrong, if it is wrongly defined, expressed or applied to an incorrect model of the actual world, which is always possible from the human error. Claiming it is absolutely right in all circumstance sounds nutty.
That is like saying the integer five may not be any kind of number at all. Everything that is {incorrect} is excluded from the body of {truth}. That people make mistakes has no actual effect what-so-ever on truth itself. If everyone in the universe is certain that X is true and X is not true their incorrect belief does not change this.
You are not reading what comes after, Quoting Corvus :)
Analytic truth is a definition fallacy. It is defined as,
1. It is true, even if it is false.
2. Therefore to say it is false, is false even if it is true.
There is always potential possibility of human error in application side of the business due to unknown or changing states of the models in the world, which can make analytic truth wrong.
{correct} is an aspect of the meaning of the term {truth} so analytic truth cannot possibly be wrong in any way what-so-ever. If it cannot possibly be wrong in any way what-so-ever then it cannot possibly be wrong in any specific way.
If it is "if it is wrongly defined" then it never was any sort of truth at all. If it was "applied to an incorrect model of the actual world", then again it never was any sort of truth at all. {Analytic truth} are only the subset of expressions of language that are actually true even if everyone in the universe disagrees about the truth of these expressions.
The terrible mistake is that no self-contradictory expression is any kind of propositional at all. Not only is it a mistake it is a ridiculously stupid mistake as if we spent 2000 years years trying to figure out whether this sentence is true or false: "What time is it".
Self-contradictory expressions are not truth bearers in the same way that questions are not truth bearers. Most of the best experts in the world are still trying to "resolve" the truth value of the liar paradox: "This sentence is not true".
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. https://en.wikipedia.org/wiki/Proposition
In other words you too simply don't understand that epistemological antinomies (AKA self-contradictory expressions) are simply not truth bearers thus have no idea why this statement is pure nonsense:
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44)
Your points seem to be confined in the domain of analytic truth only. In a domain where all in the domain is defined as truth regardless of the real world cases, it doesn't seem to be meaningful or productive keep insisting analytic truth is true in all cases. Jump out from the cave of the analytic truth, you can see that there are the real world and possible world with chaotic situations and events, where truth can be wrong, falsity can be right, and lots of possible unknown events, objects and situations. Analytic truths becomes useless in the all possible world.
Another point is that, you have been talking about the Paradox cases in the old propositional logic only. It looks the paradox is problem, and cannot be handled logically, and devoid of truth value from the old restricted logic. But if you look at the paradox from even PL or FOL, it can be handled no problem.
"This sentence is false" can be generalised into "Some sentence is false" which is not a contradiction. Suddenly it is not explicitly self referencing for the truth value. It generalise the sentence into some sentence which is false out there. HOL generalisation and abstraction would be able to handle far more complex cases with its expanded variables for relations, operations and predicates.
That is not true at all. If someone says that a {dog}
The way that all self-contradictory sentences are ruled out is simple. Self-contradictory sentences cannot be proven or refuted from axioms thus are tossed out as non-truth bearers.
¬TruthBearer(L, x) ? ?x ? Language(L) ((L ? x) ? (L ? ¬x))
¬TruthBearer(L,x) ? ?x ? Language(L) ((L ? x) ? (L ? ¬x))
It does seem ridiculously stupid that a formal system could be construed as incomplete on the basis that it cannot prove self-contradictory expressions. We could analogously say that a baker that cannot bake a perfect angel food cakes using only house bricks for ingredients lacks baking skill.
Likewise we can generalize cows eat house bricks into cows eat something.
Any nonsense sentence can be changed into a different sentence that is not nonsense.
We can determine that the Liar Paradox applied to itself is true:
This sentence is not true: "This sentence is not true" is true.
yet we can only do this on the basis that the Liar Paradox is not a truth bearer, thus would have rejected it before it gets to the meta-level of analysis.
To be proven requires a sequence of inference steps that prove that they themselves do not exist.
This is just like this adapted form of René Descartes: "I think therefore I am"
becomes: "I think therefore thoughts do not exist". (AKA nonsense).
Quoting tim wood
That he is simply too stupid to reject self-contradictory expressions makes him enormously foolish. On a related note he starved himself to death because he only trusted his wife's cooking. That he did not even trust his own cooking was quite psychotic.
When reviewing the actual publications in the field it seems that the greatest experts in the field are incapable of understanding that self-contradictory expressions are not true. This forum right here has proven to be the best forum for these things. People here (on this site) are generally very intelligent and thoughtful.
The world's leading experts all seem to be uniformly indoctrinated into believing that Gödel's words are utterly infallible. No one even bothered to notice that any expression asserting its own unprovability requires a sequence of inference steps that prove that they themselves do not exist.
It sounds a weak argument for your point. Some surly confused guy calling an honest man dishonest doesn't make the honest man dishonest. Likewise some obtuse man making totally irrelevant claims wouldn't have anything to do with the fact that analytic truth is true or false.
You expect your interlocutor try to make the most reasonable inferences for the arguments. If they come with totally irrelevant barmy claims, then you know he is not worth for any discussions on truth or logic.
You know the cows eat house bricks is false from common sense.
https://en.wikipedia.org/wiki/Common_sense
You don't need to generalise it to find out it is false. But generalisation and abstraction is what FOL and HOL are for the computability of ordinary language.
I got this book as well. It just arrived. It seems Prolog is a great logic program language which is built on FOL and HOL. An ideal PL for AI applications.
The actual model of the world is the basis. Facts not opinions.
That set of facts that comprise the actual model of the real world is the basis.
This includes common sense and also details that almost everyone does not know.
The key most important thing about Prolog is that Gödel's incompleteness can not be implemented in Prolog. Unprovable simply means untrue. Since this
[b]...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44)[/b]
In Prolog epistemological antinomies are simply rejected as malformed:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y,
which appears within it. As a result, Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)
This is ALL there is to expressions of language that are true on the basis of their meaning
(1) Some expressions of language are stipulated to be true thus providing semantic meaning to otherwise totally meaningless finite strings. These expressions are the set of facts.
(2) Some expressions of language are derived by applying truth preserving operations to (1).
Epistemological antinomies belong to neither (1) nor (2) thus are merely untrue.
Copyright 2023 and earlier PL Olcott
The ONLY way that we know that {cats are animals} is that it is stipulated to be true on the basis of the assigned meaning of the words.
2+2=4 is derived from Peano Arithmetic axioms, thus (2) derived from (1).
Actual facts are expressions of language that correctly model the actual world even if everyone in the universe disagrees or no one in the universe knows them.
I am making zero assumptions what-so-ever. Facts are expressions of language that are true
EVEN IF NO ONE KNOWS THIS OR EVERYONE IN THE WHOLE UNIVERSE DISAGREES.
Here you seem to be saying that we can determine the set of facts from a well constructed dictionary.
Quoting PL Olcott
And here you seem to be re-stating the Correspondence Theory of Truth.
We can combine (1) and (2) and say that every expression of language that is true on the basis of its meaning is either a fact or derived from a fact. Facts are true even if everyone disagrees or no one knows.
Writing down every single detail of all of the general knowledge of the actual world would probably need a book at least a million miles tall. Since this is only 59 petabytes this is probably not nearly enough.
The reason for my persistence with correcting the notion of truth is that incorrect notions are resulting in the extinction of humanity through climate change and the end of Democracy through Nazi propaganda.
If we had a properly formalized notion of truth then it would be possible for a computer program to argue against the hired liar climate change deniers and Nazi propagandists so effectively that this people would look like complete fools even to themselves.
It will not focus its attention on every lie, only the ones that can have near term catastrophic consequences. I can't understand how 45% of the electorate can believe that election fraud changed the outcome of the 2020 presidential election when there has been literally no evidence of this.
The system that I propose would know 10,000-fold more about counter-propaganda than any human mind can possibly hold. The bad people that are pushing Nazi propaganda have had many decades perfecting their craft. The good people telling the truth don't have the slightest clue of how to effectively deal with this.
The Germans currently know how to counter-propaganda?
One of the things that they did that has worked is limiting free speech.
It does seem to me that counter-factual lies should come with civil liability.
To keep free-speech open you are allowed to assert any opinion as long
as you qualify it as only an opinion.
When you assert a counter-factual lie as a verified fact you can lose up to
all of your assets no matter how much you have. This would be especially
helpful for the fossil fuel industry's hiring of liars.
No one was talking about opinions here apart from yourself. Isn't it a typical case of the strawman?
But your example "cows don't eat house bricks" is neither a fact nor common sense. It is just an irrelevant daft statement, which is based on senseless reasoning. :)
It can be implemented in C or Java in modified form with abstraction and generalisation. It cannot be implemented because you are seeing it in the propositional logic rather than predicate or first-order logic.
It is a concrete example of an expression of language that is true on the basis of it meaning. Quine objected to true on the basis of meaning trying to get away with saying there is no such thing as meaning. The stupid nitwit could not even begin to understand that bachelors are not married.
Gödel Incompleteness can only be implemented in systems that implement Boolean True(L, x) incorrectly. It cannot exist in systems where True(L, x) means that x is provable from L and False(L, x) means ~x is provable from L and for everything else x is simply untrue in L.
This same reasoning also conquers Tarski Undefinability.
When Tarski anchors his undefinability in the Liar Paradox:
x = "This sentence is not true" we get
Truth-Bearer(L, x) ? ?x ? L ((L ? x) ? (L ? ¬x)) // x is not a Truth-Bearer
Quine was not a stupid. He was very academic and famous. He wrote many Logic and Philosophy books. I have some Quine books.
Bachelors can mean different things. Bachelor is also "a person who holds a first degree from a university or other academic institution" - Oxford Dictionary
Hence a woman can be a bachelor, so could a man married many times. I am sure there are surnames called "Bachelor", hence some married old folk could be a Bachelor, Mr Bachelor, or if for a woman, Ms Bachelor. They are all B(b)achelors.
A person with a 50 million IQ that cannot understand that (one the the sense meanings of) the term {bachelor} is assigned the semantic meaning of {unmarried + male + adult} is ridiculously stupid about this one point.
I think Quine did understand what bachelor meant. But his point was that a word can mean different things, the meanings of words can change through time and culture, and for a word to convey clear meanings, it needs the context in the expressions in grammatically correct sentence reflecting the reality situations.
It sounds naive to say that a word means just the simple definitions in a bracket in tautological form, and that is the only truth in all cases under the sun.
No that it not it. He used the term {synonymous} 98 times. He did not understand that the term {bachelor} is simply assigned the semantic meaning of {unmarried + male + adult}.
Are there expressions of language that are true but are NOT true on the basis of their meaning AND also are not derived from other facts? Put slightly differently - is there another mechanism/method to determine the truth value of expressions of language?
Yes there is a TV in my living room right now is true on the basis of eyesight.
Really? In which book or article did he do that? I have his Mathematical Logic, Method of Logic, Elementary Logic and The Significance of New Logic, total 4 books. But cannot recall seeing it.
Quoting PL Olcott
Bachelor is a rather simple term. There are many other words in English which are more abstract to define. Try to define "Self", "Soul" and "Existence". Let's see if analytic truths can define them without contradiction or obscurity.
As I said before, will say again. The whole confusion with the paradox and undefinability have been originated from the single narrow perspective seeing the problems in propositional logic, which only allows a proposition must be either True or False.
If you think about the real world situations and objects, there are cases where things are neutral i.e. neither true nor false such as Number 0. And there are the real world cases where things are both True and False, read on QM or some Metaphysical topics.
If you open up the perspective wide and accept all these possibilities in the real world, it is quite normal for some cases to be either True or False, neither True nor False, or both True and False. If you apply FOL and HOL into your program languages bearing that point in your mind, and design the programs to deal with the particular cases in the real world examples, they deal all the case quite fine (Quine).
Two Dogmas of Empiricism Willard Van Orman Quine
https://www.theologie.uzh.ch/dam/jcr:ffffffff-fbd6-1538-0000-000070cf64bc/Quine51.pdf
Quoting Corvus
Yet he wrote a whole paper on his failure to understand that the term {bachelor} is simply assigned the semantic meaning of {unmarried + male + adult}.
The term {true bearer} is very widely know throughout philosophy. That declarative sentences can be {truth bearers} and questions cannot be {truth bearers} is known by everyone that knows what {truth bearers} are. It takes very little additional understanding to know that {self-contradictory expressions} are not {truth bearers}.
That Tarski and Gödel did not understand something as simple as this makes them totally incompetent.
A {truth-maker} is a more difficult subject than a {truth-bearer} It took me 20 years of primary and secondary research to fully understand exactly what a {truth-maker} is for expressions of language that are true on the basis of their semantic meaning. It turns out that the final analysis of this is very simple.
On the other hand a {truth-bearer} is much simpler than this:
A truth-bearer is an entity that is said to be either true or false and nothing else.
https://en.wikipedia.org/wiki/Truth-bearer
In other words a {truth-bearer} is any expression of language that can possibly have a semantic value of true or false. This generally includes declarative sentences and generally excludes questions.
I have focused 20 years of primary and secondary research on the relationship between epistemological antinomies and expressions of language that are true on the basis of their semantic meaning.
At this point it does seem very very stupid that people cannot understand that self-contradictory expressions are not {truth-bearers}.
Quoting PL Olcott
So there are two distinct mechanisms to determine the truth value of a language expressions, yes?
That almost everyone including the greatest experts in the field do not fully understand that self-contradictory expressions are not {truth-bearers} does seem ridiculously stupid to me. To me it seems like the same thing as a PhD mathematics professor that disagrees with first grade arithmetic because they simply "do not believe in" numbers.
Yes. There is expressions of language that are true on the basis of their semantic meaning and there are expressions of language that are true on the basis of direct observation by the sense organs. The first kind boils down to relations between expressions of language.
Very close. A proposition / logic sentence is defined to always be a {truth-bearer}. This means that it is either true or its negation is true.
A truth-bearer is any expression of language that can have the semantic value of true or false. That after 2000 years people do not understand that the Liar Paradox (and other self-contradictory expressions) are not {truth-bearers} seems as ridiculous as a PhD math professor that simply "does not believe in" numbers.
Tarski's Undefinability theorem still stands even though its basis is that a Truth predicate cannot correctly determine that the actual Liar Paradox is true or false. To me this is like all of the bakers in the world trying again and again to bake an angel food cake using only house bricks for ingredients and never having any idea that this can't possibly work.
That is the same as saying there are a whole lot of integers that are greater than five and less than three, utterly ridiculous nonsense. That logicians make sure to never pay any attention at all to philosophy of logic makes them complete ignoramuses. There there are no mistakes within their false assumptions DOES NOT MEAN THERE ARE NO MISTAKES.
That actual self-contradictory sentences (not the deliberate double-talk of so-called) cannot possibly be true or false should have been universally accepted thousands of years ago shortly after the Liar Paradox was created.
Please provide one example. Contradiction is a very well-known and certain measure of falsity in classical logic, symbolic logic, predicate logic.
Gödel's Incompleteness use diagonalization that show G is not provable in F yet totally hides why it is unprovable. When reasoning is entirely hidden behind mathematical operations there is no basis for rebuttal.
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
...We are therefore confronted with a proposition which asserts its own unprovability. 15 ...
(Gödel 1931:43-44)
Exposes the actual reasoning that is hidden behind the mathematical operations.
I just recently figured out that the proof of any "proposition which asserts its own unprovability"
requires a sequence of inference steps that prove that they themselves do not exist.
That would be the same as converting René Descartes famous: "I think therefore I am"
into "I think therefore thoughts do not exist", ridiculous nonsense.
Russell's Paradox was solved by simply correcting the incoherent definition of a set.
We can solve Tarski Undefinability this same way: Truth_Bearer(F, x) ? ((F ? x) ? (F ? ¬x))
Your statement here sounds nonsense. Some questions can be for true or false. For example, "You lied, didn't you?" This means you lied, and it is true. It is also to mean you should be aware of the fact that you lied.
That is a great counter-example. It seems to me that is actually a declarative sentence that is phrased as a rhetorical question. It is comprised of two distinctive parts: The statement: (a) "You lied." and the question: (b) Did you lie? When we break it down to its constituent parts (b) is still not a truth bearer.
I am not sure if you are allowed to modify the given example sentence under the process of breakdown.
If it is allowed, then virtually all questions can be truth bearers.
For instance, "What time is it now?"
One could modify it into "It is true that she asked what time it is now.", hence one can say it is true.
"How are you doing?" - one can modify it again - "It is true that she asked him how he was doing." Therefore "How are you dong?" is a truth bearer.
Are modifications, inferences and breakdowns on the original sentence allowed for TF values?
Sentences with ambiguity must be disambiguated before that can be properly analyzed.
For example asking a man that has never been married: Have you stopped beating you wife?
Would be rejected as semantically incorrect on the basis of the false presupposition.
An expression of language that is both a question and a statement would also have
to be rejected until it is translated into one or the other. The sentence: "Did you lie?"
is not a truth bearer thus would be rejected by a correct Truth Predicate.
More generally, Godel's and Tarski's proofs do not have the defects claimed in this thread (and claimed by the same poster several other times in this forum). That can be verified by reading an introductory textbook on mathematical logic in which the groundwork and proofs of Godel-Rosser incompleteness and Tarski undefinability are provided.
...We are therefore confronted with a proposition which asserts its own unprovability. 15 ...
(Gödel 1931:43-44)
The above is a direct quote from the proof and the system referred to by the above quote certainly does require a sequence of inference steps that prove that they themselves do not exist. The actual proof itself hides all of its underlying semantics behind the purely symbolic manipulation of mathematical operations. Diagonalization shows THAT G is unprovable in F and hides WHY G is unprovable in F.
Tarski's proof is directly anchored in the actual Liar Paradox itself.
Liar Paradox basis of proof: https://liarparadox.org/Tarski_247_248.pdf
The actual proof itself: https://liarparadox.org/Tarski_247_248.pdf
Most people can understand that: "This sentence is not true" cannot possibly
be true or false thus is not a truth bearer. Tarski did not seem to understand that
or he would not have used it as the basis of his proof.
Rather, using the above style of notation, we have:
True(M x) where M is a model and x is a sentence. Read as "x is true in M".
and
Theorem(L x) where L is a set of axioms and x is a sentence. Read as "x is a theorem from L".
And we prove about certain systems:
Theorem(L x) implies that for every model M, if True(M y) for every y in L, then True(M x). (This is the soundness theorem).
And we prove about certain axiom sets:
If True(M x) in every model M, then Theorem(L x).
And incompleteness proves that there are M and L such that:
(1) For every y such that Theorem(M y), we have True(M y); and (2) True(M x); but (3) it is not the case that Theorem(L x).
Quoting Corvus
Corvus was testing the boundaries of what is included and what is not included by using a rhetorical question as a pseudo statement.
G asserts that G is not provable in system P.
But P does not prove G, and P does not prove that it does not prove G.
/
Proofs don't "hide" things. From fully declared axioms and rules of inference, we may prove Godel-Rosser. We may prove versions that do not mention semantics. And we may prove versions that mention both syntax and semantics. This is all famous and understood by reading an introductory textbook in mathematical logic.
/
I know the context in which interrogatory sentences were mentioned lately. But the matter of interrogatories has been brought into other posts in this forum as part of incorrect attempts to refute the theorems.
When G asserts its own unprovability in F the proof of G in F does require a sequence of inference steps in F that prove that they themselves do not exist. We at the meta-math level can see that there cannot possibly be such a proof of G in F thus we know that the assertion that G is unprovable in F is true.
That unhides the whole essence of Gödel's proof where we can see WHY G is unprovable in F not merely THAT G is unprovable in F.
When (as in Prolog) True(L, x) means Provable(L, x) and
(as in Prolog) False(L, x) means Provable(L, ~x) then Tarski Undefinability theorem utterly fails.
Self-contradictory expressions are simply rejected as not bearers of truth.
That's the point.
Too miss that point is to utterly not know what the theorem is about.
"Why" is not a technical term, more a heuristic matter, and could mean different things to different people. In the most bare sense, "Why is T a theorem?" is answered by showing the proof of T . But, heuristically, there is a massive amount of discussion in the literature giving insight into the theorem and its proof; and insight is given in Godel's own paper.
But to accommodate someone who insists that 'true' means 'provable', then we could simply say that wherever we have written the word 'true', it is to be replaced by 'gorue'. Then read all the proofs and discussions about them with that change. It matters not toward understanding the substance of them.
That there is no proof of nonsense does not make any formal system incomplete unless
Incomplete(F) is a euphemism for Incorrect(G).
The definition of 'incomplete' is simple:
A theory T is incomplete if and only if there is a sentence S in the language for T such that neither S nor its negation are a theorem of T.
It is trivial to prove that there are incomplete theories, and not trivial, though pretty easy, is proving the soundness theorem that then trivially proves the incompleteness of certain theories. What is interesting about Godel-Rosser is that there are incomplete theories of a particular kind (consistent, recursively axiomatizable and arithmetically sufficient).
The problem with this definition is that it proves that mathematical systems are "incomplete" when they cannot prove or refute nonsense. Self-contradictory expressions are nonsense and cannot be proven or refuted only because they are nonsense.
Gödel specifically states that the inability to prove a self-contradictory expression
DOES MAKE THE FORMAL SYSTEM INCOMPLETE.
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44)
Using stipulative definition Incomplete(F) is simply a euphemism for Incorrect(G).
[b]Incomplete does not retain any of its conventional meaning
incomplete: not having all the necessary or appropriate parts.[/b]
Using stipulative definition this same way we could say that the inability of a formal system to prove a self-contradictory expression makes this formal system "A big fat cow".
Moreover the Godel sentence is not a self-contradiction.
Again, 'incomplete' in this context is given a stipulative technical definition pertaining to mathematical logic. The use of 'incomplete' in mathematics is not claimed to pertain to all the other everyday meanings or other technical meanings in other fields of study. The nature of stipulative technical definitions is not even something that one should have to point out in a philosophy forum.
You misquoted me. An epistemological antinomy
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44)
Does say that the inability to prove a SELF-contradictory expression
"can likewise be used for a similar undecidability proof..."
The proof itself does not mention 'epistemological antinomy'. Godel's footnote pertains to analogies of the proof, the proof itself does not invoke a notion of 'epistemological antimony'. Godel is talking about heuristic insight there, which is an analogy (not an identification) between certain informal antinomies and his mathematical proof. It is quite an error to grasp onto a footnote out of context while ignoring the actual hard mathematical proof.
Again, however one characterizes the Godel sentence, it is not a contradiction. Indeed it is a true sentence of arithmetic.
This G is unprovable in F because this G is nonsense in F
[b]That G is nonsense in F does not show that there is anything wrong with F
the issue is ALL G's fault.[/b]
Quoting PL Olcott
The Godel sentence is not a contradiction and it is not nonsense. It is a statement of arithmetic. And G is true, and G is true if and only if G is not provable in a theory such as PA. That doesn't make G a contradiction nor nonsense. And the theory itself does not prove G (first incompleteness) and the theory itself does not prove that it does not prove G (second incompleteness).
This all can be understood by simply reading an introductory textbook in mathematical logic.
By saying that F is incomplete when the real issue is that G is incorrect the blame
for the unprovability of G is F it misallocated.
Quoting TonesInDeepFreeze
The Gödel sentence itself cannot possibly be directly understood because all of its actual semantics are completely hidden from view. Because of this we must use these quotes to have a glimpse into his underlying reasoning:
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
...We are therefore confronted with a proposition which asserts its own unprovability. 15 ...
(Gödel 1931:43-44)
When G asserts its own unprovability in F the proof of G in F does require a sequence of inference steps in F that prove that they themselves do not exist. That unhides the whole essence of Gödel's proof where we can see WHY G is unprovable in F not merely THAT G is unprovable in F.
This G is unprovable in F because this G is nonsense and Gödel expressly states that this kind of nonsense "can likewise be used for a similar undecidability proof"
You seem to simply ignore the main points that prove my case.
...We are therefore confronted with a proposition which asserts its own unprovability. 15 ...
(Gödel 1931:43-44)
When I talk about that quote you simply change the subject to something else totally ignoring my analysis of it.
I pointed out that the footnote pertains to informal heuristic analogy and is not part of the formal proof itself. That is not changing the subject. And a proper analysis of the proof is not advanced by taking a footnote that is part of the informal remarks about the proof out of context. A proper analysis is to address the actual formal proof. Moreover, since Godel's original paper, the theorem has been strengthened to Godel-Rosser, and the context has been sharpened by the subjects of recursion and model theory, and the notation has been modernized, and the proofs have been streamlined, and the whole subject has been given greater elucidation and presentation. And all of that is provided by many introductory textbooks in mathematical logic. Thus, a proper analysis of incompleteness begins with study of an introductory textbook in mathematical logic. It is sure that flitting among snippets on the Internet and mere cursory readings of even original sources, while skimming all of that not toward step by step mathematical understanding and verification of inferences, to the point of seizing upon footnotes out of context and not understood, is not the way to an understanding or analysis of the subject.
By the way, the only authorized and authoritative translation is the one in van Heijenoort's anthology.
The important point is that it self-contradictory expressions are still considered valid proof of undecidability and this proves that the entire notion of undecidability that ALL mathematical incompleteness depends is totally bogus. When we understand and accept that then your repeatedly going back to utterly extraneous details to this point is simply deflection.
Try and show how it makes sense to base undecidability on self-contradictory expressions or acknowledge that you do not understand that Tarski Undefinability is anchored in the Liar Paradox and we can move forward. Simply changing the subject to something else blocks all actual progress.
No one anywhere on any forum ever addressed the issue that:
(a) Undecidability is fully met by self-contradictory expressions.
(b) Self-contradictory expressions cannot possibly be truth bearers.
(c) Formal systems requires that all of its expressions must truth bearers.
Everyone everywhere used the change the subject form of rebuttal or denied the verified facts stated above.
Mentioning that you believe that (a) (b) or (c) is incorrect once and then dropping it is not enough to arrive at closure. I think that our sticking point may be (a). You disbelieve (a) yet will not allow me sufficient dialogue to prove (a).
Self-contradictions are false in all models.
For a given model M, every sentence in the formal language is either true in M or false in M, and not both.
I don't preclude anyone from posting a proof of anything they want to proof. I have no such power.
OK now we are getting somewhere. "This sentence is not true" cannot be true because that would make it untrue and cannot be false because that would make it true. Thus it is not a bearer of truth anywhere.
Every closed WFF of the formal language of any formal system must be true or false thus the Liar Paradox is excluded from every formal system and Tarski was wrong for including it.
Again, Tarski did not "include" such a sentence, especially an informal one.
Again, in context of Tarski's undefinability, it's not a matter of whether the liar sentence is or is not a truth bearer, rather the matter is that, in the relevant contexts, there is no formalization of such a sentence.
To say that Tarski's proof is wrong because he uses a liar sentence as if it is a truth bearer is to get it all backwards. Tarski doesn't at all say that there is a formal sentence in the manner of the liar sentence that is a truth bearer. He says even more than the contrary: that, in the relevant contexts, there does not even exist such a formal sentence.
All of that can be understood in detail and with all the groundwork by studying an introductory textbook in mathematical logic.
Tarski's undefinability theorem is that, in the relevant contexts, there is no formula T(n) that is satisfied by all and only those n that are Godel numbers of true sentences of arithmetic. That is proven by showing that if there were such a T(n) then there would be a sentence H such that H is true if and only if H is false, but since there is no such H, there is no such T(n).
Again, he is not claiming there is such an H, let alone that he is not claiming that there is such an H that is true or that is false. Rather, toward a contradiction, we suppose there is a T(n) as described above, then we derive the absurdity that there is an H that is true if and only if it is false, so we conclude, courtesy argument by contradiction, that there is no such T(n).
Again, Tarski was not trying to figure out how to deal with the liar paradox. Rather, he used the fact that there is no sentence that is true if and only if it is false to prove that there is no formula in the language of arithmetic that defines the set of true sentences of arithmetic.
Theorem: There is no formula T(x) such that for every sentence S, T(g(S)) is true if and only if S is true.
Proof:
Toward a contradiction, suppose there is such a T(x).
So, there is a formula D(x) such that for every numeral m, D(m) is true if and only if m is the numeral for the Godel number of a formula P(x) such that P(m) is false. (The steps in obtaining this line from the previous line are not included in the article on which this summary is based.)
D(g(D(x))) is true
if and only if
g(D(x)) is the numeral for the Godel number of a formula P(x) such that P(g(D(x))) is false.
Toward a contradiction, suppose D(g(D(x))) is true.
So g(D(x)) is the numeral for the Godel number of a formula P(x) such that P(g(D(x))) is false.
g(D(x)) is g(P(x)), so D(x) is P(x), so D(g(S(x))) is P(g(S(x))), so D(g(S(x))) is false. Contradiction.
Toward a contradiction, suppose D(g(D(x))) is false.
So it is not the case that g(D(x)) is the numeral for the Godel number of a formula P(x) such that P(g(D(x))) is false.
So D(g(D(x))) is true. Contradiction.
So there is no formula T(x) such that for every sentence S, T(g(S)) is true if and only if S is true.
/
Theorem: There is no formula T(x) such that for every sentence S, S is true if and only if T(g(S)) is true.
Proof:
Lemma: For every formula P(x) there is a sentence D such that D <-> P(g(D)) is true. (The proof of this lemma is not included here.)
Toward a contradiction, suppose there is a formula T(x) such that for every sentence S, S is true if and only if T(g(S)) is true.
So, for every sentence S, S <-> T(g(S)) is true.
But, by the lemma, there is a sentence D such that D <-> ~T(g(D)) is true. But also, D <-> T(g(D)) is true. Contradiction.
So there is no formula T(x) such that for every sentence S, S is true if and only if T(g(S)) is true.
It does. Indeed Godel's original proof was about such a system.
As long as the system is recursively axiomatizable and with recursive inference rules, consistent and arithmetically adequate, it is incomplete.
But people use the expression all the time in daily ordinary communications. Why reject?
Quoting PL Olcott
It wasn't "Did you lie?" we were talking about. It was "You lied, didn't you?" That was the original sentence. It cannot be chopped into two sentences. It is one sentence, which is both declarative and questioning form. It means, you lied, and it is true.
"Isn't it a beautiful day?" Another example saying that it is true that it is a beautiful day, but in questioning form.
If it is false, then it is true.
If it is true, then it is false.
The If parts need reference (under what ground it is false or true) to claim it is either false or true.
There is no indication of what the reference for presuming it is false or true.
Hence the arguments are invalid.
Natural language cannot be accurately evaluated until it is translated into some totally precise form. An expression that is both a statement and a question cannot be properly evaluated by any Boolean True(L, x) predicate.
It must be broken down into its constituent parts. The question aspect must rejected by any Boolean True(L, x) predicate as not a truth bearer.
If we ask people is this sentence true: "What time is it?" the smartest ones will say type mismatch error. Those that have less insight will simply be confused.
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44)
Basically I am saying that self-contradictory expressions such as the epistemological antinomies that Gödel refers to are not truth bearers (neither true nor false) thus must be excluded from formal systems and never any part of any formal proof.
Every truth or falsity must be derived from some facts in the world or the known axioms which are self evidently true. The paradox starts with the obscure sentence whose truth falsity value no one knows where or what it was derived from. Therefore there is no point for you progressing into the If then arguments or inferencing. That is my point.
What time is it? can be true or false depending on what was the criteria of the truth.
If the criteria of truth was whether someone asked the question or not, and someone asked the question, then it was true that the question was asked.
Also it can be inferred and reasoned that the person who asked the question didn't know the time. If the criteria of truth was, if there was anyone who didn't know the time, then it was true that the questioner didn't know the time at the time of asking the question.
If you didn't have the criteria of truth, then you wouldn't have the information regarding true or false on the question, which sounds obvious then you don't know what the context of the question was about, and you had no knowledge of what the criteria of truth of the expression was.
Often the smartest sounding folks can be the dumbest. You have to learn to think differently from others. If you sound the same as the others on these issues, then it wouldn't prove anything apart from that you have spent all your life browsing the internet. If you think differently and come up with different ideas, you may get told that you have a problem in logic by the crowds, but you know that you are thinking with your own mind, not just parroting or agreeing and yearning to be accepted to the group of the crowds.
I agree.
Quoting Corvus
Not when the entire notion of undecidability depends on these things. In that case we use your first quote as the basis of True(x). From this we derive False(x) ? True(¬x) and by this process the whole notion of undecidability utterly ceases to exist.
In other words the fact that he cannot prove that a lie is true he construes as proof that truth cannot be proven.
When we understand that self-contradictory expressions have no truth value and that formal systems require every proposition to have a truth value then we know that self-contradictory expressions are not allowed to exist in any formal system or formal proof.
Here is where is says he includes it
https://liarparadox.org/Tarski_247_248.pdf
"In accordance with the first part of Th. I we can obtain the negation
of one of the sentences in condition (?) of convention T of § 3..." (275)
His actual formalized Liar Paradox
x ? True if and only if p
where the symbol 'p' represents the whole sentence x
"...as a consequence of the definition of the symbol 'Pr' (provided we
replace 'Tr' in this convention by 'Pr')." (275)
His Liar Paradox: x ? True if and only if p
is converted to Line (1) of the proof.
His actual proof based on his Liar Paradox
https://liarparadox.org/Tarski_275_276.pdf
Here is the Tarski Undefinability Theorem proof
(1) x ? Provable if and only if p // assumption
(2) x ? True if and only if p // assumption
(3) x ? Provable if and only if x ? True.
(4) either x ? True or x? ? True; // axiom: ~True(x) ? ~True(~x)
(5) if x ? Provable, then x ? True; // axiom: Provable(x) ? True(x)
(6) if x? ? Provable, then x? ? True; // axiom: Provable(~x) ? True(~x)
(7) x ? True
(8) x ? Provable
(9) x? ? Provable
:ok:
Quoting PL Olcott
In "This sentence is false", whether "is false" or "is true" referred to the subject of the sentence "The sentence" or the whole sentence "This sentence is false" was obscure. Would this be part of the undecidability? Or is it for something else? If for something else, then can you give a few example of the undecidability?
If you say, natural language must be translated into some totally precise form (I take it to axiomatic or formal language.), then questioning sentences can be translated into declarative or descriptive form, which can make them truth bearers.
All linguistic expressions are usually interpreted into the hidden or suggestive meanings in practical conversations. For example, if you say "Are you a non-native English speaker?", to mean polite way of saying "You must have flunked your English in school.", or "What time is it now?" to suggest, "It is time to prepare some dinner. I am bloody hungry the now." ... etc.
"This sentence is not true" is called the strengthened Liar Paradox and is its best form.
If it is true that makes it untrue if it it false that makes it true. This proves that it is neither true nor false.
Quoting Corvus
Facts of the world can be translated into axioms of the correct model of the current world.
L is a formal system of the two types of axioms.
https://www.liarparadox.org/Wittgenstein.pdf essentially states this:
True(L, x) ? ?x ? L (L ? x)
False(L, x) ? ?x ? L (L ? ¬x)
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. https://en.wikipedia.org/wiki/Undecidable_problem
In other words the input to the decision problem is neither true nor false, thus must be excluded on this basis: ¬Proposition(L, x) ? (¬True(L, x) ? ¬False(L, x))
The Liar Paradox is an epistemological antinomy.
...14 Every epistemological antinomy can likewise be used for a similar undecidability
proof...(Gödel 1931:43-44)
Parphrased as:
Every expression X that cannot possibly be true or false proves that the formal system F cannot correctly determine whether X is true or false. Which shows that X is undecidable in F.
Which shows that F is incomplete, even though X cannot possibly be a proposition in F because propositions must be true or false.
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.
https://en.wikipedia.org/wiki/Proposition
"This sentence is not true." can be true in the form of the sentence X is not true in grammar. Nothing wrong with that. But the content of the sentence is unclear. It doesn't say which sentence it is talking about, and "not true" in what sense. So, it is both true and unclear.
Quoting PL Olcott
This wiki document needs to be verified, the wiki says. But going back to the OP, you need to bring out some arithmetic sentences or expressions, which proves Tarski's undefinability is correct or incorrect. And then we will try them under HOL, and see if it is still valid.
In FOL or PL, "X is not true" depends on the content of X.
In the traditional propositional logic, there is no option for that, hence it is only true in grammatical form of the sentence. Some folks insist it is still true. Likewise "What time is it now?" is true in the form of grammar. So is, "There are the Martians living in Mars."
Thanks for the update, on how you are trying to soothe your ego.
You are not paying attention.
(a) If it is true that makes it untrue so it can't be true.
(b) If it is false that makes it true so it can't be false.
(c) Therefore it can't be true or false thus not a proposition in 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. https://en.wikipedia.org/wiki/Proposition
If it can't be a proposition then it must be rejected by any logic system
from propositional logic on up to higher order logic.
https://iep.utm.edu/propositional-logic-sentential-logic/
All other sources agree.
Undecidability
Definition: A decision problem is a problem that requires a yes or no answer.
Definition: A decision problem that admits no algorithmic solution is said to be undecidable.
https://www.cs.rochester.edu/u/nelson/courses/csc_173/computability/undecidable.html
Undecidable
Not decidable as a result of being neither formally provable nor unprovable.
https://mathworld.wolfram.com/Undecidable.html
Incomplete(F) ? ?x ? L ((L ? x) ? (L ? ¬x))
Undecidability
The non-existence of an algorithm or the impossibility of proving or disproving a statement within a formal system.
https://encyclopediaofmath.org/wiki/Undecidability#:~:text=The%20non%2Dexistence%20of%20an,statement%20within%20a%20formal%20system.
It seems that you are not able to tell the difference between propositional logic, predicate logic and HOL. What you were saying is confined to propositional logic. But once you are in the realm of predicate logic and upwards, the concept of truths becomes multifaceted nature.
The sentence, "This sentence is not true." can be true, unknown, false or contradictory depending on the condition of truth.
The Liar Paradox written in Minimal Type Theory:
LP := ~True(LP)
Which says ~True(~True(~True(~True(~True(...)))))
Minimal Type Theory (YACC BNF)
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
The same thing can be done in Prolog with the same result.
Prolog specifically detects the "infinite structure" and rejects it.
Every increment of HOL above FOL quantifies over expressions of the next lower order. FOL quantifies over propositions, thus propositions are the ground level of all every order of logic.
That is like saying that a dead mouse can be a type of office building.
"This sentence is not true" is not a truth bearer thus not a proposition thus cannot be included in any Boolean logic system.
This seems to be 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.
Your claim that FOL quantifies over propositions doesn't make sense. FOL can use the variables in the individuals and subjects in the sentence. Not over the propositions.
Your point is locked up in the propositional logic only, not seeing further into the other domains of Logics.
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.
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.
Good job that is a perfect analogy!
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.
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}.
Quoting 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.
Quoting PL Olcott
You have been reading too much Wiki pages, and they can lead you to the wrong places unfortunately.
Quoting 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}
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.
Quoting 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.
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.
Quoting PL Olcott
In HOL, "What time is it?" would be translated into computable format, and can be processed for the proper truth values.
Quoting 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 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
Quoting 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
Quoting 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
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 !! Nonsense is just a colloquial expression saying, no you are bloody wrong mate.
Quoting 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.
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.
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.
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.
Please reread my post above.
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.
Quoting 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.
Quoting Corvus
Yet again can possibly be resolved to a value of true or false depending on location.
Quoting 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
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
Quoting 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".
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
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?
Quoting PL Olcott
Could you please explain that in plain English? And how is it related to our discussion?
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.
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.
Not at all every declarative sentence is {True, False} or incorrect.
Quoting Corvus
Prolog does not simply assume that every statement is True or False, thus can screen
out epistemological antinomies that are simply incorrect.
(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.
(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.
(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."
https://en.wikipedia.org/wiki/Second-order_logic
(under MetaLogical results).
Could you demonstrate your point with some example proofs?