On 5/1/22 8:58 PM, olcott wrote:
> On 5/1/2022 6:18 PM, Richard Damon wrote:
>> On 5/1/22 6:39 PM, olcott wrote:
>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> So which categories are you claiming are involved?
>>>>>>>>>>>>>>>> Claiming something is a 'category error' means nothing
>>>>>>>>>>>>>>>> if you don't specify the actual categories involved.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the Liar
>>>>>>>>>>>>>>> Paradox all demonstrate the exact same error. I only have
>>>>>>>>>>>>>>> considered (3) in recent years, prior to that I never
>>>>>>>>>>>>>>> heard of (3).
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> The category error would be that none of them is in the
>>>>>>>>>>>>>>> category of truth bearers. For Gödel's G and Tarski's p
>>>>>>>>>>>>>>> it would mean that the category error is that G and p are
>>>>>>>>>>>>>>> not logic sentences.
>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> And how can you possibly justify your claim that Gödel's G
>>>>>>>>>>>>>> is not a truth bearer?
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Do I have to say the same thing 500 times before you bother
>>>>>>>>>>>>> to notice that I said it once?
>>>>>>>>>>>>>
>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for
>>>>>>>>>>>>> a similar undecidability proof
>>>>>>>>>>>>>
>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>
>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>
>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>
>>>>>>>>>>>> And what does any of the above have to do with what I state
>>>>>>>>>>>> below? That's your faulty attempt at expressing The Liar in
>>>>>>>>>>>> Prolog, which has nothing to do with Gödel's G. G has *a
>>>>>>>>>>>> relationship* to The Liar, but G is *very* different from
>>>>>>>>>>>> The Liar in crucial ways.
>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>> similar
>>>>>>>>>>> undecidability proof
>>>>>>>>>>>
>>>>>>>>>>> Therfore the liar paradox can likewise be used for a similar
>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>
>>>>>>>>>>> I would not call you a nitwit except that you so persistently
>>>>>>>>>>> make sure to ignore my key points, thus probably making you a
>>>>>>>>>>> jackass rather than a nitwit.
>>>>>>>>>>
>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>
>>>>>>>>> God damned attempt to get away with the dishonest dodge of the
>>>>>>>>> strawman error.
>>>>>>>>>
>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>> similar undecidability proof
>>>>>>>>>
>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>
>>>>>>>> Do you understand the difference between 'close relationship'
>>>>>>>> and 'the same'?
>>>>>>>
>>>>>>> You freaking dishonest bastard
>>>>>>
>>>>>> The only one being dishonest here is you as you keep snipping the
>>>>>> substance of my post.
>>>>>>
>>>>>> Gödel claims there is a *close relationship* between The Liar and
>>>>>> G. He most certainly does *not* claim that they are the same.
>>>>>> (That one can construct similar proofs which bear a similar close
>>>>>> relationship to other antinomies is hardly relevant since it is
>>>>>> The Liar which is under discussion).
>>>>>>
>>>>>> There are two crucial differences between G and The Liar:
>>>>>>
>>>>>> (a) G does *not* assert its own unprovability whereas The Liar
>>>>>> *does* assert its own falsity.
>>>>>>
>>>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>>>
>>>>>> Your claim the Gödel's theorem is a 'category error' is predicated
>>>>>> on the fact that you don't grasp (b) above. I'm not going to
>>>>>> retype my explanation for this as I have already given it in a
>>>>>> previous post. You're more than welcome to go back and read that
>>>>>> post. Unless you actually have some comment on that explanation,
>>>>>> there's no point repeating yourself.
>>>>>>
>>>>>> André
>>>>>>
>>>>>
>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>> similar undecidability proof
>>>>>
>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>> lying bastard.
>>>>>
>>>>
>>>> So, there is a difference between being used for and being just like.
>>>
>>> sufficiently equivalent
>>>
>>
>> You can PROVE it?
>>
>
> I backed André into a corner and forced him to quit lying
>

So, No. Note a trimming to change meaning, the original was:

>>>>>
>>>>
>>>> 14 Every epistemological antinomy can likewise be used for a similar undecidability proof
>>>>
>>>> and the Liar Paradox is and is an epistemological antinomy you lying bastard.
>>>>
>>>
>>> So, there is a difference between being used for and being just like.
>>
>> sufficiently equivalent
>>
>
> You can PROVE it?

On 5/1/2022 8:32 PM, Richard Damon wrote:
> On 5/1/22 8:58 PM, olcott wrote:
>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>> On 5/1/22 6:39 PM, olcott wrote:
>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> So which categories are you claiming are involved?
>>>>>>>>>>>>>>>>> Claiming something is a 'category error' means nothing
>>>>>>>>>>>>>>>>> if you don't specify the actual categories involved.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the Liar
>>>>>>>>>>>>>>>> Paradox all demonstrate the exact same error. I only
>>>>>>>>>>>>>>>> have considered (3) in recent years, prior to that I
>>>>>>>>>>>>>>>> never heard of (3).
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> The category error would be that none of them is in the
>>>>>>>>>>>>>>>> category of truth bearers. For Gödel's G and Tarski's p
>>>>>>>>>>>>>>>> it would mean that the category error is that G and p
>>>>>>>>>>>>>>>> are not logic sentences.
>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> And how can you possibly justify your claim that Gödel's
>>>>>>>>>>>>>>> G is not a truth bearer?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Do I have to say the same thing 500 times before you
>>>>>>>>>>>>>> bother to notice that I said it once?
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for
>>>>>>>>>>>>>> a similar undecidability proof
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>
>>>>>>>>>>>>> And what does any of the above have to do with what I state
>>>>>>>>>>>>> below? That's your faulty attempt at expressing The Liar in
>>>>>>>>>>>>> Prolog, which has nothing to do with Gödel's G. G has *a
>>>>>>>>>>>>> relationship* to The Liar, but G is *very* different from
>>>>>>>>>>>>> The Liar in crucial ways.
>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>>> similar
>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>
>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a similar
>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>
>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>
>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>
>>>>>>>>>> God damned attempt to get away with the dishonest dodge of the
>>>>>>>>>> strawman error.
>>>>>>>>>>
>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>> similar undecidability proof
>>>>>>>>>>
>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>
>>>>>>>>> Do you understand the difference between 'close relationship'
>>>>>>>>> and 'the same'?
>>>>>>>>
>>>>>>>> You freaking dishonest bastard
>>>>>>>
>>>>>>> The only one being dishonest here is you as you keep snipping the
>>>>>>> substance of my post.
>>>>>>>
>>>>>>> Gödel claims there is a *close relationship* between The Liar and
>>>>>>> G. He most certainly does *not* claim that they are the same.
>>>>>>> (That one can construct similar proofs which bear a similar close
>>>>>>> relationship to other antinomies is hardly relevant since it is
>>>>>>> The Liar which is under discussion).
>>>>>>>
>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>
>>>>>>> (a) G does *not* assert its own unprovability whereas The Liar
>>>>>>> *does* assert its own falsity.
>>>>>>>
>>>>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>>>>
>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>> predicated on the fact that you don't grasp (b) above. I'm not
>>>>>>> going to retype my explanation for this as I have already given
>>>>>>> it in a previous post. You're more than welcome to go back and
>>>>>>> read that post. Unless you actually have some comment on that
>>>>>>> explanation, there's no point repeating yourself.
>>>>>>>
>>>>>>> André
>>>>>>>
>>>>>>
>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>> similar undecidability proof
>>>>>>
>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>> lying bastard.
>>>>>>
>>>>>
>>>>> So, there is a difference between being used for and being just like.
>>>>
>>>> sufficiently equivalent
>>>>
>>>
>>> You can PROVE it?
>>>
>>
>> I backed André into a corner and forced him to quit lying
>>
>
> So, No. Note a trimming to change meaning, the original was:
>
>>>>>>
>>>>>
>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>> similar undecidability proof
>>>>>
>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>> lying bastard.
>>>>>
>>>>
>>>> So, there is a difference between being used for and being just like.
>>>
>>> sufficiently equivalent
>>>
>>
>> You can PROVE it?
>
> So, clearly the requested proof was that about USING the epistemolgocal
> antinomy and it being just like one so not a Truth Bearer. Note, the
> comment that you claimed you backed him into isn't about that, so you
> are just proving yourself to be a deciver.
>
>
>
>
>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>  > Yes. The Liar and the Liar can be used for similar undecidability
>>  > proofs. I have no idea what it is you hope to achieve by arguing for a
>>  > truism.
>>
>
> Nice out of context quoting, showing again you are the deciver.

