↪PL Olcott And this is just no correction at all. Near as i can tell from both reading your posts and your listed citations, all you have done is invoke an idea of a list of propositions that you have decreed "true facts." And there being no undecidable propositions among them - being excluded by you - you declare undecidability corrected. Unless you can mix in some sense, this stands both as nonsense and nonsensical — tim wood

When we have all of the truth facts of the world or even all the true facts about logic, math and computation then it is easy to see that epistemological antinomies and their negation cannot be derived from these true facts. LP := ~True(L, LP) then True(L, LP) is false and True(L, ~LP) is false.

The only issue that I am correcting is the notion of decidability.
— PL Olcott
A great thing! But tell, how have you corrected it? — tim wood

If there are no sequence of truth preserving operations from the verbal semantic meaning of expression x {true on the basis of its meaning} to x or ~x then the expression is rejected as not a truth bearer thus a type mismatch error for every system of bivalent logic. LP := ~True(L, LP) is the best known example of this.

Assuming then it returns true for all true strings and false for all false ones, right? — ssu

Yes and non truth-bearers are screened out.
Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x))
False ≡ True(L,~x))

So are you going here for the solution for the Entscheidungsproblem? Seems something like that. — ssu

Yes. https://simple.wikipedia.org/wiki/Entscheidungsproblem

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

Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x))

Epistemological antinomies no longer for the basis for any undecidability proof they are
simply rejected as a type mismatch error for every formal system of bivalent logic.

So with this assumption you think you can state that the Church-Turing thesis has no truth-bearing? — ssu

The only issue that I am correcting is the notion of decidability.
The notion of computation remains the same.

Then why bother with a machine/program? You have simply gone to the trouble of creating a data-base - in theory because there are significant problems im creating one for real. — tim wood

I am referring to the finite set of finite strings that encode the actual general knowledge true facts of the world. I refer to general knowledge because this is finite. That no one has written them all down in one place does not mean that they do not exist.

The only reason that "cats are animals" is true is that it is stipulated to be true thus allocating semantic meaning to otherwise utterly meaningless finite strings. Language different than English does this same thing with their own set of finite strings.

So far I think your machine just generates strings of symbols as candidates for inclusion in a list, but that apparently require the judgment of a person for that inclusion. — tim wood

We simply correctly encode all of the true facts of the world. When the discussion
devolves into "facts according to who" I lose interest because the discussion has
devolved away from actual truth.

But these associations are probabilistic only, and neither in themselves truth bearing or producing — tim wood

In other words you seem to believe that "a cat is probably an animal" and "a cat is probably not a fifteen story office building". I disagree.

That's a pretty good definition! But you're missing the whole point. Who or what defines, and on what basis or by what criteria? If it's humans all the way down, I'll take that as an answer, but that will leave the question as to how your whole program will work, in as much as it will have to be preloaded with that which it is supposed to produce. — tim wood

Yes it is the case that only humans have a complex language, however, apes have learned a symbolic language known as Yerkish. https://en.wikipedia.org/wiki/Yerkish

There is a data structure known as a knowledge ontology that is based on a directed graph.
https://en.wikipedia.org/wiki/Ontology_(information_science)

