• Re: The Halting Problem asks for too much

    From olcott@polcott333@gmail.com to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Sun Jan 25 20:31:23 2026
    From Newsgroup: comp.theory

    On 1/25/2026 2:44 PM, Richard Damon wrote:
    On 1/25/26 3:07 PM, olcott wrote:
    On 1/25/2026 1:54 PM, Richard Damon wrote:
    On 1/25/26 2:09 PM, olcott wrote:
    On 1/25/2026 12:36 PM, Richard Damon wrote:
    On 1/24/26 8:44 PM, olcott wrote:
    On 1/24/2026 6:52 PM, Richard Damon wrote:
    On 1/24/26 5:31 PM, olcott wrote:
    On 1/24/2026 4:25 PM, Richard Damon wrote:
    On 1/24/26 3:38 PM, olcott wrote:
    On 1/24/2026 1:52 PM, Richard Damon wrote:
    On 1/24/26 2:25 PM, olcott wrote:
    On 1/24/2026 1:23 PM, Richard Damon wrote:
    On 1/24/26 12:54 PM, olcott wrote:
    On 1/24/2026 11:10 AM, Richard Damon wrote:
    On 1/24/26 10:44 AM, olcott wrote:

    The statement that G is true and unprovable in PA has >>>>>>>>>>>>>>>> always been counter-factual. It has never actually been >>>>>>>>>>>>>>>> true <in> PA and that is why it is unprovable in PA. >>>>>>>>>>>>>>>
    Sure it is. At least it is a FACT that no natural number >>>>>>>>>>>>>>> will statisfy that relationship, and there is no proof in >>>>>>>>>>>>>>> PA of that fact.


    Have you ever heard of: "true in the standard model of >>>>>>>>>>>>>> arithmetic"?


    Sure, but they are not in Peano Arithmatic, but are >>>>>>>>>>>>> (generally) 1st order variations of the Peano Axioms which >>>>>>>>>>>>> lead to alternate number systems.

    Godel's proof is statd to be in a system with at least the >>>>>>>>>>>>> properties of Peano Arithmatic, having the ability to show >>>>>>>>>>>>> the properties of the "Natural Numbers"

    G||delrCOs incompleteness theorem only rCLworksrCY if
    one smuggles in an external notion of truth
    (truth in rao) and then pretends it is an
    internal notion of truth (truth in PA).
    If we refuse to make that identification,
    incompleteness evaporates.


    But Truth in N is part of Peano Arithmatic, as Peano
    Arithmatic is a axiomiation to create the Natural Numbers. >>>>>>>>>>>

    You have that backwards. Truth in rao requires PA
    as part of it, and PA itself has no notion of
    Truth in rao. PA only has proofs from its own axioms
    that can be construed as truth in PA, not truth in rao.


    Which means you don't understand what N actually is.

    Nothing can be "True in N" unless that truth comes from the >>>>>>>>> Axioms of PA, as N is the result of PA.


    combined with the meta-math external model.

    Nope. N is just a set of object built in the Formal System
    defined by PA. 0 comes from Axiom 1 which states there is a 0.


    If G is true and not provable then you have
    the wrong kind of true. I have known that
    the entire body of knowledge is a semantic
    tautology for 28 years.

    No, YOU do. The problem is Truth in the real world isn't based on
    being about to prove the fact, and most things are not actually
    provable, just well approximatable.


    That is why this insight was so important:
    "true on the basis of meaning expressed in language"
    I broke through the 75 year logjam of the analytic/synthetic
    distinction.

    In other words, you don't accept the Pythgorean Theorem as "True",
    since its Tru-ness doesn't come out of the meaning of its words.


    [meaning of its words]
    My sentence is not restricted to words and
    does include mathematical expressions.


    Then it accepts Godel's G as a valid statement

    That has no truth value in PA.

    and Goldbach's
    conjecture, even if improbably true, is a truth bearer.


    As a truth bearer with a currently unknown truth value.

    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    I never said anything about words.
    It took me 25 years to derive that exact phrase.

    You are just admitting to your own equivocation of meaning.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Mon Jan 26 14:55:14 2026
    From Newsgroup: comp.theory

    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You can deny >>>>>> the proof but you cannot perform what is meta-provably impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Mon Jan 26 09:22:01 2026
    From Newsgroup: comp.theory

    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You can deny >>>>>>> the proof but you cannot perform what is meta-provably impossible. >>>>>
    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to sci.logic,comp.theory,sci.math on Mon Jan 26 11:45:23 2026
    From Newsgroup: comp.theory

    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You can >>>>>>>> deny
    the proof but you cannot perform what is meta-provably impossible. >>>>>>
    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is true
    in PA?

    I thought you said that PA had to be able to determine the truth itself?
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 11:49:20 2026
    From Newsgroup: comp.theory

    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    On 1/25/26 3:07 PM, olcott wrote:
    On 1/25/2026 1:54 PM, Richard Damon wrote:
    On 1/25/26 2:09 PM, olcott wrote:
    On 1/25/2026 12:36 PM, Richard Damon wrote:
    On 1/24/26 8:44 PM, olcott wrote:
    On 1/24/2026 6:52 PM, Richard Damon wrote:
    On 1/24/26 5:31 PM, olcott wrote:
    On 1/24/2026 4:25 PM, Richard Damon wrote:
    On 1/24/26 3:38 PM, olcott wrote:
    On 1/24/2026 1:52 PM, Richard Damon wrote:
    On 1/24/26 2:25 PM, olcott wrote:
    On 1/24/2026 1:23 PM, Richard Damon wrote:
    On 1/24/26 12:54 PM, olcott wrote:
    On 1/24/2026 11:10 AM, Richard Damon wrote:
    On 1/24/26 10:44 AM, olcott wrote:

    The statement that G is true and unprovable in PA has >>>>>>>>>>>>>>>>> always been counter-factual. It has never actually been >>>>>>>>>>>>>>>>> true <in> PA and that is why it is unprovable in PA. >>>>>>>>>>>>>>>>
    Sure it is. At least it is a FACT that no natural number >>>>>>>>>>>>>>>> will statisfy that relationship, and there is no proof >>>>>>>>>>>>>>>> in PA of that fact.


    Have you ever heard of: "true in the standard model of >>>>>>>>>>>>>>> arithmetic"?


    Sure, but they are not in Peano Arithmatic, but are >>>>>>>>>>>>>> (generally) 1st order variations of the Peano Axioms which >>>>>>>>>>>>>> lead to alternate number systems.

    Godel's proof is statd to be in a system with at least the >>>>>>>>>>>>>> properties of Peano Arithmatic, having the ability to show >>>>>>>>>>>>>> the properties of the "Natural Numbers"

    G||delrCOs incompleteness theorem only rCLworksrCY if >>>>>>>>>>>>> one smuggles in an external notion of truth
    (truth in rao) and then pretends it is an
    internal notion of truth (truth in PA).
    If we refuse to make that identification,
    incompleteness evaporates.


    But Truth in N is part of Peano Arithmatic, as Peano
    Arithmatic is a axiomiation to create the Natural Numbers. >>>>>>>>>>>>

    You have that backwards. Truth in rao requires PA
    as part of it, and PA itself has no notion of
    Truth in rao. PA only has proofs from its own axioms
    that can be construed as truth in PA, not truth in rao.


    Which means you don't understand what N actually is.

    Nothing can be "True in N" unless that truth comes from the >>>>>>>>>> Axioms of PA, as N is the result of PA.


    combined with the meta-math external model.

    Nope. N is just a set of object built in the Formal System
    defined by PA. 0 comes from Axiom 1 which states there is a 0. >>>>>>>>

    If G is true and not provable then you have
    the wrong kind of true. I have known that
    the entire body of knowledge is a semantic
    tautology for 28 years.

    No, YOU do. The problem is Truth in the real world isn't based on >>>>>> being about to prove the fact, and most things are not actually
    provable, just well approximatable.


    That is why this insight was so important:
    "true on the basis of meaning expressed in language"
    I broke through the 75 year logjam of the analytic/synthetic
    distinction.

    In other words, you don't accept the Pythgorean Theorem as "True",
    since its Tru-ness doesn't come out of the meaning of its words.


    [meaning of its words]
    My sentence is not restricted to words and
    does include mathematical expressions.


    Then it accepts Godel's G as a valid statement

    That has no truth value in PA.

    Only if you are willing to say that the existance of some number doesn't
    have a truth value.


    and Goldbach's conjecture, even if improbably true, is a truth bearer.


    As a truth bearer with a currently unknown truth value.

    But, since it might be unprovable, that means it might not, or you
    accept that it could be true but unprovble.


    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    As you have effective admitted by not answering about my example with
    the Pythgorean Theorem.


    I never said anything about words.
    It took me 25 years to derive that exact phrase.

    What is language, but meaning expressed in "words".

    I think your problem is a fundamental failure to understand what you are talking about as you accept your own double-speak.


    You are just admitting to your own equivocation of meaning.



    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Mon Jan 26 10:58:21 2026
    From Newsgroup: comp.theory

    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You can >>>>>>>>> deny
    the proof but you cannot perform what is meta-provably impossible. >>>>>>>
    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is true
    in PA?

    I thought you said that PA had to be able to determine the truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to sci.logic,comp.theory,sci.math on Mon Jan 26 12:13:45 2026
    From Newsgroup: comp.theory

    On 1/26/26 11:58 AM, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>> can deny
    the proof but you cannot perform what is meta-provably
    impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is
    true in PA?

    I thought you said that PA had to be able to determine the truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.


    But Peano Arithmatic *IS* a standard model of arithmetic.

    The Induction Axiom makes it so.

    The other models tend to come from making a variant of PA by changing
    that 2nd order Induction Axiom to various first order versions to
    "simulate" its power using the rest of the Peano Axioms, and then adding something more to complete it.
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 11:23:56 2026
    From Newsgroup: comp.theory

    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    All of the LLM systems understand that
    "true on the basis of meaning expressed in language"
    breaks the logjam established in:

    "Two Dogmas of Empiricism" Willard Van Orman Quine https://www.theologie.uzh.ch/dam/jcr:ffffffff-fbd6-1538-0000-000070cf64bc/Quine51.pdf


    regarding the fundamental nature of truth itself
    previously called the analytic/synthetic distinction
    now renamed to the analytic/empirical distinction.

    These LLM systems do not yet understand that
    succinctly. It takes them some back and forth
    to understand that.

    As you have effective admitted by not answering about my example with
    the Pythgorean Theorem.


    I never said anything about words.
    It took me 25 years to derive that exact phrase.

    What is language, but meaning expressed in "words".

    I think your problem is a fundamental failure to understand what you are talking about as you accept your own double-speak.


    You are just admitting to your own equivocation of meaning.



    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Mon Jan 26 11:28:05 2026
    From Newsgroup: comp.theory

    On 1/26/2026 11:13 AM, Richard Damon wrote:
    On 1/26/26 11:58 AM, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>>> can deny
    the proof but you cannot perform what is meta-provably
    impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is >>>>>>>>> also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a >>>>>>> language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is
    true in PA?

    I thought you said that PA had to be able to determine the truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.


    But Peano Arithmatic *IS* a standard model of arithmetic.

    The Induction Axiom makes it so.


    PA is a firstrCaorder theory, not a model. The induction
    axiom does not force the standard model; PA has many
    nonrCastandard models. My metarCalevel truth predicate
    is proofrCatheoretic: True(PA, x) means PA reo x. It does
    not appeal to truth in the standard model of arithmetic.

    The other models tend to come from making a variant of PA by changing
    that 2nd order Induction Axiom to various first order versions to
    "simulate" its power using the rest of the Peano Axioms, and then adding something more to complete it.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 13:24:01 2026
    From Newsgroup: comp.theory

    On 1/26/26 12:23 PM, olcott wrote:
    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    And is build of "words" which is the symbolism of that langauge.

    Many things are "True", not based on the basic meaning of the "words",
    but becuase a (potentially infinite) sequence of operations defined in
    the system make it so.

    This is why the Pythagorean Theorem can be "True" even if it doesn't
    flow from the basic meaning of the words.

    One easy was to see this is that the Pythagorean Theorem is only True in
    Plain Geometry, but nothing in its "words" that define which form of
    Geometry we are in, which is determined only by which "version" of the
    5th postulate is in effect, and all the terms in the Theorem are defined
    in terms of things that are agnostic of that postulate.


    All of the LLM systems understand that
    "true on the basis of meaning expressed in language"
    breaks the logjam established in:

    "Two Dogmas of Empiricism" Willard Van Orman Quine https://www.theologie.uzh.ch/dam/jcr:ffffffff- fbd6-1538-0000-000070cf64bc/Quine51.pdf

    Which isn't about formal logic,


    regarding the fundamental nature of truth itself
    previously called the analytic/synthetic distinction
    now renamed to the analytic/empirical distinction.

    Which is a problem of general Philosophy, but not of Formal Logic that
    starts with a definition of it,


    These LLM systems do not yet understand that
    succinctly. It takes them some back and forth
    to understand that.

    And never can, as LLMs don't "understand" anything.

    It seems you don't even understand that conceptof "thinking" and "understanding".


    As you have effective admitted by not answering about my example with
    the Pythgorean Theorem.


    I never said anything about words.
    It took me 25 years to derive that exact phrase.

    What is language, but meaning expressed in "words".

    I think your problem is a fundamental failure to understand what you
    are talking about as you accept your own double-speak.


    You are just admitting to your own equivocation of meaning.






    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 12:43:45 2026
    From Newsgroup: comp.theory

    On 1/26/2026 12:24 PM, Richard Damon wrote:
    On 1/26/26 12:23 PM, olcott wrote:
    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    And is build of "words" which is the symbolism of that langauge.

    All of those copies of what I said ARE VERY SPECIFICALLY
    AND VERY INTENTIONALLY NOT LIMITED TO WORDS.

    Do I need to say that 10,000 times to get
    you to notice that I said it at least once?

    I build Minimal Type Theory entirely on the
    basis of the YACC grammar specification of the
    language of FOL.

    https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 16:58:35 2026
    From Newsgroup: comp.theory

    On 1/26/26 1:43 PM, olcott wrote:
    On 1/26/2026 12:24 PM, Richard Damon wrote:
    On 1/26/26 12:23 PM, olcott wrote:
    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    And is build of "words" which is the symbolism of that langauge.

    All of those copies of what I said ARE VERY SPECIFICALLY
    AND VERY INTENTIONALLY NOT LIMITED TO WORDS.

    Do I need to say that 10,000 times to get
    you to notice that I said it at least once?

    No just answer the question.

    But, I guess since you don't actually knoew what you mean, you can't do
    that,


    I build Minimal Type Theory entirely on the
    basis of the YACC grammar specification of the
    language of FOL.

    So?


    https://www.researchgate.net/ publication/331859461_Minimal_Type_Theory_YACC_BNF


    So, what is a "language" built on if not what it considers its "words"?

    And, how does you system handle the truth of something like the
    Pythagorean Theorem?

    Your repeated failure just proves that you CAN'T answer as you know your system is broken but need to continue clinging to its lie.
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 16:08:38 2026
    From Newsgroup: comp.theory

    On 1/26/2026 3:58 PM, Richard Damon wrote:
    On 1/26/26 1:43 PM, olcott wrote:
    On 1/26/2026 12:24 PM, Richard Damon wrote:
    On 1/26/26 12:23 PM, olcott wrote:
    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    And is build of "words" which is the symbolism of that langauge.

    All of those copies of what I said ARE VERY SPECIFICALLY
    AND VERY INTENTIONALLY NOT LIMITED TO WORDS.

    Do I need to say that 10,000 times to get
    you to notice that I said it at least once?

    No just answer the question.

    But, I guess since you don't actually knoew what you mean, you can't do that,


    I build Minimal Type Theory entirely on the
    basis of the YACC grammar specification of the
    language of FOL.

    So?


    https://www.researchgate.net/
    publication/331859461_Minimal_Type_Theory_YACC_BNF


    So, what is a "language" built on if not what it considers its "words"?



    All of the logic, math and computation languages
    are not grounded in words deep ship.

    And, how does you system handle the truth of something like the
    Pythagorean Theorem?


    written in PA syntax as:
    reCa reCb reCc (a-+a + b-+b = c-+c)

    Your repeated failure just proves that you CAN'T answer as you know your system is broken but need to continue clinging to its lie.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 17:36:05 2026
    From Newsgroup: comp.theory

    On 1/26/26 5:08 PM, olcott wrote:
    On 1/26/2026 3:58 PM, Richard Damon wrote:
    On 1/26/26 1:43 PM, olcott wrote:
    On 1/26/2026 12:24 PM, Richard Damon wrote:
    On 1/26/26 12:23 PM, olcott wrote:
    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    And is build of "words" which is the symbolism of that langauge.

    All of those copies of what I said ARE VERY SPECIFICALLY
    AND VERY INTENTIONALLY NOT LIMITED TO WORDS.

    Do I need to say that 10,000 times to get
    you to notice that I said it at least once?

    No just answer the question.

    But, I guess since you don't actually knoew what you mean, you can't
    do that,


    I build Minimal Type Theory entirely on the
    basis of the YACC grammar specification of the
    language of FOL.

    So?


    https://www.researchgate.net/
    publication/331859461_Minimal_Type_Theory_YACC_BNF


    So, what is a "language" built on if not what it considers its "words"?



    All of the logic, math and computation languages
    are not grounded in words deep ship.

    sure they are, when you consider a "word" to include the symbols and
    number they use.


    And, how does you system handle the truth of something like the
    Pythagorean Theorem?


    written in PA syntax as:
    reCa reCb reCc (a-+a + b-+b = c-+c)

    So, why is that true for EVERY a and b that are sides of a right triangle?

    Note, the Pythagorean Theorem isn't part of PA, but Plain Geometry.


    I guess you just belive in truth conditional logic.


    Your problem is you just don't know that truth or proof means because of
    your ignorance.


    Your repeated failure just proves that you CAN'T answer as you know
    your system is broken but need to continue clinging to its lie.



    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 16:44:48 2026
    From Newsgroup: comp.theory

    On 1/26/2026 4:36 PM, Richard Damon wrote:
    On 1/26/26 5:08 PM, olcott wrote:
    On 1/26/2026 3:58 PM, Richard Damon wrote:
    On 1/26/26 1:43 PM, olcott wrote:
    On 1/26/2026 12:24 PM, Richard Damon wrote:
    On 1/26/26 12:23 PM, olcott wrote:
    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    And is build of "words" which is the symbolism of that langauge.

    All of those copies of what I said ARE VERY SPECIFICALLY
    AND VERY INTENTIONALLY NOT LIMITED TO WORDS.

    Do I need to say that 10,000 times to get
    you to notice that I said it at least once?

    No just answer the question.

    But, I guess since you don't actually knoew what you mean, you can't
    do that,


    I build Minimal Type Theory entirely on the
    basis of the YACC grammar specification of the
    language of FOL.

    So?


    https://www.researchgate.net/
    publication/331859461_Minimal_Type_Theory_YACC_BNF


    So, what is a "language" built on if not what it considers its "words"?



    All of the logic, math and computation languages
    are not grounded in words deep ship.

    sure they are, when you consider a "word" to include the symbols and
    number they use.


    And, how does you system handle the truth of something like the
    Pythagorean Theorem?


    written in PA syntax as:
    reCa reCb reCc (a-+a + b-+b = c-+c)

    So, why is that true for EVERY a and b that are sides of a right triangle?

    Note, the Pythagorean Theorem isn't part of PA, but Plain Geometry.


    I guess you just belive in truth conditional logic.


    "true on the basis of meaning expressed in language"
    Inherently includes every element of the entire body
    of knowledge that can be expressed in any formal
    mathematical or natural language.


    Your problem is you just don't know that truth or proof means because of your ignorance.


    Your repeated failure just proves that you CAN'T answer as you know
    your system is broken but need to continue clinging to its lie.



    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 26 21:51:57 2026
    From Newsgroup: comp.theory

    On 1/26/26 5:44 PM, olcott wrote:
    On 1/26/2026 4:36 PM, Richard Damon wrote:
    On 1/26/26 5:08 PM, olcott wrote:
    On 1/26/2026 3:58 PM, Richard Damon wrote:
    On 1/26/26 1:43 PM, olcott wrote:
    On 1/26/2026 12:24 PM, Richard Damon wrote:
    On 1/26/26 12:23 PM, olcott wrote:
    On 1/26/2026 10:49 AM, Richard Damon wrote:
    On 1/25/26 9:31 PM, olcott wrote:
    On 1/25/2026 2:44 PM, Richard Damon wrote:
    If not, you don't know what you words mean,

    And how is "Meaning of its words" not about the WORDS?


    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"
    "true on the basis of meaning expressed in language"

    Which can't handle math.

    All math and logic has a language of math and logic.
    I literally spent 25 years coming up with that.

    And is build of "words" which is the symbolism of that langauge.

    All of those copies of what I said ARE VERY SPECIFICALLY
    AND VERY INTENTIONALLY NOT LIMITED TO WORDS.

    Do I need to say that 10,000 times to get
    you to notice that I said it at least once?

    No just answer the question.

    But, I guess since you don't actually knoew what you mean, you can't
    do that,


    I build Minimal Type Theory entirely on the
    basis of the YACC grammar specification of the
    language of FOL.

    So?


    https://www.researchgate.net/
    publication/331859461_Minimal_Type_Theory_YACC_BNF


    So, what is a "language" built on if not what it considers its "words"? >>>>


    All of the logic, math and computation languages
    are not grounded in words deep ship.

    sure they are, when you consider a "word" to include the symbols and
    number they use.


    And, how does you system handle the truth of something like the
    Pythagorean Theorem?


    written in PA syntax as:
    reCa reCb reCc (a-+a + b-+b = c-+c)

    So, why is that true for EVERY a and b that are sides of a right
    triangle?

    Note, the Pythagorean Theorem isn't part of PA, but Plain Geometry.


    I guess you just belive in truth conditional logic.


    "true on the basis of meaning expressed in language"
    Inherently includes every element of the entire body
    of knowledge that can be expressed in any formal
    mathematical or natural language.

    ONLY if meaning means the (possibly infinite) operation of the logical operations of the system to its axioms.

    That isn't the normal meaning of "meaning express in language", so you
    are just admitting to speaking with a forked toungue.

    For instance, the "Meaning" of the Pythgorean Theorem describes the
    operation of computing the square of the lengths of the sides adding to
    two side legs and seeing that it matchs the hypotenuse.

    But, its TRUTH doesn't come from that meaning, but from actually seeing
    that it DOES work, and that fact turns out to be provable, so we can
    know it works. At least if we are working in Plane Geometry.

    Thus, it is NOT the "meaning of the words" that makes it true, but the
    axioms of the system those words are put into that makes it true.

    It seewms you are just too stupid to understand that simple concept of
    what the "meaning" of a statement actually means, or what "True"
    actually means,



    Your problem is you just don't know that truth or proof means because
    of your ignorance.


    Your repeated failure just proves that you CAN'T answer as you know
    your system is broken but need to continue clinging to its lie.






    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@NoOne@NoWhere.com to sci.logic,sci.math,comp.theory,comp.ai.philosophy,alt.philosophy on Mon Jan 26 21:28:20 2026
    From Newsgroup: comp.theory

    On 1/26/2026 8:51 PM, Richard Damon wrote:
    On 1/26/26 5:44 PM, olcott wrote:>>
    "true on the basis of meaning expressed in language"
    Inherently includes every element of the entire body
    of knowledge that can be expressed in any formal
    mathematical or natural language.

    ONLY if meaning means the (possibly infinite) operation of the logical operations of the system to its axioms.


    You are the one that told me that proofs are
    not infinite. Did you forget that?
    --
    Copyright 2026 Olcott

    My 28 year goal has been to make
    "true on the basis of meaning expressed in language"
    reliably computable for the entire body of knowledge.

    This required establishing a new foundation
    for correct reasoning.
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Tue Jan 27 10:05:05 2026
    From Newsgroup: comp.theory

    On 26/01/2026 17:22, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You can >>>>>>>> deny
    the proof but you cannot perform what is meta-provably impossible. >>>>>>
    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.

    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY

    The above is not a notational convention. The symbols may be defined
    in some context but they are undefined elsewhere.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Tue Jan 27 10:17:08 2026
    From Newsgroup: comp.theory

    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>> can deny
    the proof but you cannot perform what is meta-provably
    impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is
    true in PA?

    I thought you said that PA had to be able to determine the truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Tue Jan 27 10:15:32 2026
    From Newsgroup: comp.theory

    On 26/01/2026 18:45, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You can >>>>>>>>> deny
    the proof but you cannot perform what is meta-provably impossible. >>>>>>>
    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY

    In outher words, you ACCEPT that the meta level can define what is true
    in PA?

    In the metatheory one can construct a model of PA. Everyting in that
    model can be proven in the metatheory is true in that model so it is
    true in some model of PA.

    I thought you said that PA had to be able to determine the truth itself?

    No, I said it doesn't. But what is provable in first order PA is true in
    every model of first order PA and what is not provable in PA is false in
    some model of first order PA. But there is no known way to extend this
    result to the second order, and the original PA is a sencond order
    theory.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Tue Jan 27 08:48:53 2026
    From Newsgroup: comp.theory

    On 1/27/2026 2:05 AM, Mikko wrote:
    On 26/01/2026 17:22, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You can >>>>>>>>> deny
    the proof but you cannot perform what is meta-provably impossible. >>>>>>>
    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.

    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY

    The above is not a notational convention. The symbols may be defined
    in some context but they are undefined elsewhere.


    Mendelson simply uses reo EYAR to indicate that EYAR is a theorem.
    reCx (True(x) rei reo EYAR)
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to comp.theory,sci.logic,sci.math on Tue Jan 27 09:32:42 2026
    From Newsgroup: comp.theory

    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>>> can deny
    the proof but you cannot perform what is meta-provably
    impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is >>>>>>>>> also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a >>>>>>> language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is
    true in PA?

    I thought you said that PA had to be able to determine the truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.


    That was Tarski's mistake. All of the expressions
    where True(L, x) is not computable x is semantically
    incoherent or outside of the domain of knowledge.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Wed Jan 28 11:40:26 2026
    From Newsgroup: comp.theory

    On 27/01/2026 16:48, olcott wrote:
    On 1/27/2026 2:05 AM, Mikko wrote:
    On 26/01/2026 17:22, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>> can deny
    the proof but you cannot perform what is meta-provably
    impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is also >>>>>>>> a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.

    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY

    The above is not a notational convention. The symbols may be defined
    in some context but they are undefined elsewhere.

    Mendelson simply uses reo EYAR to indicate that EYAR is a theorem.

    That is the usual metalogical notation.

    reCx (True(x) rei reo EYAR)

    Usually the symbol True, if used at all, is reserved for other purposes.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to comp.theory,sci.logic,sci.math on Wed Jan 28 11:54:17 2026
    From Newsgroup: comp.theory

    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>>>> can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA is >>>>>>>>>> also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a >>>>>>>> language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and
    WellFounded with two arguments. And you did not specify in which
    context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is
    true in PA?

    I thought you said that PA had to be able to determine the truth
    itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.

    All of the expressions where True(L, x) is not computable
    x is semantically incoherent or outside of the domain of knowledge.

    Computability does not depend on semantics or knowledge.
    --
    Mikko

    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to comp.theory,sci.logic,sci.math on Wed Jan 28 07:49:31 2026
    From Newsgroup: comp.theory

    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>>>>> can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA.
    All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA >>>>>>>>>>> is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a >>>>>>>>> language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and >>>>>>> WellFounded with two arguments. And you did not specify in which >>>>>>> context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is
    true in PA?

    I thought you said that PA had to be able to determine the truth
    itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.


    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    All of the expressions where True(L, x) is not computable
    x is semantically incoherent or outside of the domain of knowledge.

    Computability does not depend on semantics or knowledge.


    In this case it does
    My 28 year goal has been to make
    "true on the basis of meaning expressed in language"
    reliably computable for the entire body of knowledge.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to comp.theory,sci.logic,sci.math on Thu Jan 29 11:12:05 2026
    From Newsgroup: comp.theory

    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. >>>>>>>>>>>>>> You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA. >>>>>>>>>>>>> All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA >>>>>>>>>>>> is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x)))

    Those sentences don't mean anything without specificantions of a >>>>>>>>>> language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms
    of PA.

    There are no notational convention that defines True, False, and >>>>>>>> WellFounded with two arguments. And you did not specify in which >>>>>>>> context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what is >>>>>> true in PA?

    I thought you said that PA had to be able to determine the truth
    itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Thu Jan 29 07:57:29 2026
    From Newsgroup: comp.theory

    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. >>>>>>>>>>>>>>> You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA
    and that is the reason why an external truth in
    an external model cannot be proved internally in PA. >>>>>>>>>>>>>> All of these years it was only a mere conflation
    error.

    It is perfectly clear which is which. But every proof in PA >>>>>>>>>>>>> is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>
    Those sentences don't mean anything without specificantions of a >>>>>>>>>>> language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the
    axioms of PA and False for PA as refutable from the axioms >>>>>>>>>> of PA.

    There are no notational convention that defines True, False, and >>>>>>>>> WellFounded with two arguments. And you did not specify in which >>>>>>>>> context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what >>>>>>> is true in PA?

    I thought you said that PA had to be able to determine the truth >>>>>>> itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.


    If there was then there never would be a Tarski proof. https://liarparadox.org/Tarski_247_248.pdf
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Fri Jan 30 11:34:10 2026
    From Newsgroup: comp.theory

    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. >>>>>>>>>>>>>>>> You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>> and that is the reason why an external truth in
    an external model cannot be proved internally in PA. >>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof in >>>>>>>>>>>>>> PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>
    Those sentences don't mean anything without specificantions >>>>>>>>>>>> of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the >>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>> of PA.

    There are no notational convention that defines True, False, and >>>>>>>>>> WellFounded with two arguments. And you did not specify in which >>>>>>>>>> context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what >>>>>>>> is true in PA?

    I thought you said that PA had to be able to determine the truth >>>>>>>> itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.

    That would have no effet. Even if the metalanguage had an occcurs_check
    it would not be necessary to use it in a proof.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Fri Jan 30 08:35:02 2026
    From Newsgroup: comp.theory

    On 1/30/2026 3:34 AM, Mikko wrote:
    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. >>>>>>>>>>>>>>>>> You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>>> and that is the reason why an external truth in >>>>>>>>>>>>>>>> an external model cannot be proved internally in PA. >>>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof in >>>>>>>>>>>>>>> PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>>
    Those sentences don't mean anything without specificantions >>>>>>>>>>>>> of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational >>>>>>>>>>>> conventions that define True for PA as provable from the >>>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>>> of PA.

    There are no notational convention that defines True, False, and >>>>>>>>>>> WellFounded with two arguments. And you did not specify in which >>>>>>>>>>> context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what >>>>>>>>> is true in PA?

    I thought you said that PA had to be able to determine the
    truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.

    That would have no effet. Even if the metalanguage had an occcurs_check
    it would not be necessary to use it in a proof.


    It would only seem to have no effect because you
    never bothered to understand what an occurs_check is.

    Truth is computable because rCLmeaningful sentencerCY
    is defined as rCLsentence with a well-founded
    justification tree,rCY and evaluating any well-founded
    tree always terminates. Anything else isnrCOt truth-apt.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,sci.math,comp.ai.philosophy,comp.theory on Fri Jan 30 20:10:47 2026
    From Newsgroup: comp.theory

    On 1/30/2026 7:47 PM, Tristan Wibberley wrote:
    On 16/01/2026 04:03, olcott wrote:

    It is the same reCx ree T ((True(T, x) rei (T reo x))

    I still think you're asking for confusion with that use of the turnstile.


    I mean exactly what it says provable in the syntactic sense.
    For all of these years the model theoretic notion of true
    was simply totally wrong-headed.

    I have my 28 years of work boiled down to about 1/2
    page of text that five LLMs all agree would make:

    "true on the basis of meaning expressed in language"
    reliably computable for the entire body of knowledge.

    But it does make it very obvious that we should expect negation to be restricted in your system which might overcome a psychological hurdle.

    How is negation restricted in your system?

    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Sat Jan 31 10:41:30 2026
    From Newsgroup: comp.theory

    On 30/01/2026 16:35, olcott wrote:
    On 1/30/2026 3:34 AM, Mikko wrote:
    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout >>>>>>>>>>>>>>>>>> PA. You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>>>> and that is the reason why an external truth in >>>>>>>>>>>>>>>>> an external model cannot be proved internally in PA. >>>>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof in >>>>>>>>>>>>>>>> PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>>>
    Those sentences don't mean anything without
    specificantions of a
    language and a theory that gives them some meaning. >>>>>>>>>>>>>
    In other word you do not understand standard notational >>>>>>>>>>>>> conventions that define True for PA as provable from the >>>>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>>>> of PA.

    There are no notational convention that defines True, False, >>>>>>>>>>>> and
    WellFounded with two arguments. And you did not specify in >>>>>>>>>>>> which
    context your sentences are true or otherwise relevant. >>>>>>>>>>>>

    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define >>>>>>>>>> what is true in PA?

    I thought you said that PA had to be able to determine the >>>>>>>>>> truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results >>>>>> are related and there are much similarity in the proofs. Tarski did >>>>>> not use Turing machines in the proof but a computability proof must >>>>>> use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.

    That would have no effet. Even if the metalanguage had an occcurs_check
    it would not be necessary to use it in a proof.

    It would only seem to have no effect because you
    never bothered to understand what an occurs_check is.

    That assumption is false.

    Truth is computable because rCLmeaningful sentencerCY
    is defined as rCLsentence with a well-founded
    justification tree,rCY and evaluating any well-founded
    tree always terminates. Anything else isnrCOt truth-apt.

    That "bcause" is wrong. Whether a sentence has a well-founded
    justifiation tree is not computable, especially for arithmetic
    sentences.

    But that does not alter the fact that an existence or non-existence
    of a metalanguage feature that is not present in the justification
    tree is irrelevant.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Sat Jan 31 10:56:22 2026
    From Newsgroup: comp.theory

    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. >>>>>>>>>>>>>>>> You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>> and that is the reason why an external truth in
    an external model cannot be proved internally in PA. >>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof in >>>>>>>>>>>>>> PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>
    Those sentences don't mean anything without specificantions >>>>>>>>>>>> of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational
    conventions that define True for PA as provable from the >>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>> of PA.

    There are no notational convention that defines True, False, and >>>>>>>>>> WellFounded with two arguments. And you did not specify in which >>>>>>>>>> context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what >>>>>>>> is true in PA?

    I thought you said that PA had to be able to determine the truth >>>>>>>> itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.


    If there was then there never would be a Tarski proof. https://liarparadox.org/Tarski_247_248.pdf

    Irrelevant. Tarski's proof is what it is and there is no "occurs_check"
    there.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Sat Jan 31 09:23:51 2026
    From Newsgroup: comp.theory

    On 1/31/2026 2:41 AM, Mikko wrote:
    On 30/01/2026 16:35, olcott wrote:
    On 1/30/2026 3:34 AM, Mikko wrote:
    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout >>>>>>>>>>>>>>>>>>> PA. You can deny
    the proof but you cannot perform what is meta- >>>>>>>>>>>>>>>>>>> provably impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>>>>> and that is the reason why an external truth in >>>>>>>>>>>>>>>>>> an external model cannot be proved internally in PA. >>>>>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof >>>>>>>>>>>>>>>>> in PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>>>>
    Those sentences don't mean anything without
    specificantions of a
    language and a theory that gives them some meaning. >>>>>>>>>>>>>>
    In other word you do not understand standard notational >>>>>>>>>>>>>> conventions that define True for PA as provable from the >>>>>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>>>>> of PA.

    There are no notational convention that defines True, >>>>>>>>>>>>> False, and
    WellFounded with two arguments. And you did not specify in >>>>>>>>>>>>> which
    context your sentences are true or otherwise relevant. >>>>>>>>>>>>>

    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define >>>>>>>>>>> what is true in PA?

    I thought you said that PA had to be able to determine the >>>>>>>>>>> truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results >>>>>>> are related and there are much similarity in the proofs. Tarski did >>>>>>> not use Turing machines in the proof but a computability proof must >>>>>>> use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.

    That would have no effet. Even if the metalanguage had an occcurs_check
    it would not be necessary to use it in a proof.

    It would only seem to have no effect because you
    never bothered to understand what an occurs_check is.

    That assumption is false.


    So far you have conclusively proven that you
    do not understand what an occurs_check is.

    If you want to provide that you do know then
    you must provide all of the correct details.

    Merely claiming that my statement is false
    is an assertion entirely bereft of supporting
    reasoning thus inherently baseless.

    Truth is computable because rCLmeaningful sentencerCY
    is defined as rCLsentence with a well-founded
    justification tree,rCY and evaluating any well-founded
    tree always terminates. Anything else isnrCOt truth-apt.

    That "bcause" is wrong. Whether a sentence has a well-founded
    justifiation tree is not computable, especially for arithmetic
    sentences.


    My one half page of text explaining all of the key details
    of my 28 years of work was completely validated by five
    different LLM systems. proof theoretic semantics is correct
    model theoretic semantics is profoundly wrong-headed.

    Your ignorance of the details of well-founded proof theoretic
    semantics makes your rebuttal baseless.

    But that does not alter the fact that an existence or non-existence
    of a metalanguage feature that is not present in the justification
    tree is irrelevant.


    An existence or non-existence of a metalanguage feature
    is entirely anchored in a totally wrong-headed notion.
    The only way that this can be seen is to become an expert
    in well-founded proof theoretic semantics.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From olcott@polcott333@gmail.com to sci.logic,comp.theory,sci.math on Sat Jan 31 09:26:43 2026
    From Newsgroup: comp.theory

    On 1/31/2026 2:56 AM, Mikko wrote:
    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout PA. >>>>>>>>>>>>>>>>> You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>>> and that is the reason why an external truth in >>>>>>>>>>>>>>>> an external model cannot be proved internally in PA. >>>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof in >>>>>>>>>>>>>>> PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>>
    Those sentences don't mean anything without specificantions >>>>>>>>>>>>> of a
    language and a theory that gives them some meaning.

    In other word you do not understand standard notational >>>>>>>>>>>> conventions that define True for PA as provable from the >>>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>>> of PA.

    There are no notational convention that defines True, False, and >>>>>>>>>>> WellFounded with two arguments. And you did not specify in which >>>>>>>>>>> context your sentences are true or otherwise relevant.


    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define what >>>>>>>>> is true in PA?

    I thought you said that PA had to be able to determine the
    truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results
    are related and there are much similarity in the proofs. Tarski did
    not use Turing machines in the proof but a computability proof must
    use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.


    If there was then there never would be a Tarski proof.
    https://liarparadox.org/Tarski_247_248.pdf

    Irrelevant. Tarski's proof is what it is and there is no "occurs_check" there.


    Sure and a car that has a missing engine will always
    be a car that will not run.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Sun Feb 1 12:17:39 2026
    From Newsgroup: comp.theory

    On 31/01/2026 17:26, olcott wrote:
    On 1/31/2026 2:56 AM, Mikko wrote:
    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout >>>>>>>>>>>>>>>>>> PA. You can deny
    the proof but you cannot perform what is meta-provably >>>>>>>>>>>>>>>>>> impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>>>> and that is the reason why an external truth in >>>>>>>>>>>>>>>>> an external model cannot be proved internally in PA. >>>>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof in >>>>>>>>>>>>>>>> PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x )
    reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>>>
    Those sentences don't mean anything without
    specificantions of a
    language and a theory that gives them some meaning. >>>>>>>>>>>>>
    In other word you do not understand standard notational >>>>>>>>>>>>> conventions that define True for PA as provable from the >>>>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>>>> of PA.

    There are no notational convention that defines True, False, >>>>>>>>>>>> and
    WellFounded with two arguments. And you did not specify in >>>>>>>>>>>> which
    context your sentences are true or otherwise relevant. >>>>>>>>>>>>

    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define >>>>>>>>>> what is true in PA?

    I thought you said that PA had to be able to determine the >>>>>>>>>> truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results >>>>>> are related and there are much similarity in the proofs. Tarski did >>>>>> not use Turing machines in the proof but a computability proof must >>>>>> use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.


    If there was then there never would be a Tarski proof.
    https://liarparadox.org/Tarski_247_248.pdf

    Irrelevant. Tarski's proof is what it is and there is no "occurs_check"
    there.

    Sure and a car that has a missing engine will always
    be a car that will not run.

    That's true, too.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,comp.theory,sci.math on Sun Feb 1 12:28:05 2026
    From Newsgroup: comp.theory

    On 31/01/2026 17:23, olcott wrote:
    On 1/31/2026 2:41 AM, Mikko wrote:
    On 30/01/2026 16:35, olcott wrote:
    On 1/30/2026 3:34 AM, Mikko wrote:
    On 29/01/2026 15:57, olcott wrote:
    On 1/29/2026 3:12 AM, Mikko wrote:
    On 28/01/2026 15:49, olcott wrote:
    On 1/28/2026 3:54 AM, Mikko wrote:
    On 27/01/2026 17:32, olcott wrote:
    On 1/27/2026 2:17 AM, Mikko wrote:
    On 26/01/2026 18:58, olcott wrote:
    On 1/26/2026 10:45 AM, Richard Damon wrote:
    On 1/26/26 10:22 AM, olcott wrote:
    On 1/26/2026 6:55 AM, Mikko wrote:
    On 25/01/2026 15:30, olcott wrote:
    On 1/25/2026 5:24 AM, Mikko wrote:
    On 24/01/2026 16:18, olcott wrote:
    On 1/24/2026 2:23 AM, Mikko wrote:
    On 22/01/2026 18:47, olcott wrote:
    On 1/22/2026 2:21 AM, Mikko wrote:

    Anyway, what can be provven that way is true aboout >>>>>>>>>>>>>>>>>>>> PA. You can deny
    the proof but you cannot perform what is meta- >>>>>>>>>>>>>>>>>>>> provably impossible.

    The meta-proof does not exist in the axioms of PA >>>>>>>>>>>>>>>>>>> and that is the reason why an external truth in >>>>>>>>>>>>>>>>>>> an external model cannot be proved internally in PA. >>>>>>>>>>>>>>>>>>> All of these years it was only a mere conflation >>>>>>>>>>>>>>>>>>> error.

    It is perfectly clear which is which. But every proof >>>>>>>>>>>>>>>>>> in PA is also
    a proof in G||del's metatheory.

    reCx ree PA (-a True(PA, x) rei PA reo-a x ) >>>>>>>>>>>>>>>>> reCx ree PA ( False(PA, x) rei PA reo -4x )
    reCx ree PA ( -4WellFounded(PA, x) rei
    -a-a-a-a-a-a-a-a-a (-4True(PA, x) reo (-4False(PA, x))) >>>>>>>>>>>>>>>>
    Those sentences don't mean anything without
    specificantions of a
    language and a theory that gives them some meaning. >>>>>>>>>>>>>>>
    In other word you do not understand standard notational >>>>>>>>>>>>>>> conventions that define True for PA as provable from the >>>>>>>>>>>>>>> axioms of PA and False for PA as refutable from the axioms >>>>>>>>>>>>>>> of PA.

    There are no notational convention that defines True, >>>>>>>>>>>>>> False, and
    WellFounded with two arguments. And you did not specify in >>>>>>>>>>>>>> which
    context your sentences are true or otherwise relevant. >>>>>>>>>>>>>>

    rCLx is a single finite string representing
    a PArCaformula, such as rCy2 + 3 = 5rCO.
    True(PA, x), False(PA, x), and WellFounded(PA, x)
    are metarCalevel unary predicates classifying
    that formula by its provability in PA.rCY


    In outher words, you ACCEPT that the meta level can define >>>>>>>>>>>> what is true in PA?

    I thought you said that PA had to be able to determine the >>>>>>>>>>>> truth itself?

    We need a meta-level truth predicate anchored
    only in the axioms of PA itself and thus not
    anchored in the standard model of arithmetic.

    That predicate is not computable.

    That was Tarski's mistake.

    No, Tarski's proof is about a different problem, though the results >>>>>>>> are related and there are much similarity in the proofs. Tarski did >>>>>>>> not use Turing machines in the proof but a computability proof must >>>>>>>> use that.

    Because you refuse to understand the underlying
    details of what occurs_check means I cannot
    explain to you how Tarski erred.

    Irrelevant. There is no "occurs_check" in Tarski's proof.

    That would have no effet. Even if the metalanguage had an occcurs_check >>>> it would not be necessary to use it in a proof.

    It would only seem to have no effect because you
    never bothered to understand what an occurs_check is.

    That assumption is false.

    So far you have conclusively proven that you
    do not understand what an occurs_check is.

    That's false. Your "proof" is not sound.
    If you want to provide that you do know then
    you must provide all of the correct details.

    That's false. Irrelevant details should not be included. Obvious details
    shold not be included, either, except those that someone asks about.

    Merely claiming that my statement is false
    is an assertion entirely bereft of supporting
    reasoning thus inherently baseless.

    If you don't understand some point in the justification you may ask.

    Truth is computable because rCLmeaningful sentencerCY
    is defined as rCLsentence with a well-founded
    justification tree,rCY and evaluating any well-founded
    tree always terminates. Anything else isnrCOt truth-apt.

    That "bcause" is wrong. Whether a sentence has a well-founded
    justifiation tree is not computable, especially for arithmetic
    sentences.

    My one half page of text explaining all of the key details
    of my 28 years of work was completely validated by five
    different LLM systems. proof theoretic semantics is correct
    model theoretic semantics is profoundly wrong-headed.

    That "proof theoretic semantics is correct model theoretic semantics"
    may indeed be profoundly wrong-headed but there is another possibility
    that you just don't understand it.

    Your ignorance of the details of well-founded proof theoretic
    semantics makes your rebuttal baseless.

    No, that does not follow.

    But that does not alter the fact that an existence or non-existence
    of a metalanguage feature that is not present in the justification
    tree is irrelevant.

    An existence or non-existence of a metalanguage feature
    is entirely anchored in a totally wrong-headed notion.

    It does not matter where sometihing irrelevant is anchored.

    The only way that this can be seen is to become an expert
    in well-founded proof theoretic semantics.

    No reason to belive that.
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2