• PL Olcott
    516
    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.
  • Corvus
    3k
    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.
  • PL Olcott
    516
    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.
  • Corvus
    3k
    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?
  • PL Olcott
    516
    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.
  • tim wood
    8.7k
    One can formalize the semantics—define truth—of lower orderCorvus
    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."
  • PL Olcott
    516
    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.
  • Corvus
    3k
    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?
  • PL Olcott
    516
    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 ?
  • Corvus
    3k
    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
    516
    ↪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
  • tim wood
    8.7k
    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.
  • Corvus
    3k
    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:
  • Corvus
    3k
    The full actual proof: https://liarparadox.org/Tarski_275_276.pdf

    Is the actual Liar Paradox in PA ?
    PL Olcott
    What is PA?

    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.
  • Corvus
    3k
    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.
  • PL Olcott
    516
    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.
  • Corvus
    3k
    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?
  • PL Olcott
    516
    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)
  • Corvus
    3k
    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.
  • Corvus
    3k
    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.
  • PL Olcott
    516
    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.
  • Corvus
    3k

    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.
  • PL Olcott
    516
    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.
  • Corvus
    3k
    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.
  • PL Olcott
    516
    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
  • tim wood
    8.7k
    This eliminates this terrible mistake by GödelPL 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.
  • Corvus
    3k
    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).
  • PL Olcott
    516
    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.
bold
italic
underline
strike
code
quote
ulist
image
url
mention
reveal
youtube
tweet
Add a Comment

Welcome to The Philosophy Forum!

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.