A knowledge ontology has a unique integer (such as the CYC project's use of the 128-bit GUIDs) for each sense meaning of every word. https://en.wikipedia.org/wiki/Cyc

A word is a string (AKA sequence) of characters such as "dog". The first sense meaning is the most common one: https://www.merriam-webster.com/dictionary/dog# These differing sense meanings have an integer index in dictionaries. A knowledge ontology might require an ISO standard dictionary so that its unique sense meanings expressed as 128-bit integers can correspond to their sequence of characters in this IOS standard dictionary.

A knowledge ontology is an inheritance hierarchy of these sense meanings. This means that the sense meaning of {dog} (the animal) gets most of its meaning from {animal} and only adds details that distinguish a {dog} from other {animals}.

I'll try to make it simpler. Given some string, call it Σ, we can start by supposing that Σ is/is not meaningful, is/is not true. How do you know/decide? Because I infer you have your program do it, the question is really, how does your program decide? — tim wood

Facts are sentences that are defined as true. Cats <are> Animals is defined as true.
The otherwise totally meaningless sequence of letters of "cats" and "animals" are defined to have the <is a type of> relation to each other.

All of the facts about the world work this same way. You wanted it simple and provided a complex example. In one case "Σ" is a Greek letter. Even this begs the question: What is Greek? and What is a letter?

https://www.mathsisfun.com/algebra/sigma-notation.html requires a whole mathematical infrastructure.

Ah, meaning. What is that? How does your program assess or even recognize meaning? I am asking the simplest and most basic questions because it seems to me you must have both asked and answered them. But so far I have no evidence of that in this thread, or seen it in your other threads. — tim wood

https://en.wikipedia.org/wiki/Ontology_(information_science)
of Rudolf Carnap / Richard Montague {meaning postulates} that stipulate relations
between finite strings as providing the semantic meanings that form an accurate
model of the general knowledge of the actual world.

Rudolf Carnap told Willard Van Orman Quine that the otherwise totally
meaningless finite string of "Bachelor(x)" is defined as the otherwise totally
meaningless finite string "~Married(x)" and Quine just could not get it.

The full definition of "Married(x)" entails (at least) billions of other meaning
postulates defining "Human(x)".

{All cats are animals}
— PL Olcott
You have a programming language - where does a statement about cats come from? How do you know "no cats are animals" is false and not itself an axiom? — tim wood

Expressions that are {true on the basis of meaning} are ONLY
(a) A set of finite string semantic meanings that form an accurate
model of the general knowledge of the actual world.

(b) Expressions derived by applying truth preserving operations to (a).

The above algorithm specifies True(L,x) and False(L,x) defined
as True(L, ~x).

If we merely encoded all of the rules of algorithms, logic, and programming in a single formal system
— PL Olcott
All right, a programming language.
truth preserving operations (TPOS)
— PL Olcott
An example or two, please?

And the Truths these TPOs are expected to preserve, whence them - your having only a language? And, "no sequence"? How do you define "no sequence"? — tim wood

{All cats are animals}
{All animals are living things}
therefore {All cats are living things}

The principle of explosion is not truth preserving.
{All cats are animals} // axiom
{No cats are animals} // false assumption
therefore FALSE

That is the point. Not only have you not got it; it may not be achievable - that depending on the exact details and definitions. You invoke an oracle, but give no account of it other than some hand-waving. And what do you mean by "verified fact"? Is a verified fact different from just a fact? How do you verify it - what does verified mean? Do you even know what a fact is? Do you know the difference between fact and true? — tim wood

If we merely encoded all of the rules of algorithms, logic, and programming in a single
formal system then when when no sequence of truth preserving operations from these
basic axioms derives x or ~x then x can be rejected as a type mismatch error on the basis
that all formal systems of bivalent logic require every expression to be a truth-bearer.

↪PL Olcott The problem is that you have a set. But it is by no means clear how you create that set. — tim wood

That is not the point. The set of verified facts of the world is defined to exist, it is merely
not written down all in one place yet. LLM AI models might be able to achieve this
within a few years.

The point is that when we know all of the general knowledge facts of the world then
we can easily screen out every epistemological antinomy (as a type mismatch error
non-truth-bearer) that many of the undecidability proofs depend on. Tarski undefinability
proof depends on this.

https://liarparadox.org/Tarski_247_248.pdf
https://liarparadox.org/Tarski_275_276.pdf

(a) A set of finite string semantic meanings that form an accurate
model of the general knowledge of the actual world.
— PL Olcott
Ok, but how exactly do you decide what is, or is not, a member of this set? — tim wood

It is simply all of the details of every fact of the world. General knowledge is a finite set of axioms.

True(L,x)
— PL Olcott
Tell us, how do you know True(L,x) is true? — tim wood

Expressions that are {true on the basis of meaning} are ONLY
(a) A set of finite string semantic meanings that form an accurate
model of the general knowledge of the actual world.

(b) Expressions derived by applying truth preserving operations to (a).

True(English, "a cat is an animal") is true.

What's "general knowledge" supposed to mean as opposed to just "knowledge"? — Lionino

General knowledge can be expressed in a finite set of finite strings.
Specific knowledge of everything is unmanageably large and infinite.

It is the criticism of the liar paradox refering to nothing. It was discussed in the thread I linked. — Lionino

I have spent two decades on this. It <is> a truth predicate that would
work because Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) screens out
epistemological antinomies that Tarski get stuck on.

That is the naïve reply to sentences such as "This sentence is a lie". Claiming that it is not a truth-bearer is alike hand-waving, you must give some account as to how it is not a truth bearer. — Lionino

It is far too much to unpack all oat once.
I don't say: "This sentence is a lie",
I refer to the strengthened Liar Paradox: "This sentence is not true."

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

The means LP is rejected as not a truth bearer in Prolog because
it has an infinite cycle in its evaluation graph.

This sentence is not true.
What it is not true about?
It is not true about being not true.
What is it not true about being not true about?

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.