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.
— 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. — 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? — 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.One can formalize the semantics—define truth—of lower order — Corvus
It sounds like Tarski's indefinability theorem is only applicable to arithmetical truths according to the dictionary. — Corvus
What is PA?The full actual proof: https://liarparadox.org/Tarski_275_276.pdf
Is the actual Liar Paradox in PA ? — 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.
Ok, Peano. :up:https://en.wikipedia.org/wiki/Peano_axioms PA = (Peano Arithmetic) — PL Olcott
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
That's cool Olcott.I have been working on self-referential paradox for two decades. — 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?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? — Corvus
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
From your coding, it seems no problem for HOL dealing with the Liars paradox and also Tarksi's undefinability. — Corvus
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. — PL Olcott
Isn't HOL the expanded logical system from the other simpler ones with the relation and operation variables in the formulas? — Corvus
This eliminates this terrible mistake by Gödel — PL Olcott
In simple English, please, please make clear just what Godel's terrible mistake was. — tim wood
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.