On 5/1/22 9:53 PM, olcott wrote:
> On 5/1/2022 8:32 PM, Richard Damon wrote:
>> On 5/1/22 8:58 PM, olcott wrote:
>>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>>> On 5/1/22 6:39 PM, olcott wrote:
>>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> So which categories are you claiming are involved?
>>>>>>>>>>>>>>>>>> Claiming something is a 'category error' means nothing
>>>>>>>>>>>>>>>>>> if you don't specify the actual categories involved.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the Liar
>>>>>>>>>>>>>>>>> Paradox all demonstrate the exact same error. I only
>>>>>>>>>>>>>>>>> have considered (3) in recent years, prior to that I
>>>>>>>>>>>>>>>>> never heard of (3).
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> The category error would be that none of them is in the
>>>>>>>>>>>>>>>>> category of truth bearers. For Gödel's G and Tarski's p
>>>>>>>>>>>>>>>>> it would mean that the category error is that G and p
>>>>>>>>>>>>>>>>> are not logic sentences.
>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> And how can you possibly justify your claim that Gödel's
>>>>>>>>>>>>>>>> G is not a truth bearer?
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Do I have to say the same thing 500 times before you
>>>>>>>>>>>>>>> bother to notice that I said it once?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>> for a similar undecidability proof
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> And what does any of the above have to do with what I
>>>>>>>>>>>>>> state below? That's your faulty attempt at expressing The
>>>>>>>>>>>>>> Liar in Prolog, which has nothing to do with Gödel's G. G
>>>>>>>>>>>>>> has *a relationship* to The Liar, but G is *very*
>>>>>>>>>>>>>> different from The Liar in crucial ways.
>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for
>>>>>>>>>>>>> a similar
>>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>>
>>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a similar
>>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>>
>>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>>
>>>>>>>>>>> God damned attempt to get away with the dishonest dodge of
>>>>>>>>>>> the strawman error.
>>>>>>>>>>>
>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>> similar undecidability proof
>>>>>>>>>>>
>>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>>
>>>>>>>>>> Do you understand the difference between 'close relationship'
>>>>>>>>>> and 'the same'?
>>>>>>>>>
>>>>>>>>> You freaking dishonest bastard
>>>>>>>>
>>>>>>>> The only one being dishonest here is you as you keep snipping
>>>>>>>> the substance of my post.
>>>>>>>>
>>>>>>>> Gödel claims there is a *close relationship* between The Liar
>>>>>>>> and G. He most certainly does *not* claim that they are the
>>>>>>>> same. (That one can construct similar proofs which bear a
>>>>>>>> similar close relationship to other antinomies is hardly
>>>>>>>> relevant since it is The Liar which is under discussion).
>>>>>>>>
>>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>>
>>>>>>>> (a) G does *not* assert its own unprovability whereas The Liar
>>>>>>>> *does* assert its own falsity.
>>>>>>>>
>>>>>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>>>>>
>>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>>> predicated on the fact that you don't grasp (b) above. I'm not
>>>>>>>> going to retype my explanation for this as I have already given
>>>>>>>> it in a previous post. You're more than welcome to go back and
>>>>>>>> read that post. Unless you actually have some comment on that
>>>>>>>> explanation, there's no point repeating yourself.
>>>>>>>>
>>>>>>>> André
>>>>>>>>
>>>>>>>
>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>> similar undecidability proof
>>>>>>>
>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>> lying bastard.
>>>>>>>
>>>>>>
>>>>>> So, there is a difference between being used for and being just like.
>>>>>
>>>>> sufficiently equivalent
>>>>>
>>>>
>>>> You can PROVE it?
>>>>
>>>
>>> I backed André into a corner and forced him to quit lying
>>>
>>
>> So, No. Note a trimming to change meaning, the original was:
>>
>>>>>>>
>>>>>>
>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>> similar undecidability proof
>>>>>>
>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>> lying bastard.
>>>>>>
>>>>>
>>>>> So, there is a difference between being used for and being just like.
>>>>
>>>> sufficiently equivalent
>>>>
>>>
>>> You can PROVE it?
>>
>> So, clearly the requested proof was that about USING the
>> epistemolgocal antinomy and it being just like one so not a Truth
>> Bearer. Note, the comment that you claimed you backed him into isn't
>> about that, so you are just proving yourself to be a deciver.
>>
>>
>>
>>
>>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>>  > Yes. The Liar and the Liar can be used for similar undecidability
>>>  > proofs. I have no idea what it is you hope to achieve by arguing
>>> for a
>>>  > truism.
>>>
>>
>> Nice out of context quoting, showing again you are the deciver.
>
> If you look at the full context of many messages you will see that he
> kept continuing to deny that the Liar Paradox can be used for similar
> undecidability proofs at least a half dozen times. Only when I made
> denying this look utterly ridiculously foolish did he finally quit lying
> about it.
>

On 5/1/2022 9:14 PM, Richard Damon wrote:
>
> On 5/1/22 9:53 PM, olcott wrote:
>> On 5/1/2022 8:32 PM, Richard Damon wrote:
>>> On 5/1/22 8:58 PM, olcott wrote:
>>>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>>>> On 5/1/22 6:39 PM, olcott wrote:
>>>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> So which categories are you claiming are involved?
>>>>>>>>>>>>>>>>>>> Claiming something is a 'category error' means
>>>>>>>>>>>>>>>>>>> nothing if you don't specify the actual categories
>>>>>>>>>>>>>>>>>>> involved.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the Liar
>>>>>>>>>>>>>>>>>> Paradox all demonstrate the exact same error. I only
>>>>>>>>>>>>>>>>>> have considered (3) in recent years, prior to that I
>>>>>>>>>>>>>>>>>> never heard of (3).
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> The category error would be that none of them is in
>>>>>>>>>>>>>>>>>> the category of truth bearers. For Gödel's G and
>>>>>>>>>>>>>>>>>> Tarski's p it would mean that the category error is
>>>>>>>>>>>>>>>>>> that G and p are not logic sentences.
>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> And how can you possibly justify your claim that
>>>>>>>>>>>>>>>>> Gödel's G is not a truth bearer?
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Do I have to say the same thing 500 times before you
>>>>>>>>>>>>>>>> bother to notice that I said it once?
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>> for a similar undecidability proof
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> And what does any of the above have to do with what I
>>>>>>>>>>>>>>> state below? That's your faulty attempt at expressing The
>>>>>>>>>>>>>>> Liar in Prolog, which has nothing to do with Gödel's G. G
>>>>>>>>>>>>>>> has *a relationship* to The Liar, but G is *very*
>>>>>>>>>>>>>>> different from The Liar in crucial ways.
>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for
>>>>>>>>>>>>>> a similar
>>>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a similar
>>>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>>>
>>>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>>>
>>>>>>>>>>>> God damned attempt to get away with the dishonest dodge of
>>>>>>>>>>>> the strawman error.
>>>>>>>>>>>>
>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>>> similar undecidability proof
>>>>>>>>>>>>
>>>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>>>
>>>>>>>>>>> Do you understand the difference between 'close relationship'
>>>>>>>>>>> and 'the same'?
>>>>>>>>>>
>>>>>>>>>> You freaking dishonest bastard
>>>>>>>>>
>>>>>>>>> The only one being dishonest here is you as you keep snipping
>>>>>>>>> the substance of my post.
>>>>>>>>>
>>>>>>>>> Gödel claims there is a *close relationship* between The Liar
>>>>>>>>> and G. He most certainly does *not* claim that they are the
>>>>>>>>> same. (That one can construct similar proofs which bear a
>>>>>>>>> similar close relationship to other antinomies is hardly
>>>>>>>>> relevant since it is The Liar which is under discussion).
>>>>>>>>>
>>>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>>>
>>>>>>>>> (a) G does *not* assert its own unprovability whereas The Liar
>>>>>>>>> *does* assert its own falsity.
>>>>>>>>>
>>>>>>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>>>>>>
>>>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>>>> predicated on the fact that you don't grasp (b) above. I'm not
>>>>>>>>> going to retype my explanation for this as I have already given
>>>>>>>>> it in a previous post. You're more than welcome to go back and
>>>>>>>>> read that post. Unless you actually have some comment on that
>>>>>>>>> explanation, there's no point repeating yourself.
>>>>>>>>>
>>>>>>>>> André
>>>>>>>>>
>>>>>>>>
>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>> similar undecidability proof
>>>>>>>>
>>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>>> lying bastard.
>>>>>>>>
>>>>>>>
>>>>>>> So, there is a difference between being used for and being just
>>>>>>> like.
>>>>>>
>>>>>> sufficiently equivalent
>>>>>>
>>>>>
>>>>> You can PROVE it?
>>>>>
>>>>
>>>> I backed André into a corner and forced him to quit lying
>>>>
>>>
>>> So, No. Note a trimming to change meaning, the original was:
>>>
>>>>>>>>
>>>>>>>
>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>> similar undecidability proof
>>>>>>>
>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>> lying bastard.
>>>>>>>
>>>>>>
>>>>>> So, there is a difference between being used for and being just like.
>>>>>
>>>>> sufficiently equivalent
>>>>>
>>>>
>>>> You can PROVE it?
>>>
>>> So, clearly the requested proof was that about USING the
>>> epistemolgocal antinomy and it being just like one so not a Truth
>>> Bearer. Note, the comment that you claimed you backed him into isn't
>>> about that, so you are just proving yourself to be a deciver.
>>>
>>>
>>>
>>>
>>>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>>>  > Yes. The Liar and the Liar can be used for similar undecidability
>>>>  > proofs. I have no idea what it is you hope to achieve by arguing
>>>> for a
>>>>  > truism.
>>>>
>>>
>>> Nice out of context quoting, showing again you are the deciver.
>>
>> If you look at the full context of many messages you will see that he
>> kept continuing to deny that the Liar Paradox can be used for similar
>> undecidability proofs at least a half dozen times. Only when I made
>> denying this look utterly ridiculously foolish did he finally quit
>> lying about it.
>>
>
> No, he says that the use of the Liar Paradox in the form that Godel does
> doesn't make the Godel Sentence a non-truth holder.
>

On 2022-05-01 20:18, olcott wrote:
> On 5/1/2022 9:14 PM, Richard Damon wrote:
>>
>> On 5/1/22 9:53 PM, olcott wrote:

>>> If you look at the full context of many messages you will see that he
>>> kept continuing to deny that the Liar Paradox can be used for similar
>>> undecidability proofs at least a half dozen times. Only when I made
>>> denying this look utterly ridiculously foolish did he finally quit
>>> lying about it.
>>>
>>
>> No, he says that the use of the Liar Paradox in the form that Godel
>> does doesn't make the Godel Sentence a non-truth holder.
>>
>
> If you look at the actual facts you will see that he continued to deny
> that kept continuing to deny that the Liar Paradox can be used for
> similar undecidability proofs at least a half dozen times.

I didn't so much deny that as I did claim it was vacuous and irrelevant.

Gödel draws a parallel between his proof and The Liar.

He also notes that other antinomies could be used to construct similar
proofs.

That would seem to mean that OTHER ANTINOMIES could be used to construct
similar proofs to the one he based on The Liar.

To say that The Liar can be used to construct similar proofs is just
plain silly since that's the one he was talking about to begin with.

More importantly, though, it is absolutely irrelevant to any of the
points I was making which didn't deny some relationship between G and
The Liar but concerned the exact *nature* of the relationship between G
and The Liar, points which would hold for proofs based on other
antinomies as well.

