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

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

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

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

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

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

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

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

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

Please reread my post above. — Corvus

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

duplicate

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Good job that is a perfect analogy!

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

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

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

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.

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.

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.

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.

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

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

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

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.

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.

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

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.

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.

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 cannot provide for progress in a conversation by repeating that I cannot provide for progress in a conversation by repeating refutations and explanations that are ignored while what has been refuted is simply reasserted. — TonesInDeepFreeze

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 important point has been ignored. It's the other way around. — TonesInDeepFreeze

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.

I cannot provide for progress in a conversation by repeating refutations and explanations that are ignored while what has been refuted is simply reasserted. — TonesInDeepFreeze

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.

Mathematical logic does not assign "fault". Fault though would be vital to assign if one were a judge in a traffic accident case. — TonesInDeepFreeze

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.

The Godel sentence is not a contradiction and it is not nonsense. — 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"

Again, however one characterizes the Godel sentence, it is not a contradiction. Indeed it is a true sentence of arithmetic. — TonesInDeepFreeze

This G is unprovable in F because this G is nonsense in F
That G is nonsense in F does not show that there is anything wrong with F
the issue is ALL G's fault.

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

Godel never said any such nonsense that if a system proves a contradiction then the system is incomplete. Indeed, if a system proves a contradiction then the system is complete. — TonesInDeepFreeze

You misquoted me. An epistemological antinomy <is> a self-contradictory expression

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

No self-contradiction is provable in a consistent theory, irrespective of incompleteness. — TonesInDeepFreeze

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).
Incomplete does not retain any of its conventional meaning
incomplete: not having all the necessary or appropriate parts.

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

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

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.

There is no proof of G in F.

That's the point.

Too miss that point is to utterly not know what the theorem is about. — TonesInDeepFreeze

That there is no proof of nonsense does not make any formal system incomplete unless
Incomplete(F) is a euphemism for Incorrect(G).

Regarding Tarski's undefinablity theorem, Tarski proved that in certain systems, there does not even exist such a sentence. Not only did Tarski not use such sentences as a basis, he actually proved that such sentences don't even exist in the relevant systems. To not understand that is to not understand what the theorem is even about. — TonesInDeepFreeze

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.

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

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.

"Did you lie?" doesn't have a truth value, because it is not a declarative sentence. Indeed, interrogatory sentences do not appear as lines in proofs. — TonesInDeepFreeze

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

Corvus was testing the boundaries of what is included and what is not included by using a rhetorical question as a pseudo statement.

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

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.

Contrary to a claim made in this thread (and made by the same poster several other times in this forum), it is not the case the Godel sentence requires that there is a sequence of inference steps that prove that they don't exist (as has been explained several other times in this forum). — TonesInDeepFreeze

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