• Re: What formal logical systems resolve the Liar Paradox?

    From olcott@polcott333@gmail.com to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Sun Jan 18 07:45:37 2026
    From Newsgroup: comp.ai.philosophy

    On 1/18/2026 5:54 AM, Mikko wrote:
    On 16/01/2026 01:40, olcott wrote:
    On 1/15/2026 5:50 AM, Richard Damon wrote:
    On 1/15/26 12:24 AM, olcott wrote:
    On 1/14/2026 8:57 PM, Richard Damon wrote:
    On 1/13/26 1:43 PM, olcott wrote:
    On 1/13/2026 6:10 AM, Richard Damon wrote:
    On 1/12/26 11:46 PM, olcott wrote:
    On 1/12/2026 9:16 PM, Richard Damon wrote:
    On 1/12/26 4:41 PM, olcott wrote:
    How The Well-Founded Semantics for General Logic Programs

    of (Van Gelder, Ross & Schlipf, 1991)
    Journal of the Association for Computing Machinery,
    volume 38, number 3, pp. 620{650 (1991).
    https://users.soe.ucsc.edu/%7Eavg/Papers/wf.pdf

    handle the Liar Paradox when we construe
    non-well-founded / undefined as not a truth-bearer?

    % This sentence is not true.
    ?- LP = not(true(LP)).
    LP = not(true(LP)).
    ?- unify_with_occurs_check(LP, not(true(LP))).
    false.

    WFS assigns undefined to self-referential paradoxes
    without external support.

    When we interpret undefined as lack of truth-bearer
    status the Liar sentence fails to be about anything
    that can bear truth values

    The paradox dissolves - there's no contradiction
    because there's no genuine proposition

    This is actually similar to how some philosophers
    (like the "gap theorists") handle the Liar: sentences
    that fail to achieve determinate truth conditions
    simply aren't truth-bearers. WFS's undefined value
    provides a formal mechanism for identifying exactly
    these cases.

    A Subtle Point The occurs-check failure in Prolog is
    slightly different from WFS's undefined assignment -
    it's a structural constraint on term formation. But
    both point to the same insight: circular, unsupported
    self-reference doesn't create genuine semantic content.




    I thought you said that no one in the past handled the liar >>>>>>>>> paradox?


    That is no one in the past handling the Liar Paradox.
    That all happened today.

    So, today is 1991?


    The paper provides the basis for me to
    handle the Liar Paradox today. The Paper
    does not mention the Liar Paradox it
    only shows how to implement Proof Theoretic
    semantics in a logic programming system.


    I guess you are just admitting you are just a liar.


    Note, since Prolog's logic is not sufficient to handle PA,

    I never said it was. A formal system anchored in
    Proof Theoretic Semantics is powerful enough.

    Nope. It can't handle PA.


    It definitely can. I already showed you the details
    of how.

    Nope,  you PRESUME that Godel is non-sense.


    “When PA is interpreted within proof‑theoretic semantics, only
    well‑founded inferential structures are admissible as meaningful
    statements. Gödel’s diagonal construction produces an ungrounded,
    self‑referential formula whose proof‑dependency graph contains a
    cycle. Since such expressions are not truthbearers in this
    framework, the classical incompleteness phenomenon does not arise.
    PA itself remains sound and complete with respect to its grounded
    proof rules.”

    In other words, you are just admitting to be an idiot that deosn't
    care what your words actually mean.


    The term *proof‑theoretic semantics* has always
    proved my point long before I ever heard of it.

    A term does not prove anything. Only a proof proves.


    Proof Theoretic Semantics with the notion of
    non-well-founded expressions is the same thing
    that I have been saying for years.

    True and False in PA have always been x or ~x is
    provable from the actual axioms of PA, otherwise
    x is simply not a truth bearer in PA. The only
    clarification that I make now explicitly adding a
    truth predicate to PA.

    ∀x ∈ PA ((True(PA, x) ≡ (PA ⊢ x))
    ∀x ∈ PA ((False(PA, x) ≡ (PA ⊢ ~x))
    ∀x ∈ PA ((~True(PA, x) ∧ (~False(PA, x) ≡ ~TruthBearer(PA, x))
    --
    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.<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 Sun Jan 18 12:55:14 2026
    From Newsgroup: comp.ai.philosophy

    On 1/18/26 8:45 AM, olcott wrote:
    On 1/18/2026 5:54 AM, Mikko wrote:
    On 16/01/2026 01:40, olcott wrote:
    On 1/15/2026 5:50 AM, Richard Damon wrote:
    On 1/15/26 12:24 AM, olcott wrote:
    On 1/14/2026 8:57 PM, Richard Damon wrote:
    On 1/13/26 1:43 PM, olcott wrote:
    On 1/13/2026 6:10 AM, Richard Damon wrote:
    On 1/12/26 11:46 PM, olcott wrote:
    On 1/12/2026 9:16 PM, Richard Damon wrote:
    On 1/12/26 4:41 PM, olcott wrote:
    How The Well-Founded Semantics for General Logic Programs >>>>>>>>>>>
    of (Van Gelder, Ross & Schlipf, 1991)
    Journal of the Association for Computing Machinery,
    volume 38, number 3, pp. 620{650 (1991).
    https://users.soe.ucsc.edu/%7Eavg/Papers/wf.pdf

    handle the Liar Paradox when we construe
    non-well-founded / undefined as not a truth-bearer?

    % This sentence is not true.
    ?- LP = not(true(LP)).
    LP = not(true(LP)).
    ?- unify_with_occurs_check(LP, not(true(LP))).
    false.

    WFS assigns undefined to self-referential paradoxes
    without external support.

    When we interpret undefined as lack of truth-bearer
    status the Liar sentence fails to be about anything
    that can bear truth values

    The paradox dissolves - there's no contradiction
    because there's no genuine proposition

    This is actually similar to how some philosophers
    (like the "gap theorists") handle the Liar: sentences
    that fail to achieve determinate truth conditions
    simply aren't truth-bearers. WFS's undefined value
    provides a formal mechanism for identifying exactly
    these cases.

    A Subtle Point The occurs-check failure in Prolog is
    slightly different from WFS's undefined assignment -
    it's a structural constraint on term formation. But
    both point to the same insight: circular, unsupported
    self-reference doesn't create genuine semantic content.




    I thought you said that no one in the past handled the liar >>>>>>>>>> paradox?


    That is no one in the past handling the Liar Paradox.
    That all happened today.

    So, today is 1991?


    The paper provides the basis for me to
    handle the Liar Paradox today. The Paper
    does not mention the Liar Paradox it
    only shows how to implement Proof Theoretic
    semantics in a logic programming system.


    I guess you are just admitting you are just a liar.


    Note, since Prolog's logic is not sufficient to handle PA, >>>>>>>>>
    I never said it was. A formal system anchored in
    Proof Theoretic Semantics is powerful enough.

    Nope. It can't handle PA.


    It definitely can. I already showed you the details
    of how.

    Nope,  you PRESUME that Godel is non-sense.


    “When PA is interpreted within proof‑theoretic semantics, only
    well‑founded inferential structures are admissible as meaningful
    statements. Gödel’s diagonal construction produces an ungrounded, >>>>> self‑referential formula whose proof‑dependency graph contains a >>>>> cycle. Since such expressions are not truthbearers in this
    framework, the classical incompleteness phenomenon does not arise.
    PA itself remains sound and complete with respect to its grounded
    proof rules.”

    In other words, you are just admitting to be an idiot that deosn't
    care what your words actually mean.


    The term *proof‑theoretic semantics* has always
    proved my point long before I ever heard of it.

    A term does not prove anything. Only a proof proves.


    Proof Theoretic Semantics with the notion of
    non-well-founded expressions is the same thing
    that I have been saying for years.

    True and False in PA have always been x or ~x is
    provable from the actual axioms of PA, otherwise
    x is simply not a truth bearer in PA. The only
    clarification that I make now explicitly adding a
    truth predicate to PA.

    ∀x ∈ PA ((True(PA, x)  ≡ (PA ⊢ x))
    ∀x ∈ PA ((False(PA, x) ≡ (PA ⊢ ~x))
    ∀x ∈ PA ((~True(PA, x) ∧ (~False(PA, x) ≡ ~TruthBearer(PA, x))




    No, because your embodyment uses a non-well-founded criteria.

    The problem is you can't always prove "TruthBearer" or "~TruthBearer" so
    your third line is just non-well-founded, and isn't a TruthBearing
    statement for all x.

    It seems you forget that is was proven that adding a truth predicate to
    PA makes in inconsistent, and you haven't shown where Tarski was wrong.

    At best you say that a result he gets must be wrong, but can't show the
    actual error in his work.
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to sci.logic,sci.math,comp.theory,comp.ai.philosophy on Mon Jan 19 10:24:03 2026
    From Newsgroup: comp.ai.philosophy

    On 18/01/2026 15:45, olcott wrote:
    On 1/18/2026 5:54 AM, Mikko wrote:
    On 16/01/2026 01:40, olcott wrote:

    The term *proof‑theoretic semantics* has always
    proved my point long before I ever heard of it.

    A term does not prove anything. Only a proof proves.

    Note that my comment is not conradicted nor denied below:

    Proof Theoretic Semantics with the notion of
    non-well-founded expressions is the same thing
    that I have been saying for years.

    True and False in PA have always been x or ~x is
    provable from the actual axioms of PA, otherwise
    x is simply not a truth bearer in PA. The only
    clarification that I make now explicitly adding a
    truth predicate to PA.

    ∀x ∈ PA ((True(PA, x)  ≡ (PA ⊢ x))
    ∀x ∈ PA ((False(PA, x) ≡ (PA ⊢ ~x))
    ∀x ∈ PA ((~True(PA, x) ∧ (~False(PA, x) ≡ ~TruthBearer(PA, x))
    --
    Mikko
    --- Synchronet 3.21b-Linux NewsLink 1.2