And points which you still have not addressed.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/1/22 10:18 PM, olcott wrote:
> On 5/1/2022 9:14 PM, Richard Damon wrote:
>>
>> On 5/1/22 9:53 PM, olcott wrote:
>>> On 5/1/2022 8:32 PM, Richard Damon wrote:
>>>> On 5/1/22 8:58 PM, olcott wrote:
>>>>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>>>>> On 5/1/22 6:39 PM, olcott wrote:
>>>>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> So which categories are you claiming are involved?
>>>>>>>>>>>>>>>>>>>> Claiming something is a 'category error' means
>>>>>>>>>>>>>>>>>>>> nothing if you don't specify the actual categories
>>>>>>>>>>>>>>>>>>>> involved.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the
>>>>>>>>>>>>>>>>>>> Liar Paradox all demonstrate the exact same error. I
>>>>>>>>>>>>>>>>>>> only have considered (3) in recent years, prior to
>>>>>>>>>>>>>>>>>>> that I never heard of (3).
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> The category error would be that none of them is in
>>>>>>>>>>>>>>>>>>> the category of truth bearers. For Gödel's G and
>>>>>>>>>>>>>>>>>>> Tarski's p it would mean that the category error is
>>>>>>>>>>>>>>>>>>> that G and p are not logic sentences.
>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> And how can you possibly justify your claim that
>>>>>>>>>>>>>>>>>> Gödel's G is not a truth bearer?
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Do I have to say the same thing 500 times before you
>>>>>>>>>>>>>>>>> bother to notice that I said it once?
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>>> for a similar undecidability proof
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> And what does any of the above have to do with what I
>>>>>>>>>>>>>>>> state below? That's your faulty attempt at expressing
>>>>>>>>>>>>>>>> The Liar in Prolog, which has nothing to do with Gödel's
>>>>>>>>>>>>>>>> G. G has *a relationship* to The Liar, but G is *very*
>>>>>>>>>>>>>>>> different from The Liar in crucial ways.
>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>> for a similar
>>>>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a similar
>>>>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>>>>
>>>>>>>>>>>>> God damned attempt to get away with the dishonest dodge of
>>>>>>>>>>>>> the strawman error.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for
>>>>>>>>>>>>> a similar undecidability proof
>>>>>>>>>>>>>
>>>>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>>>>
>>>>>>>>>>>> Do you understand the difference between 'close
>>>>>>>>>>>> relationship' and 'the same'?
>>>>>>>>>>>
>>>>>>>>>>> You freaking dishonest bastard
>>>>>>>>>>
>>>>>>>>>> The only one being dishonest here is you as you keep snipping
>>>>>>>>>> the substance of my post.
>>>>>>>>>>
>>>>>>>>>> Gödel claims there is a *close relationship* between The Liar
>>>>>>>>>> and G. He most certainly does *not* claim that they are the
>>>>>>>>>> same. (That one can construct similar proofs which bear a
>>>>>>>>>> similar close relationship to other antinomies is hardly
>>>>>>>>>> relevant since it is The Liar which is under discussion).
>>>>>>>>>>
>>>>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>>>>
>>>>>>>>>> (a) G does *not* assert its own unprovability whereas The Liar
>>>>>>>>>> *does* assert its own falsity.
>>>>>>>>>>
>>>>>>>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>>>>>>>
>>>>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>>>>> predicated on the fact that you don't grasp (b) above. I'm not
>>>>>>>>>> going to retype my explanation for this as I have already
>>>>>>>>>> given it in a previous post. You're more than welcome to go
>>>>>>>>>> back and read that post. Unless you actually have some comment
>>>>>>>>>> on that explanation, there's no point repeating yourself.
>>>>>>>>>>
>>>>>>>>>> André
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>> similar undecidability proof
>>>>>>>>>
>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>>>> lying bastard.
>>>>>>>>>
>>>>>>>>
>>>>>>>> So, there is a difference between being used for and being just
>>>>>>>> like.
>>>>>>>
>>>>>>> sufficiently equivalent
>>>>>>>
>>>>>>
>>>>>> You can PROVE it?
>>>>>>
>>>>>
>>>>> I backed André into a corner and forced him to quit lying
>>>>>
>>>>
>>>> So, No. Note a trimming to change meaning, the original was:
>>>>
>>>>>>>>>
>>>>>>>>
>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>> similar undecidability proof
>>>>>>>>
>>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>>> lying bastard.
>>>>>>>>
>>>>>>>
>>>>>>> So, there is a difference between being used for and being just
>>>>>>> like.
>>>>>>
>>>>>> sufficiently equivalent
>>>>>>
>>>>>
>>>>> You can PROVE it?
>>>>
>>>> So, clearly the requested proof was that about USING the
>>>> epistemolgocal antinomy and it being just like one so not a Truth
>>>> Bearer. Note, the comment that you claimed you backed him into isn't
>>>> about that, so you are just proving yourself to be a deciver.
>>>>
>>>>
>>>>
>>>>
>>>>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>>>>  > Yes. The Liar and the Liar can be used for similar undecidability
>>>>>  > proofs. I have no idea what it is you hope to achieve by arguing
>>>>> for a
>>>>>  > truism.
>>>>>
>>>>
>>>> Nice out of context quoting, showing again you are the deciver.
>>>
>>> If you look at the full context of many messages you will see that he
>>> kept continuing to deny that the Liar Paradox can be used for similar
>>> undecidability proofs at least a half dozen times. Only when I made
>>> denying this look utterly ridiculously foolish did he finally quit
>>> lying about it.
>>>
>>
>> No, he says that the use of the Liar Paradox in the form that Godel
>> does doesn't make the Godel Sentence a non-truth holder.
>>
>
> If you look at the actual facts you will see that he continued to deny
> that kept continuing to deny that the Liar Paradox can be used for
> similar undecidability proofs at least a half dozen times.
>
> If you make sure to knowingly contradict the verified facts then
> Revelations 21:8 may eventually apply to you.
>

On 5/1/2022 9:47 PM, Richard Damon wrote:
> On 5/1/22 10:18 PM, olcott wrote:
>> On 5/1/2022 9:14 PM, Richard Damon wrote:
>>>
>>> On 5/1/22 9:53 PM, olcott wrote:
>>>> On 5/1/2022 8:32 PM, Richard Damon wrote:
>>>>> On 5/1/22 8:58 PM, olcott wrote:
>>>>>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>>>>>> On 5/1/22 6:39 PM, olcott wrote:
>>>>>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> So which categories are you claiming are involved?
>>>>>>>>>>>>>>>>>>>>> Claiming something is a 'category error' means
>>>>>>>>>>>>>>>>>>>>> nothing if you don't specify the actual categories
>>>>>>>>>>>>>>>>>>>>> involved.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the
>>>>>>>>>>>>>>>>>>>> Liar Paradox all demonstrate the exact same error. I
>>>>>>>>>>>>>>>>>>>> only have considered (3) in recent years, prior to
>>>>>>>>>>>>>>>>>>>> that I never heard of (3).
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> The category error would be that none of them is in
>>>>>>>>>>>>>>>>>>>> the category of truth bearers. For Gödel's G and
>>>>>>>>>>>>>>>>>>>> Tarski's p it would mean that the category error is
>>>>>>>>>>>>>>>>>>>> that G and p are not logic sentences.
>>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> And how can you possibly justify your claim that
>>>>>>>>>>>>>>>>>>> Gödel's G is not a truth bearer?
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Do I have to say the same thing 500 times before you
>>>>>>>>>>>>>>>>>> bother to notice that I said it once?
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>>>> for a similar undecidability proof
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> And what does any of the above have to do with what I
>>>>>>>>>>>>>>>>> state below? That's your faulty attempt at expressing
>>>>>>>>>>>>>>>>> The Liar in Prolog, which has nothing to do with
>>>>>>>>>>>>>>>>> Gödel's G. G has *a relationship* to The Liar, but G is
>>>>>>>>>>>>>>>>> *very* different from The Liar in crucial ways.
>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>> for a similar
>>>>>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a
>>>>>>>>>>>>>>>> similar
>>>>>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> God damned attempt to get away with the dishonest dodge of
>>>>>>>>>>>>>> the strawman error.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for
>>>>>>>>>>>>>> a similar undecidability proof
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>>>>>
>>>>>>>>>>>>> Do you understand the difference between 'close
>>>>>>>>>>>>> relationship' and 'the same'?
>>>>>>>>>>>>
>>>>>>>>>>>> You freaking dishonest bastard
>>>>>>>>>>>
>>>>>>>>>>> The only one being dishonest here is you as you keep snipping
>>>>>>>>>>> the substance of my post.
>>>>>>>>>>>
>>>>>>>>>>> Gödel claims there is a *close relationship* between The Liar
>>>>>>>>>>> and G. He most certainly does *not* claim that they are the
>>>>>>>>>>> same. (That one can construct similar proofs which bear a
>>>>>>>>>>> similar close relationship to other antinomies is hardly
>>>>>>>>>>> relevant since it is The Liar which is under discussion).
>>>>>>>>>>>
>>>>>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>>>>>
>>>>>>>>>>> (a) G does *not* assert its own unprovability whereas The
>>>>>>>>>>> Liar *does* assert its own falsity.
>>>>>>>>>>>
>>>>>>>>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>>>>>>>>
>>>>>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>>>>>> predicated on the fact that you don't grasp (b) above. I'm
>>>>>>>>>>> not going to retype my explanation for this as I have already
>>>>>>>>>>> given it in a previous post. You're more than welcome to go
>>>>>>>>>>> back and read that post. Unless you actually have some
>>>>>>>>>>> comment on that explanation, there's no point repeating
>>>>>>>>>>> yourself.
>>>>>>>>>>>
>>>>>>>>>>> André
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>> similar undecidability proof
>>>>>>>>>>
>>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>>>>> lying bastard.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> So, there is a difference between being used for and being just
>>>>>>>>> like.
>>>>>>>>
>>>>>>>> sufficiently equivalent
>>>>>>>>
>>>>>>>
>>>>>>> You can PROVE it?
>>>>>>>
>>>>>>
>>>>>> I backed André into a corner and forced him to quit lying
>>>>>>
>>>>>
>>>>> So, No. Note a trimming to change meaning, the original was:
>>>>>
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>> similar undecidability proof
>>>>>>>>>
>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>>>> lying bastard.
>>>>>>>>>
>>>>>>>>
>>>>>>>> So, there is a difference between being used for and being just
>>>>>>>> like.
>>>>>>>
>>>>>>> sufficiently equivalent
>>>>>>>
>>>>>>
>>>>>> You can PROVE it?
>>>>>
>>>>> So, clearly the requested proof was that about USING the
>>>>> epistemolgocal antinomy and it being just like one so not a Truth
>>>>> Bearer. Note, the comment that you claimed you backed him into
>>>>> isn't about that, so you are just proving yourself to be a deciver.
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>>>>>  > Yes. The Liar and the Liar can be used for similar undecidability
>>>>>>  > proofs. I have no idea what it is you hope to achieve by
>>>>>> arguing for a
>>>>>>  > truism.
>>>>>>
>>>>>
>>>>> Nice out of context quoting, showing again you are the deciver.
>>>>
>>>> If you look at the full context of many messages you will see that
>>>> he kept continuing to deny that the Liar Paradox can be used for
>>>> similar undecidability proofs at least a half dozen times. Only when
>>>> I made denying this look utterly ridiculously foolish did he finally
>>>> quit lying about it.
>>>>
>>>
>>> No, he says that the use of the Liar Paradox in the form that Godel
>>> does doesn't make the Godel Sentence a non-truth holder.
>>>
>>
>> If you look at the actual facts you will see that he continued to deny
>> that kept continuing to deny that the Liar Paradox can be used for
>> similar undecidability proofs at least a half dozen times.
>>
>> If you make sure to knowingly contradict the verified facts then
>> Revelations 21:8 may eventually apply to you.
>>
>
> You mean like when he said (and you snipped):
>
>>
>> The only one being dishonest here is you as you keep snipping the
>> substance of my post.
>>
>> Gödel claims there is a *close relationship* between The Liar and G.
>> He most certainly does *not* claim that they are the same. (That one
>> can construct similar proofs which bear a similar close relationship
>> to other antinomies is hardly relevant since it is The Liar which is
>> under discussion).
>>
>> There are two crucial differences between G and The Liar:
>>
>> (a) G does *not* assert its own unprovability whereas The Liar *does*
>> assert its own falsity.
>>
>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>
>> Your claim the Gödel's theorem is a 'category error' is predicated on
>> the fact that you don't grasp (b) above. I'm not going to retype my
>> explanation for this as I have already given it in a previous post.
>> You're more than welcome to go back and read that post. Unless you
>> actually have some comment on that explanation, there's no point
>> repeating yourself.
>>
>
> Maybe you should check your OWN facts.
>

