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

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.

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

Great link with much useful info to learn. Thank you PL.

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

Great link with much useful info to learn. Thank you PL. — Corvus

I am trying to see whether or not HOL actually defeats Tarski Undefinability.

I am trying to see whether or not HOL actually defeats Tarski Undefinability. — PL Olcott

One can formalize the semantics—define truth—of 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?

One can formalize the semantics—define truth—of 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? — Corvus

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.

One can formalize the semantics—define truth—of lower order — Corvus

It's been observed were truth so definable, then the usual reading of Godel's sentence, unprovable but true, would have been instead untrue but true. That implies that truth is not so definable. Not to be confused with determining whether some proposition is true or not true, which can usually be done.

Edit. Actually, this from Olcott's citation above:
"(f3) assuming that the class of all provable sentences of the metatheory is consistent, it is impossible to construct an adequate definition of truth in the sense of convention T on the basis of the metatheory."

Good points.

It's been observed were truth so definable, then the usual reading of Godel's sentence, unprovable but true, would have been instead untrue but true. — tim wood

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.

My copy of " A Dictionary of Philosophical Logic" by R. T. Cook says,

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

It sounds like Tarski's indefinability theorem is only applicable to arithmetical truths according to the dictionary. — Corvus

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 ?

Sure, I am currently reading on "High-Order Logics" by Andrew Bacon, and this is a really nice supporting thread for the reading. Thanks.

↪PL Olcott Sure, I am currently reading on "High-Order Logics" by Andrew Bacon, and this is a really nice supporting thread for the reading. Thanks. — Corvus

https://andrew-bacon.github.io/papers/Front%20matter.pdf

Here:
http://www.thatmarcusfamily.org/philosophy/Course_Websites/Readings/Tarski%20-%20The%20Concept%20of%20Truth%20in%20Formalized%20Languages.pdf
Is the whole paper. I cannot copy and paste from it.

I think you will find on p. 254 the requisite qualifications.

And it's worth noting that the languages referred to are all mathematical-logical languages, in the sense that any primitive language to be be discussed be translated into numbers, and the semantics of the language(s) being mathematical operations.

https://andrew-bacon.github.io/papers/Front%20matter.pdf — PL Olcott

That's the book.

s the whole paper. I cannot copy and paste from it.

I think you will find on p. 254 the requisite qualifications. — tim wood

Downloaded and saved into my iPad, thanks. Great reading material. :up: :pray:

The full actual proof: https://liarparadox.org/Tarski_275_276.pdf

Is the actual Liar Paradox in PA ? — PL Olcott

What is PA?

https://andrew-bacon.github.io/papers/Front%20matter.pdf — 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.

What is PA? — Corvus

https://en.wikipedia.org/wiki/Peano_axioms PA = (Peano Arithmetic)

https://en.wikipedia.org/wiki/Peano_axioms PA = (Peano Arithmetic) — PL Olcott

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.

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

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.

I have been working on self-referential paradox for two decades. — PL Olcott

That's cool Olcott.

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

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

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

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

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

that is, they will allow you to match a term against an uninstantiated
subterm of itself. — PL Olcott

From your coding, it seems no problem for HOL dealing with the Liars paradox and also Tarksi's undefinability.

From your coding, it seems no problem for HOL dealing with the Liars paradox and also Tarksi's undefinability. — Corvus

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.

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

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.

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

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.

Isn't HOL the expanded logical system from the other simpler ones with the relation and operation variables in the formulas? — Corvus

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

This eliminates this terrible mistake by Gödel — PL Olcott

In simple English, please, please make clear just what Godel's terrible mistake was.

My take so far is that you're referring to knowledge. That is, propositions (presumably) known to be true wrt some accepted criteria. Godel was not working with such systems: his propositions were not known to be either true or provable, but that both had to be demonstrated. He merely proved that such a program had built-in limits.

This eliminates this terrible mistake by Gödel: — PL Olcott

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

In simple English, please, please make clear just what Godel's terrible mistake was. — tim wood

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.