The posts have come full circle. If any new points arise, I'll consider addressing them. — TonesInDeepFreeze

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

I didn't say that it is not the case that undecidability is fully met by self-contradictory expressions. I didn't say that because I don't know what "undecidability is fully met by self-contradictory expressions" is supposed to mean.

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.

Self-contradictions are false in all models.
For a given model M, every sentence in the formal language is either true in M or it is false in M. — TonesInDeepFreeze

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.

When we are studying formal languages, formal semantics and formal theories, we would need to know how "This sentence is not true" would be formalized, or even if it can be formalized. Tarski is not merely addressing an informal paradox, but rather he is using that informal paradox to figure out how to prove a certain formal theorem. The figuring out how to prove is not itself formal, and the formal proof does not use a liar sentence but rather the proof is that, in the relevant contexts, there is no formalization of the liar sentence.

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.

I've posted explanation previously in this forum. But it seems it needs to be resaid:

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.

Here are some of the details:

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.

There was discussion about whether incompleteness pertains to systems with infinitely many types

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.

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. — PL Olcott

But people use the expression all the time in daily ordinary communications. Why reject?

The sentence: "Did you lie?"
is not a truth bearer thus would be rejected by a correct Truth Predicate. — 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.

"This sentence is false."

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.

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.
— PL Olcott
But people use the expression all the time in daily ordinary communications. Why reject? — Corvus

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.

"This sentence is false."

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. — Corvus

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

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. — PL Olcott

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.

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. — PL Olcott

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.

Every truth or falsity must be derived from some facts in the world or the known axioms which are self evidently true. — Corvus

I agree.

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

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. — TonesInDeepFreeze

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.

Again, Tarski did not "include" such a sentence, especially an informal one. — TonesInDeepFreeze

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

I agree. — PL Olcott

:ok:

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. — 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?

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. — PL Olcott

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.

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? — Corvus

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

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. — 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" is called the strengthened Liar Paradox and is its best form. — PL Olcott

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

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

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. — PL Olcott

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

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. — Corvus

Thanks for the update, on how you are trying to soothe your ego.

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

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/

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. — Corvus

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.

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. — PL Olcott

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.

Will have reads and get back to your point on this part later.

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

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.

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. — Corvus

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.

The sentence, "This sentence is not true." can be true, unknown, false or contradictory depending on the condition of truth. — Corvus

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.

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. — PL Olcott

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.