On 2022-05-01 21:04, olcott wrote:

> He is focusing on the dishonest dodge of the strawman error by making
> sure to ignore that in another quote Gödel said that Gödel's G is
> sufficiently equivalent to the Liar Paradox on the basis that the Liar
> Paradox is an epistemological antinomy, whereas the quote he keeps
> switching back to is less clear on this point.

There is no quote where Gödel claims G is "sufficiently equivalent" to
the Liars Paradox. (And "sufficiently equivalent" for what, exactly? Is
a five dollar bill "sufficiently equivalent" to 20 quarters? It's a
meaningless question without specifying what type of equivalence you
have in mind -- equivalent value, sure. Equivalent usefulness in a
vending maching, not necessarily)

> Since I focused on correcting his mistake several times it finally got
> down to the point where it was clear that he was a lying bastard.

Since you seem to be claiming that I reject some nonexistent quote, I
can't imagine what mistake I might have made.

> I am utterly immune to gas lighting.
>
>> He is CLEARLY not saying that the Liar Paradox can't be used for this
>> sort of proof, because he talks about its form being used.
>>
>
> He continued to refer to the other quote of Gödel that is much more
> vague on the equivalence between Gödel's G as his basis that equivalence
> cannot be be determined even when I kept focusing him back on the quote
> that does assert sufficient equivalence exists. I did this six times.

What is this quote you are referring to where he asserts "sufficient
equivalence"? Unless I missed something, the quote you kept harping on
was "Every epistemological antinomy can likewise be used for a similar
undecidability proof". That makes no mention whatsoever of "equivalence"
(sufficient or otherwise) between The Liar and G.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/1/22 11:04 PM, olcott wrote:
> On 5/1/2022 9:47 PM, Richard Damon wrote:
>> On 5/1/22 10:18 PM, olcott wrote:
>>> On 5/1/2022 9:14 PM, Richard Damon wrote:
>>>>
>>>> On 5/1/22 9:53 PM, olcott wrote:
>>>>> On 5/1/2022 8:32 PM, Richard Damon wrote:
>>>>>> On 5/1/22 8:58 PM, olcott wrote:
>>>>>>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>>>>>>> On 5/1/22 6:39 PM, olcott wrote:
>>>>>>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>>>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> So which categories are you claiming are involved?
>>>>>>>>>>>>>>>>>>>>>> Claiming something is a 'category error' means
>>>>>>>>>>>>>>>>>>>>>> nothing if you don't specify the actual categories
>>>>>>>>>>>>>>>>>>>>>> involved.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the
>>>>>>>>>>>>>>>>>>>>> Liar Paradox all demonstrate the exact same error.
>>>>>>>>>>>>>>>>>>>>> I only have considered (3) in recent years, prior
>>>>>>>>>>>>>>>>>>>>> to that I never heard of (3).
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> The category error would be that none of them is in
>>>>>>>>>>>>>>>>>>>>> the category of truth bearers. For Gödel's G and
>>>>>>>>>>>>>>>>>>>>> Tarski's p it would mean that the category error is
>>>>>>>>>>>>>>>>>>>>> that G and p are not logic sentences.
>>>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> And how can you possibly justify your claim that
>>>>>>>>>>>>>>>>>>>> Gödel's G is not a truth bearer?
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Do I have to say the same thing 500 times before you
>>>>>>>>>>>>>>>>>>> bother to notice that I said it once?
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be
>>>>>>>>>>>>>>>>>>> used for a similar undecidability proof
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> And what does any of the above have to do with what I
>>>>>>>>>>>>>>>>>> state below? That's your faulty attempt at expressing
>>>>>>>>>>>>>>>>>> The Liar in Prolog, which has nothing to do with
>>>>>>>>>>>>>>>>>> Gödel's G. G has *a relationship* to The Liar, but G
>>>>>>>>>>>>>>>>>> is *very* different from The Liar in crucial ways.
>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>>> for a similar
>>>>>>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a
>>>>>>>>>>>>>>>>> similar
>>>>>>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> God damned attempt to get away with the dishonest dodge
>>>>>>>>>>>>>>> of the strawman error.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>> for a similar undecidability proof
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Do you understand the difference between 'close
>>>>>>>>>>>>>> relationship' and 'the same'?
>>>>>>>>>>>>>
>>>>>>>>>>>>> You freaking dishonest bastard
>>>>>>>>>>>>
>>>>>>>>>>>> The only one being dishonest here is you as you keep
>>>>>>>>>>>> snipping the substance of my post.
>>>>>>>>>>>>
>>>>>>>>>>>> Gödel claims there is a *close relationship* between The
>>>>>>>>>>>> Liar and G. He most certainly does *not* claim that they are
>>>>>>>>>>>> the same. (That one can construct similar proofs which bear
>>>>>>>>>>>> a similar close relationship to other antinomies is hardly
>>>>>>>>>>>> relevant since it is The Liar which is under discussion).
>>>>>>>>>>>>
>>>>>>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>>>>>>
>>>>>>>>>>>> (a) G does *not* assert its own unprovability whereas The
>>>>>>>>>>>> Liar *does* assert its own falsity.
>>>>>>>>>>>>
>>>>>>>>>>>> (b) G is most definitely a truth-bearer even if The Liar is
>>>>>>>>>>>> not.
>>>>>>>>>>>>
>>>>>>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>>>>>>> predicated on the fact that you don't grasp (b) above. I'm
>>>>>>>>>>>> not going to retype my explanation for this as I have
>>>>>>>>>>>> already given it in a previous post. You're more than
>>>>>>>>>>>> welcome to go back and read that post. Unless you actually
>>>>>>>>>>>> have some comment on that explanation, there's no point
>>>>>>>>>>>> repeating yourself.
>>>>>>>>>>>>
>>>>>>>>>>>> André
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>> similar undecidability proof
>>>>>>>>>>>
>>>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy
>>>>>>>>>>> you lying bastard.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> So, there is a difference between being used for and being
>>>>>>>>>> just like.
>>>>>>>>>
>>>>>>>>> sufficiently equivalent
>>>>>>>>>
>>>>>>>>
>>>>>>>> You can PROVE it?
>>>>>>>>
>>>>>>>
>>>>>>> I backed André into a corner and forced him to quit lying
>>>>>>>
>>>>>>
>>>>>> So, No. Note a trimming to change meaning, the original was:
>>>>>>
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>> similar undecidability proof
>>>>>>>>>>
>>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy you
>>>>>>>>>> lying bastard.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> So, there is a difference between being used for and being just
>>>>>>>>> like.
>>>>>>>>
>>>>>>>> sufficiently equivalent
>>>>>>>>
>>>>>>>
>>>>>>> You can PROVE it?
>>>>>>
>>>>>> So, clearly the requested proof was that about USING the
>>>>>> epistemolgocal antinomy and it being just like one so not a Truth
>>>>>> Bearer. Note, the comment that you claimed you backed him into
>>>>>> isn't about that, so you are just proving yourself to be a deciver.
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>>>>>>  > Yes. The Liar and the Liar can be used for similar undecidability
>>>>>>>  > proofs. I have no idea what it is you hope to achieve by
>>>>>>> arguing for a
>>>>>>>  > truism.
>>>>>>>
>>>>>>
>>>>>> Nice out of context quoting, showing again you are the deciver.
>>>>>
>>>>> If you look at the full context of many messages you will see that
>>>>> he kept continuing to deny that the Liar Paradox can be used for
>>>>> similar undecidability proofs at least a half dozen times. Only
>>>>> when I made denying this look utterly ridiculously foolish did he
>>>>> finally quit lying about it.
>>>>>
>>>>
>>>> No, he says that the use of the Liar Paradox in the form that Godel
>>>> does doesn't make the Godel Sentence a non-truth holder.
>>>>
>>>
>>> If you look at the actual facts you will see that he continued to
>>> deny that kept continuing to deny that the Liar Paradox can be used
>>> for similar undecidability proofs at least a half dozen times.
>>>
>>> If you make sure to knowingly contradict the verified facts then
>>> Revelations 21:8 may eventually apply to you.
>>>
>>
>> You mean like when he said (and you snipped):
>>
>>>
>>> The only one being dishonest here is you as you keep snipping the
>>> substance of my post.
>>>
>>> Gödel claims there is a *close relationship* between The Liar and G.
>>> He most certainly does *not* claim that they are the same. (That one
>>> can construct similar proofs which bear a similar close relationship
>>> to other antinomies is hardly relevant since it is The Liar which is
>>> under discussion).
>>>
>>> There are two crucial differences between G and The Liar:
>>>
>>> (a) G does *not* assert its own unprovability whereas The Liar *does*
>>> assert its own falsity.
>>>
>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>
>>> Your claim the Gödel's theorem is a 'category error' is predicated on
>>> the fact that you don't grasp (b) above. I'm not going to retype my
>>> explanation for this as I have already given it in a previous post.
>>> You're more than welcome to go back and read that post. Unless you
>>> actually have some comment on that explanation, there's no point
>>> repeating yourself.
>>>
>>
>> Maybe you should check your OWN facts.
>>
>
> He is focusing on the dishonest dodge of the strawman error by making
> sure to ignore that in another quote Gödel said that Gödel's G is
> sufficiently equivalent to the Liar Paradox on the basis that the Liar
> Paradox is an epistemological antinomy, whereas the quote he keeps
> switching back to is less clear on this point.
>
> Since I focused on correcting his mistake several times it finally got
> down to the point where it was clear that he was a lying bastard.
>
> I am utterly immune to gas lighting.
>
>> He is CLEARLY not saying that the Liar Paradox can't be used for this
>> sort of proof, because he talks about its form being used.
>>
>
> He continued to refer to the other quote of Gödel that is much more
> vague on the equivalence between Gödel's G as his basis that equivalence
> cannot be be determined even when I kept focusing him back on the quote
> that does assert sufficient equivalence exists. I did this six times.
>
> At this point my assessment that he was a lying bastard was sufficiently
> validated.
>
> Are you a lying bastard too, or will you acknowledge that my assessment
> is correct?
>

Wow, I went offline for a weekend, because we had such a nice weather,
and this thread exploded to enormous size 😲. I didn't read the whole
thread it's just too big.

On 5/1/22 13:00, olcott wrote:
> On 5/1/2022 4:26 AM, Mikko wrote:
>> On 2022-04-30 21:08:05 +0000, olcott said:
>>
>>> negation, not, \+
>>> The concept of logical negation in Prolog is problematical, in the
>>> sense that the only method that Prolog can use to tell if a
>>> proposition is false is to try to prove it (from the facts and rules
>>> that it has been told about), and then if this attempt fails, it
>>> concludes that the proposition is false. This is referred to as
>>> negation as failure.
>>
>> Note that the negation discussed above is not present in LP =
>> not(true(LP)).
>>
>> Mikko
>>
>
> Is says that it is. It says that "not" is synonymous with \+.

I don't want to undermine your knowledge in formal logic, but still
allow me to re-iterate my point, because it looks like it didn't come
through.

1. Prolog is *not* an automated theorem prover; it is a programming
language. Nevertheless you can /implement/ one in Prolog.
2. Prolog's syntax is somewhat original and requires some
understanding.

Let me elaborate on the 2nd point. Prolog is a homoiconic language that
means that same syntactical constructs (terms) can express data, or be
executable.

Consider this knowledge base¹:

foo :- not(true).

The following query will fail:

?- foo.
false.

When we asked the program to refute `foo/0` it *executed* predicates
`not/1` and `true/0`.

But, given this knowledge base:

bar(X) :- X = not(true).

The following query does succeed:

?- bar(X).
X = not(true).

Why? — Here, both `not/1` and `true/0` were *not* executed, they were
used as a mere symbols, data without *any* meaning whatsoever. Also
please note that this has nothing to do with cyclic terms, they are
completely separate things, and the problem with your Prolog code
doesn't lie in cyclic term handling, but in basic misconception when
terms are executed and when they aren't. In your example:

> LP := ~True(LP) is translated to Prolog:
>
> ?- LP = not(true(LP)).
> LP = not(true(LP)).
>
> ?- unify_with_occurs_check(LP, not(true(LP))).
> false
None (!) of the predicates where executed in both unifications (with and
without occurs check).

Basically what I was trying to say is that `LP = not(true(LP))` is
incorrect encoding of the stated logical formula. What you have written
just tells to Prolog to unify variable `LP` with the term
`not(true(LP))`, it is similar to this query (`not` is used only as an
atom it isn't executed):

?- X = [not|X].
X = [not|X].

?- unify_with_occurs_check(X, [not|X]).
false.

I've skimmed through your paper and you encode logical formula G = ¬(F ⊢
G) as:

G = not(provable(F, G)).

Which is not correct for all the reasons I've laid down previously, at
least it is not correct with the default semantics of `=` operator.

I hope this will clear some thing out.

[¹] As a side note, according to the SWI-Prolog documentation `not/1`
predicate is deprecated and should be replaced with `'\+'/1`.
https://www.swi-prolog.org/pldoc/doc_for?object=not/1

--
Alex Grabowski

On 5/2/2022 6:49 AM, Aleksy Grabowski wrote:
> Wow, I went offline for a weekend, because we had such a nice weather,
> and this thread exploded to enormous size 😲. I didn't read the whole
> thread it's just too big.
>
> On 5/1/22 13:00, olcott wrote:
>> On 5/1/2022 4:26 AM, Mikko wrote:
>>> On 2022-04-30 21:08:05 +0000, olcott said:
>>>
>>>> negation, not, \+
>>>> The concept of logical negation in Prolog is problematical, in the
>>>> sense that the only method that Prolog can use to tell if a
>>>> proposition is false is to try to prove it (from the facts and rules
>>>> that it has been told about), and then if this attempt fails, it
>>>> concludes that the proposition is false. This is referred to as
>>>> negation as failure.
>>>
>>> Note that the negation discussed above is not present in LP =
>>> not(true(LP)).
>>>
>>> Mikko
>>>
>>
>> Is says that it is. It says that "not" is synonymous with \+.
>
> I don't want to undermine your knowledge in formal logic, but still
> allow me to re-iterate my point, because it looks like it didn't come
> through.
>
>  1. Prolog is *not* an automated theorem prover; it is a programming
>     language. Nevertheless you can /implement/ one in Prolog.
>  2. Prolog's syntax is somewhat original and requires some
>     understanding.
>
> Let me elaborate on the 2nd point. Prolog is a homoiconic language that
> means that same syntactical constructs (terms) can express data, or be
> executable.
>
> Consider this knowledge base¹:
>
>     foo :- not(true).
>
> The following query will fail:
>
>     ?- foo.
>     false.
>
> When we asked the program to refute `foo/0` it *executed* predicates
> `not/1` and `true/0`.
>
> But, given this knowledge base:
>
>     bar(X) :- X = not(true).
>
> The following query does succeed:
>
>     ?- bar(X).
>     X = not(true).
>
> Why? — Here, both `not/1` and `true/0` were *not* executed, they were
> used as a mere symbols, data without *any* meaning whatsoever. Also
> please note that this has nothing to do with cyclic terms, they are
> completely separate things, and the problem with your Prolog code
> doesn't lie in cyclic term handling, but in basic misconception when
> terms are executed and when they aren't. In your example:
>
>> LP := ~True(LP) is translated to Prolog:
>>
>> ?- LP = not(true(LP)).
>> LP = not(true(LP)).
>>
>> ?- unify_with_occurs_check(LP, not(true(LP))).
>> false
> None (!) of the predicates where executed in both unifications (with and
> without occurs check).
>
> Basically what I was trying to say is that `LP = not(true(LP))` is
> incorrect encoding of the stated logical formula. What you have written
> just tells to Prolog to unify variable `LP` with the term
> `not(true(LP))`, it is similar to this query (`not` is used only as an
> atom it isn't executed):
>
>     ?- X = [not|X].
>     X = [not|X].
>
>     ?- unify_with_occurs_check(X, [not|X]).
>     false.
>
> I've skimmed through your paper and you encode logical formula G = ¬(F ⊢
> G) as:
>
>    G = not(provable(F, G)).
>
> Which is not correct for all the reasons I've laid down previously, at
> least it is not correct with the default semantics of `=` operator.
>
> I hope this will clear some thing out.
>
>  [¹] As a side note, according to the SWI-Prolog documentation `not/1`
>      predicate is deprecated and should be replaced with `'\+'/1`.
>      https://www.swi-prolog.org/pldoc/doc_for?object=not/1
>

Here is what I understand of the relationship between logic and Prolog.
Prolog corrects all of the errors of classical and symbolic logic by
forming the underlying framework for the correct notion of truth and
provability. In all of the places where logic diverges from the Prolog
model logic fails to be correct.

Correct logic derives conclusions on the basis of applying truth
preserving operations to expressions of language known to be true. This
simple model refutes the Tarski undefinability theorem.

Tarski Undefinability Proof.
https://liarparadox.org/Tarski_275_276.pdf

If a set of rules (truth preserving operations) can be applied to a set
of facts (expressions of language known to be true) then the result is
the truth of the Prolog expression. This is the way that Truth really
works and both classical and Symbolic logic go astray of this.
https://en.wikipedia.org/wiki/Prolog#Rules_and_facts

It is also Good that Prolog as negation as failure because this detects
logic errors that are hidden from classical and symbolic logic. Logic
always assume that every expression of language that is not true must be
false. This makes semantic errors invisible to classical and symbolic
logic visible to Prolong.

This sentence is neither provable nor refutable in Prolog:
This sentence is not true. This is one of my best attempts at
formalizing that: LP ↔ ~True(LP)

The whole purpose of this thread is to find out exactly how to encode:
"This sentence is not true" in Prolog when we assume that True is
exactly the same thing as Provable in Prolog.

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/2022 6:10 AM, Richard Damon wrote:
> On 5/1/22 11:04 PM, olcott wrote:
>> On 5/1/2022 9:47 PM, Richard Damon wrote:
>>> On 5/1/22 10:18 PM, olcott wrote:
>>>> On 5/1/2022 9:14 PM, Richard Damon wrote:
>>>>>
>>>>> On 5/1/22 9:53 PM, olcott wrote:
>>>>>> On 5/1/2022 8:32 PM, Richard Damon wrote:
>>>>>>> On 5/1/22 8:58 PM, olcott wrote:
>>>>>>>> On 5/1/2022 6:18 PM, Richard Damon wrote:
>>>>>>>>> On 5/1/22 6:39 PM, olcott wrote:
>>>>>>>>>> On 5/1/2022 5:08 PM, Richard Damon wrote:
>>>>>>>>>>> On 5/1/22 6:04 PM, olcott wrote:
>>>>>>>>>>>> On 5/1/2022 3:51 PM, André G. Isaak wrote:
>>>>>>>>>>>>> On 2022-05-01 14:42, olcott wrote:
>>>>>>>>>>>>>> On 5/1/2022 3:37 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>> On 2022-05-01 14:03, olcott wrote:
>>>>>>>>>>>>>>>> On 5/1/2022 2:54 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>> On 2022-05-01 13:48, olcott wrote:
>>>>>>>>>>>>>>>>>> On 5/1/2022 2:44 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:32, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 5/1/2022 2:22 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>>> On 2022-05-01 13:00, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>> On 5/1/2022 1:33 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> So which categories are you claiming are
>>>>>>>>>>>>>>>>>>>>>>> involved? Claiming something is a 'category
>>>>>>>>>>>>>>>>>>>>>>> error' means nothing if you don't specify the
>>>>>>>>>>>>>>>>>>>>>>> actual categories involved.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> My original thinking was that (1) and (2) and the
>>>>>>>>>>>>>>>>>>>>>> Liar Paradox all demonstrate the exact same error.
>>>>>>>>>>>>>>>>>>>>>> I only have considered (3) in recent years, prior
>>>>>>>>>>>>>>>>>>>>>> to that I never heard of (3).
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> The category error would be that none of them is
>>>>>>>>>>>>>>>>>>>>>> in the category of truth bearers. For Gödel's G
>>>>>>>>>>>>>>>>>>>>>> and Tarski's p it would mean that the category
>>>>>>>>>>>>>>>>>>>>>> error is that G and p are not logic sentences.
>>>>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> And how can you possibly justify your claim that
>>>>>>>>>>>>>>>>>>>>> Gödel's G is not a truth bearer?
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Do I have to say the same thing 500 times before you
>>>>>>>>>>>>>>>>>>>> bother to notice that I said it once?
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be
>>>>>>>>>>>>>>>>>>>> used for a similar undecidability proof
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Therefore LP ↔ ~True(LP) can be used for a similar
>>>>>>>>>>>>>>>>>>>> undecidability proof, and LP ↔ ~True(LP) is clearly
>>>>>>>>>>>>>>>>>>>> semantically ill-formed.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>>>>>>>>>>>>>> LP = not(true(LP)).
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>> false. // false means semantically ill-formed.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> And what does any of the above have to do with what I
>>>>>>>>>>>>>>>>>>> state below? That's your faulty attempt at expressing
>>>>>>>>>>>>>>>>>>> The Liar in Prolog, which has nothing to do with
>>>>>>>>>>>>>>>>>>> Gödel's G. G has *a relationship* to The Liar, but G
>>>>>>>>>>>>>>>>>>> is *very* different from The Liar in crucial ways.
>>>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>>>> for a similar
>>>>>>>>>>>>>>>>>> undecidability proof
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Therfore the liar paradox can likewise be used for a
>>>>>>>>>>>>>>>>>> similar
>>>>>>>>>>>>>>>>>> undecidability proof, nitwit.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> I would not call you a nitwit except that you so
>>>>>>>>>>>>>>>>>> persistently make sure to ignore my key points, thus
>>>>>>>>>>>>>>>>>> probably making you a jackass rather than a nitwit.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> And again, you snipped all of the
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> God damned attempt to get away with the dishonest dodge
>>>>>>>>>>>>>>>> of the strawman error.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used
>>>>>>>>>>>>>>>> for a similar undecidability proof
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Do you not know what the word "every" means?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Do you understand the difference between 'close
>>>>>>>>>>>>>>> relationship' and 'the same'?
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> You freaking dishonest bastard
>>>>>>>>>>>>>
>>>>>>>>>>>>> The only one being dishonest here is you as you keep
>>>>>>>>>>>>> snipping the substance of my post.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Gödel claims there is a *close relationship* between The
>>>>>>>>>>>>> Liar and G. He most certainly does *not* claim that they
>>>>>>>>>>>>> are the same. (That one can construct similar proofs which
>>>>>>>>>>>>> bear a similar close relationship to other antinomies is
>>>>>>>>>>>>> hardly relevant since it is The Liar which is under
>>>>>>>>>>>>> discussion).
>>>>>>>>>>>>>
>>>>>>>>>>>>> There are two crucial differences between G and The Liar:
>>>>>>>>>>>>>
>>>>>>>>>>>>> (a) G does *not* assert its own unprovability whereas The
>>>>>>>>>>>>> Liar *does* assert its own falsity.
>>>>>>>>>>>>>
>>>>>>>>>>>>> (b) G is most definitely a truth-bearer even if The Liar is
>>>>>>>>>>>>> not.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Your claim the Gödel's theorem is a 'category error' is
>>>>>>>>>>>>> predicated on the fact that you don't grasp (b) above. I'm
>>>>>>>>>>>>> not going to retype my explanation for this as I have
>>>>>>>>>>>>> already given it in a previous post. You're more than
>>>>>>>>>>>>> welcome to go back and read that post. Unless you actually
>>>>>>>>>>>>> have some comment on that explanation, there's no point
>>>>>>>>>>>>> repeating yourself.
>>>>>>>>>>>>>
>>>>>>>>>>>>> André
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>>> similar undecidability proof
>>>>>>>>>>>>
>>>>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy
>>>>>>>>>>>> you lying bastard.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> So, there is a difference between being used for and being
>>>>>>>>>>> just like.
>>>>>>>>>>
>>>>>>>>>> sufficiently equivalent
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> You can PROVE it?
>>>>>>>>>
>>>>>>>>
>>>>>>>> I backed André into a corner and forced him to quit lying
>>>>>>>>
>>>>>>>
>>>>>>> So, No. Note a trimming to change meaning, the original was:
>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> 14 Every epistemological antinomy can likewise be used for a
>>>>>>>>>>> similar undecidability proof
>>>>>>>>>>>
>>>>>>>>>>> and the Liar Paradox is and is an epistemological antinomy
>>>>>>>>>>> you lying bastard.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> So, there is a difference between being used for and being
>>>>>>>>>> just like.
>>>>>>>>>
>>>>>>>>> sufficiently equivalent
>>>>>>>>>
>>>>>>>>
>>>>>>>> You can PROVE it?
>>>>>>>
>>>>>>> So, clearly the requested proof was that about USING the
>>>>>>> epistemolgocal antinomy and it being just like one so not a Truth
>>>>>>> Bearer. Note, the comment that you claimed you backed him into
>>>>>>> isn't about that, so you are just proving yourself to be a deciver.
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> On 5/1/2022 6:44 PM, André G. Isaak wrote:
>>>>>>>>  > Yes. The Liar and the Liar can be used for similar
>>>>>>>> undecidability
>>>>>>>>  > proofs. I have no idea what it is you hope to achieve by
>>>>>>>> arguing for a
>>>>>>>>  > truism.
>>>>>>>>
>>>>>>>
>>>>>>> Nice out of context quoting, showing again you are the deciver.
>>>>>>
>>>>>> If you look at the full context of many messages you will see that
>>>>>> he kept continuing to deny that the Liar Paradox can be used for
>>>>>> similar undecidability proofs at least a half dozen times. Only
>>>>>> when I made denying this look utterly ridiculously foolish did he
>>>>>> finally quit lying about it.
>>>>>>
>>>>>
>>>>> No, he says that the use of the Liar Paradox in the form that Godel
>>>>> does doesn't make the Godel Sentence a non-truth holder.
>>>>>
>>>>
>>>> If you look at the actual facts you will see that he continued to
>>>> deny that kept continuing to deny that the Liar Paradox can be used
>>>> for similar undecidability proofs at least a half dozen times.
>>>>
>>>> If you make sure to knowingly contradict the verified facts then
>>>> Revelations 21:8 may eventually apply to you.
>>>>
>>>
>>> You mean like when he said (and you snipped):
>>>
>>>>
>>>> The only one being dishonest here is you as you keep snipping the
>>>> substance of my post.
>>>>
>>>> Gödel claims there is a *close relationship* between The Liar and G.
>>>> He most certainly does *not* claim that they are the same. (That one
>>>> can construct similar proofs which bear a similar close relationship
>>>> to other antinomies is hardly relevant since it is The Liar which is
>>>> under discussion).
>>>>
>>>> There are two crucial differences between G and The Liar:
>>>>
>>>> (a) G does *not* assert its own unprovability whereas The Liar
>>>> *does* assert its own falsity.
>>>>
>>>> (b) G is most definitely a truth-bearer even if The Liar is not.
>>>>
>>>> Your claim the Gödel's theorem is a 'category error' is predicated
>>>> on the fact that you don't grasp (b) above. I'm not going to retype
>>>> my explanation for this as I have already given it in a previous
>>>> post. You're more than welcome to go back and read that post. Unless
>>>> you actually have some comment on that explanation, there's no point
>>>> repeating yourself.
>>>>
>>>
>>> Maybe you should check your OWN facts.
>>>
>>
>> He is focusing on the dishonest dodge of the strawman error by making
>> sure to ignore that in another quote Gödel said that Gödel's G is
>> sufficiently equivalent to the Liar Paradox on the basis that the Liar
>> Paradox is an epistemological antinomy, whereas the quote he keeps
>> switching back to is less clear on this point.
>>
>> Since I focused on correcting his mistake several times it finally got
>> down to the point where it was clear that he was a lying bastard.
>>
>> I am utterly immune to gas lighting.
>>
>>> He is CLEARLY not saying that the Liar Paradox can't be used for this
>>> sort of proof, because he talks about its form being used.
>>>
>>
>> He continued to refer to the other quote of Gödel that is much more
>> vague on the equivalence between Gödel's G as his basis that
>> equivalence cannot be be determined even when I kept focusing him back
>> on the quote that does assert sufficient equivalence exists. I did
>> this six times.
>>
>> At this point my assessment that he was a lying bastard was
>> sufficiently validated.
>>
>> Are you a lying bastard too, or will you acknowledge that my
>> assessment is correct?
>>
>
> I will acknowledge that you have proven yourself to be the lying bastard.
>
> YOU have REPEADTEDLY trimmed out important parts of the conversation
> either to INTENTIONALLY be deceptive, or because you are so incompetent
> at this material that you don't know what is important.
>

> The whole purpose of this thread is to find out exactly how to encode:
> "This sentence is not true" in Prolog when we assume that True is
> exactly the same thing as Provable in Prolog.

"This sentence is not provable" can be naïvely encoded:

g :- \+ g.

Then you can ask Prolog if this sentence is true:

?- g.

Prolog will give you the only correct answer — no answer 🙃.

> Here is what I understand of the relationship between logic and Prolog.
> Prolog corrects all of the errors of classical and symbolic logic by
> forming the underlying framework for the correct notion of truth and
> provability. In all of the places where logic diverges from the Prolog
> model logic fails to be correc
Prolog by itself is a very bad theorem prover and it is very limited
framework for formal logic, because it implements only Horn clauses.
However it is a very good programming language and you can implement any
theorem prover in it, like you can implement any theorem prover in C++
or Java.

--
Alex Grabowski

On 5/2/2022 8:35 AM, Aleksy Grabowski wrote:
>> The whole purpose of this thread is to find out exactly how to encode:
>> "This sentence is not true" in Prolog when we assume that True is
>> exactly the same thing as Provable in Prolog.
>
> "This sentence is not provable" can be naïvely encoded:
>
> g :- \+ g.
>
> Then you can ask Prolog if this sentence is true:
>
> ?- g.
>
> Prolog will give you the only correct answer — no answer 🙃.

That is great, now what happens when we encode:
"This sentence is provable" in Prolog?

What happens when we test both of these with
unify_with_occurs_check ?

>
>> Here is what I understand of the relationship between logic and Prolog.
>> Prolog corrects all of the errors of classical and symbolic logic by
>> forming the underlying framework for the correct notion of truth and
>> provability. In all of the places where logic diverges from the Prolog
>> model logic fails to be correc

> Prolog by itself is a very bad theorem prover and it is very limited
> framework for formal logic, because it implements only Horn clauses.

None-the-less by evaluating expressions on the basis of facts
(expression known to be true) and rules (truth preserving operations)
and having negation as failure then all of the errors of logic are
corrected and Tarski's undefinability theorem fails.
https://liarparadox.org/Tarski_275_276.pdf

Because there are ways to do Higher Order Logic in Prolog I don't see
how any of its limitations can make any actual difference.

> However it is a very good programming language and you can implement any
> theorem prover in it, like you can implement any theorem prover in C++
> or Java.
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/22 15:55, olcott wrote:
> On 5/2/2022 8:35 AM, Aleksy Grabowski wrote:
>>> The whole purpose of this thread is to find out exactly how to
>>> encode: "This sentence is not true" in Prolog when we assume that
>>> True is exactly the same thing as Provable in Prolog.
>>
>> "This sentence is not provable" can be naïvely encoded:
>>
>> g :- \+ g.
>>
>> Then you can ask Prolog if this sentence is true:
>>
>> ?- g.
>>
>> Prolog will give you the only correct answer — no answer 🙃.
>
> That is great, now what happens when we encode:
> "This sentence is provable" in Prolog?
>
> What happens when we test both of these with
> unify_with_occurs_check ?

"This sentence is provable"

g.

Both of sentences are true at the same time:

both :- g, \+ g.

Then query:

?- both.

doesn't terminate, which is correct behavior for such paradoxical
statement. Did you expect some answer here? What it should be then? I'm
not very good at hardcore formal logic I'm just a programmer - not
mathematician, but I think there shouldn't be an answer.

Also I don't get how unification is even relevant here.

> None-the-less by evaluating expressions on the basis of facts
> (expression known to be true) and rules (truth preserving operations) and
> having negation as failure then all of the errors of logic are corrected
> and Tarski's undefinability theorem fails.
> https://liarparadox.org/Tarski_275_276.pdf

I'm afraid I can't comment on this

> Because there are ways to do Higher Order Logic in Prolog I don't see
> how any of its limitations can make any actual difference.

Agree, many limitation can be fixed, like unfair enumeration for some
predicates, bad termination qualities for some correct programs, or as
you said higher order logic (I don't know why you ever need it in a real
program, but that's another topic).

On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
> > The whole purpose of this thread is to find out exactly how to encode:
> > "This sentence is not true" in Prolog when we assume that True is
> > exactly the same thing as Provable in Prolog.

As long as it's equal to "<whatever> is not provable",
that's just any proposition <whatever> that fails, e.g.
g :- fail. As to how to rather encode self-referentiality,
and to begin with one needs first-order, that's something
to think about... just I am not sure how you do without
the whole Goedel construction unless by using Prolog
and maybe its meta-programming in some clever way.

> "This sentence is not provable" can be naïvely encoded:
>
> g :- \+ g.
>
> Then you can ask Prolog if this sentence is true:
>
> ?- g.

Prolog won't give any answer, it'll just crash. You (think you)
know what the answer is, but in fact it's the same answer
you'd get with g :- g.

Julio

On 5/2/22 16:59, Julio Di Egidio wrote:
> On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
>> "This sentence is not provable" can be naïvely encoded:
>>
>> g :- \+ g.
>>
>> Then you can ask Prolog if this sentence is true:
>>
>> ?- g.
>
> Prolog won't give any answer, it'll just crash. You (think you)
> know what the answer is, but in fact it's the same answer
> you'd get with g :- g.
>
> Julio

Yep, that's exactly what I was saying. IMHO, the only correct behavior
is to go to infinite loop and refuse to give any answer.

--
Alex Grabowski

On 5/2/2022 9:28 AM, Aleksy Grabowski wrote:
> On 5/2/22 15:55, olcott wrote:
>> On 5/2/2022 8:35 AM, Aleksy Grabowski wrote:
>>>> The whole purpose of this thread is to find out exactly how to
>>>> encode: "This sentence is not true" in Prolog when we assume that
>>>> True is exactly the same thing as Provable in Prolog.
>>>
>>> "This sentence is not provable" can be naïvely encoded:
>>>
>>> g :- \+ g.
>>>
>>> Then you can ask Prolog if this sentence is true:
>>>
>>> ?- g.
>>>
>>> Prolog will give you the only correct answer — no answer 🙃.
>>
>> That is great, now what happens when we encode:
>> "This sentence is provable" in Prolog?
>>
>> What happens when we test both of these with
>> unify_with_occurs_check ?
>
> "This sentence is provable"
>
>     g.
>
> Both of sentences are true at the same time:
>
>     both :- g, \+ g.
>
> Then query:
>
>     ?- both.
>
> doesn't terminate, which is correct behavior for such paradoxical
> statement. Did you expect some answer here? What it should be then? I'm
> not very good at hardcore formal logic I'm just a programmer - not
> mathematician, but I think there shouldn't be an answer.
>

That is great. That shows when Gödel's 1931 Incompleteness Theorem is
transformed into its barest possible essence Prolog proves it to be
ill-formed.

What is happening internally that causes the expression to never terminate?

> Also I don't get how unification is even relevant here.
>
>> None-the-less by evaluating expressions on the basis of facts
>> (expression known to be true) and rules (truth preserving operations) and
>> having negation as failure then all of the errors of logic are corrected
>> and Tarski's undefinability theorem fails.
>> https://liarparadox.org/Tarski_275_276.pdf
>
> I'm afraid I can't comment on this
>
>> Because there are ways to do Higher Order Logic in Prolog I don't see
>> how any of its limitations can make any actual difference.
>
> Agree, many limitation can be fixed, like unfair enumeration for some
> predicates, bad termination qualities for some correct programs, or as
> you said higher order logic (I don't know why you ever need it in a real
> program, but that's another topic).
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/22 17:24, olcott wrote:
> On 5/2/2022 9:28 AM, Aleksy Grabowski wrote:
>> On 5/2/22 15:55, olcott wrote:
>>> On 5/2/2022 8:35 AM, Aleksy Grabowski wrote:
>>>>> The whole purpose of this thread is to find out exactly how to
>>>>> encode: "This sentence is not true" in Prolog when we assume that
>>>>> True is exactly the same thing as Provable in Prolog.
>>>>
>>>> "This sentence is not provable" can be naïvely encoded:
>>>>
>>>> g :- \+ g.
>>>>
>>>> Then you can ask Prolog if this sentence is true:
>>>>
>>>> ?- g.
>>>>
>>>> Prolog will give you the only correct answer — no answer 🙃.
>>>
>>> That is great, now what happens when we encode:
>>> "This sentence is provable" in Prolog?
>>>
>>> What happens when we test both of these with
>>> unify_with_occurs_check ?
>>
>> "This sentence is provable"
>>
>>      g.
>>
>> Both of sentences are true at the same time:
>>
>>      both :- g, \+ g.
>>
>> Then query:
>>
>>      ?- both.
>>
>> doesn't terminate, which is correct behavior for such paradoxical
>> statement. Did you expect some answer here? What it should be then?
>> I'm not very good at hardcore formal logic I'm just a programmer - not
>> mathematician, but I think there shouldn't be an answer.
>>
>
> That is great. That shows when Gödel's 1931 Incompleteness Theorem is
> transformed into its barest possible essence Prolog proves it to be
> ill-formed.
>
> What is happening internally that causes the expression to never terminate?

Some definitions. The part before `:-` is called head, and after is
called body. Conceptually the model of execution of Prolog programs
looks more-or-less as follows:

0. If predicate doesn't have body it is always true.
1. Assume that head is false.
2. Check if we can find a counter-example by proving body.
3. If counter-example was found then previous assumption is incorrect
and in fact head should be true. If counter-example wasn't found then
our assumption was correct and head is false.
4. Recursively apply same rules for each clause in the body.

In our example Prolog will just execute `g` ad infinitum.

--
Alex Grabowski

On 5/2/2022 9:59 AM, Julio Di Egidio wrote:
> On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
>>> The whole purpose of this thread is to find out exactly how to encode:
>>> "This sentence is not true" in Prolog when we assume that True is
>>> exactly the same thing as Provable in Prolog.
>
> As long as it's equal to "<whatever> is not provable",
> that's just any proposition <whatever> that fails, e.g.
> g :- fail. As to how to rather encode self-referentiality,
> and to begin with one needs first-order, that's something
> to think about... just I am not sure how you do without
> the whole Goedel construction unless by using Prolog
> and maybe its meta-programming in some clever way.
>
>> "This sentence is not provable" can be naïvely encoded:
>>
>> g :- \+ g.
>>
>> Then you can ask Prolog if this sentence is true:
>>
>> ?- g.
>
> Prolog won't give any answer, it'll just crash. You (think you)
> know what the answer is, but in fact it's the same answer
> you'd get with g :- g.
>
> Julio

That is exactly what I expected.
Does it crash because it ran out of memory?

unify_with_occurs_check is supposed to determine in advance that
unification will crash. Can it be applied to the above?

Do we have any Prolog that shows in advance that the above expressions
would crash?

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On Monday, 2 May 2022 at 17:45:26 UTC+2, olcott wrote:
> On 5/2/2022 9:59 AM, Julio Di Egidio wrote:
> > On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
> >>> The whole purpose of this thread is to find out exactly how to encode:
> >>> "This sentence is not true" in Prolog when we assume that True is
> >>> exactly the same thing as Provable in Prolog.
> >
> > As long as it's equal to "<whatever> is not provable",
> > that's just any proposition <whatever> that fails, e.g.
> > g :- fail. As to how to rather encode self-referentiality,
> > and to begin with one needs first-order, that's something
> > to think about... just I am not sure how you do without
> > the whole Goedel construction unless by using Prolog
> > and maybe its meta-programming in some clever way.
> >
> >> "This sentence is not provable" can be naïvely encoded:
> >>
> >> g :- \+ g.
> >>
> >> Then you can ask Prolog if this sentence is true:
> >>
> >> ?- g.
> >
> > Prolog won't give any answer, it'll just crash. You (think you)
> > know what the answer is, but in fact it's the same answer
> > you'd get with g :- g.
>
> That is exactly what I expected.

g:-\+g as g:-g are literally and simply infinite loops: neither
captures anything deep about anything. Aka plain and
simple divergent computation.

> Does it crash because it ran out of memory?

Yes, but even if it didn't, it'd be you at some point who would
have to switch it off. And still that wouldn't be a proof of
anything.

> unify_with_occurs_check is supposed to determine in
> advance that unification will crash. Can it be applied to
> the above?

So far you aren't using unification at all: you need to go
first order, i.e. predicates with (variable) arguments.

> Do we have any Prolog that shows in advance that the
> above expressions would crash?

Would "not terminate", "crash" is quite broader... and no,
not in general: i.e. not until you solve the halting problem.

Julio

On 5/2/2022 10:44 AM, Aleksy Grabowski wrote:
> On 5/2/22 17:24, olcott wrote:
>> On 5/2/2022 9:28 AM, Aleksy Grabowski wrote:
>>> On 5/2/22 15:55, olcott wrote:
>>>> On 5/2/2022 8:35 AM, Aleksy Grabowski wrote:
>>>>>> The whole purpose of this thread is to find out exactly how to
>>>>>> encode: "This sentence is not true" in Prolog when we assume that
>>>>>> True is exactly the same thing as Provable in Prolog.
>>>>>
>>>>> "This sentence is not provable" can be naïvely encoded:
>>>>>
>>>>> g :- \+ g.
>>>>>
>>>>> Then you can ask Prolog if this sentence is true:
>>>>>
>>>>> ?- g.
>>>>>
>>>>> Prolog will give you the only correct answer — no answer 🙃.
>>>>
>>>> That is great, now what happens when we encode:
>>>> "This sentence is provable" in Prolog?
>>>>
>>>> What happens when we test both of these with
>>>> unify_with_occurs_check ?
>>>
>>> "This sentence is provable"
>>>
>>>      g.
>>>
>>> Both of sentences are true at the same time:
>>>
>>>      both :- g, \+ g.
>>>
>>> Then query:
>>>
>>>      ?- both.
>>>
>>> doesn't terminate, which is correct behavior for such paradoxical
>>> statement. Did you expect some answer here? What it should be then?
>>> I'm not very good at hardcore formal logic I'm just a programmer -
>>> not mathematician, but I think there shouldn't be an answer.
>>>
>>
>> That is great. That shows when Gödel's 1931 Incompleteness Theorem is
>> transformed into its barest possible essence Prolog proves it to be
>> ill-formed.
>>
>> What is happening internally that causes the expression to never
>> terminate?
>
> Some definitions. The part before `:-` is called head, and after is
> called body. Conceptually the model of execution of Prolog programs
> looks more-or-less as follows:
>
>  0. If predicate doesn't have body it is always true.
>  1. Assume that head is false.
>  2. Check if we can find a counter-example by proving body.
>  3. If counter-example was found then previous assumption is incorrect
> and in fact head should be true. If counter-example wasn't found then
> our assumption was correct and head is false.
>  4. Recursively apply same rules for each clause in the body.
>
> In our example Prolog will just execute `g` ad infinitum.
>

That is beautiful and affirms the key element of all of my research on
incompleteness.

This is the mathematical definition of incompleteness:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).

It says expression φ of formal system T can neither be proved or
refuted. A formal system is comparable to a Prolog database. I have
always known that the issue is that expression φ is semantically
ill-formed, now I have Prolog agreeing with me.

>>> both :- g, \+ g.
>>>
>>> Then query:
>>>
>>> ?- both.
>>> doesn't terminate, which is correct behavior for such paradoxical
>>> statement. Did you expect some answer here? What it should be then?

Is there any Prolog that can detect that the above will not terminate
prior to executing it?

Does it specify the same sort of infinite structure that the following
Clocksin & Mellish text describes?

BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:

equal(X, X).?-
equal(foo(Y), Y).

that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y, which
appears within it. As a result, Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)

Clarification to: "foo(foo(foo(Y))), and so on":
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/2022 11:02 AM, Julio Di Egidio wrote:
> On Monday, 2 May 2022 at 17:45:26 UTC+2, olcott wrote:
>> On 5/2/2022 9:59 AM, Julio Di Egidio wrote:
>>> On Monday, 2 May 2022 at 15:35:10 UTC+2, Aleksy Grabowski wrote:
>>>>> The whole purpose of this thread is to find out exactly how to encode:
>>>>> "This sentence is not true" in Prolog when we assume that True is
>>>>> exactly the same thing as Provable in Prolog.
>>>
>>> As long as it's equal to "<whatever> is not provable",
>>> that's just any proposition <whatever> that fails, e.g.
>>> g :- fail. As to how to rather encode self-referentiality,
>>> and to begin with one needs first-order, that's something
>>> to think about... just I am not sure how you do without
>>> the whole Goedel construction unless by using Prolog
>>> and maybe its meta-programming in some clever way.
>>>
>>>> "This sentence is not provable" can be naïvely encoded:
>>>>
>>>> g :- \+ g.
>>>>
>>>> Then you can ask Prolog if this sentence is true:
>>>>
>>>> ?- g.
>>>
>>> Prolog won't give any answer, it'll just crash. You (think you)
>>> know what the answer is, but in fact it's the same answer
>>> you'd get with g :- g.
>>
>> That is exactly what I expected.
>
> g:-\+g as g:-g are literally and simply infinite loops: neither
> captures anything deep about anything. Aka plain and
> simple divergent computation.
>
>> Does it crash because it ran out of memory?
>
> Yes, but even if it didn't, it'd be you at some point who would
> have to switch it off. And still that wouldn't be a proof of
> anything.
>
>> unify_with_occurs_check is supposed to determine in
>> advance that unification will crash. Can it be applied to
>> the above?
>
> So far you aren't using unification at all: you need to go
> first order, i.e. predicates with (variable) arguments.
>
>> Do we have any Prolog that shows in advance that the
>> above expressions would crash?
>
> Would "not terminate", "crash" is quite broader... and no,
> not in general: i.e. not until you solve the halting problem.
>
> Julio

What is occurring internally with Prolog's evaluation of the above
expressions? Does it build an infinite structure?

I think that I have refuted the conventional proofs of the halting
problem. I spent a man-year creating the x86 operating system so that I
could encode the conventional HP counter example in C/x86. My halt
decider does correctly determine that its input specifies infinitely
nested simulation.

void P(u32 x)
{ if (H(x, x))
HERE: goto HERE;
return;
}

int main()
{ Output("Input_Halts = ", H((u32)P, (u32)P));
}

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/2/22 18:04, olcott wrote:
> Is there any Prolog that can detect that the above will not terminate
> prior to executing it?

As I have said previously, my example is naïve. Maybe if you will think
hard enough you can make it detect such conditions, probably by writing
meta-interpreter of some sort, and terminate. Personally, I don't think
that using Prolog can be accepted as a "rigorous proof" of anything.

> Does it specify the same sort of infinite structure that the following
> Clocksin & Mellish text describes?
>
> BEGIN:(Clocksin & Mellish 2003:254)
> Finally, a note about how Prolog matching sometimes differs from the
> unification used in Resolution. Most Prolog systems will allow you to
> satisfy goals like:
>
>   equal(X, X).?-
>   equal(foo(Y), Y).
>
> that is, they will allow you to match a term against an uninstantiated
> subterm of itself. In this example, foo(Y) is matched against Y, which
> appears within it. As a result, Y will stand for foo(Y), which is
> foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
> and so on. So Y ends up standing for some kind of infinite structure.
> END:(Clocksin & Mellish 2003:254)
>
> Clarification to: "foo(foo(foo(Y))), and so on":
> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
>

There can't be an infinite structure physically in computer memory, and
I think that programmers who implemented Prolog are smart enough not to
require large memory for such cases.

Maybe he refers for some abstract infinite structure, that need not to
exist on the hardware level.

--
Alex Grabowski

On 5/2/2022 11:38 AM, Aleksy Grabowski wrote:
> On 5/2/22 18:04, olcott wrote:
>> Is there any Prolog that can detect that the above will not terminate
>> prior to executing it?
>
> As I have said previously, my example is naïve. Maybe if you will think
> hard enough you can make it detect such conditions, probably by writing
> meta-interpreter of some sort, and terminate. Personally, I don't think
> that using Prolog can be accepted as a "rigorous proof" of anything.
>

I need to know more details about what is occurring internally (within
Prolog) when the expressions are executed.

>> Does it specify the same sort of infinite structure that the following
>> Clocksin & Mellish text describes?
>>
>> BEGIN:(Clocksin & Mellish 2003:254)
>> Finally, a note about how Prolog matching sometimes differs from the
>> unification used in Resolution. Most Prolog systems will allow you to
>> satisfy goals like:
>>
>>    equal(X, X).?-
>>    equal(foo(Y), Y).
>>
>> that is, they will allow you to match a term against an uninstantiated
>> subterm of itself. In this example, foo(Y) is matched against Y, which
>> appears within it. As a result, Y will stand for foo(Y), which is
>> foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
>> and so on. So Y ends up standing for some kind of infinite structure.
>> END:(Clocksin & Mellish 2003:254)
>>
>> Clarification to: "foo(foo(foo(Y))), and so on":
>> foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
>>
>
> There can't be an infinite structure physically in computer memory, and
> I think that programmers who implemented Prolog are smart enough not to
> require large memory for such cases.
>
> Maybe he refers for some abstract infinite structure, that need not to
> exist on the hardware level.
>

The above quote from Clocksin & Mellish refers to getting
unify_with_occurs_check to check in advance that unification would
require infinite memory.

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer