Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

RADIO SHACK LEVEL II BASIC READY >_


computers / comp.ai.philosophy / Re: Is this correct Prolog?

SubjectAuthor
* Is this correct Prolog?olcott
+* Re: Is this correct Prolog?Richard Damon
|+* Re: Is this correct Prolog?olcott
||`* Re: Is this correct Prolog?Richard Damon
|| `* Re: Is this correct Prolog?olcott
||  `* Re: Is this correct Prolog?Richard Damon
||   `* Re: Is this correct Prolog?olcott
||    `* Re: Is this correct Prolog?Richard Damon
||     `* Re: Is this correct Prolog?olcott
||      +* Re: Is this correct Prolog?Jeff Barnett
||      |+* Re: Is this correct Prolog?olcott
||      ||`- Re: Is this correct Prolog?Richard Damon
||      |`* Re: Is this correct Prolog?Mr Flibble
||      | +- Re: Is this correct Prolog?polcott
||      | +- Re: Is this correct Prolog?Richard Damon
||      | `- Re: Is this correct Prolog?Jeff Barnett
||      +* Re: Is this correct Prolog?Richard Damon
||      |`* Re: Is this correct Prolog?olcott
||      | `- Re: Is this correct Prolog?Richard Damon
||      `* Re: Is this correct Prolog?olcott
||       `* Re: Is this correct Prolog?Richard Damon
||        `* Re: Is this correct Prolog?olcott
||         `- Re: Is this correct Prolog?Richard Damon
|`* Re: Is this correct Prolog?olcott
| `* Re: Is this correct Prolog?olcott
|  +* Re: Is this correct Prolog?olcott
|  |`* Re: Is this correct Prolog?olcott
|  | `* Re: Is this correct Prolog?olcott
|  |  +- Re: Is this correct Prolog?Richard Damon
|  |  `* Re: Is this correct Prolog?olcott
|  |   `* Re: Is this correct Prolog?André G. Isaak
|  |    `* Re: Is this correct Prolog?olcott
|  |     +- Re: Is this correct Prolog?Richard Damon
|  |     `* Re: Is this correct Prolog?olcott
|  |      +* Re: Is this correct Prolog?André G. Isaak
|  |      |+* Re: Is this correct Prolog?olcott
|  |      ||+* Re: Is this correct Prolog?Richard Damon
|  |      |||`* Re: Is this correct Prolog?olcott
|  |      ||| `* Re: Is this correct Prolog?Richard Damon
|  |      |||  +- Re: Is this correct Prolog?André G. Isaak
|  |      |||  `* Re: Is this correct Prolog?olcott
|  |      |||   `* Re: Is this correct Prolog?Richard Damon
|  |      |||    `* Re: Is this correct Prolog?olcott
|  |      |||     `* Re: Is this correct Prolog?Richard Damon
|  |      |||      `* Re: Is this correct Prolog?olcott
|  |      |||       +- Re: Is this correct Prolog?André G. Isaak
|  |      |||       `* Re: Is this correct Prolog?Richard Damon
|  |      |||        `* Re: Is this correct Prolog?olcott
|  |      |||         +- Re: Is this correct Prolog?André G. Isaak
|  |      |||         `* Re: Is this correct Prolog?Richard Damon
|  |      |||          `* Re: Is this correct Prolog?olcott
|  |      |||           `- Re: Is this correct Prolog?Richard Damon
|  |      ||`* Re: Is this correct Prolog?André G. Isaak
|  |      || +* Re: Is this correct Prolog?olcott
|  |      || |`* Re: Is this correct Prolog?André G. Isaak
|  |      || | `* Re: _Is_this_correct_Prolog?_[_André_is_proven_olcott
|  |      || |  `* Re: _Is_this_correct_Prolog?_[_André_is_proven_André G. Isaak
|  |      || |   `- Re: _Is_this_correct_Prolog?_[_André_is_proven_olcott
|  |      || `* Re: _Is_this_correct_Prolog?_[_André_is_proven_olcott
|  |      ||  `* Re: _Is_this_correct_Prolog?_[_André_is_proven_Richard Damon
|  |      ||   `- Re: _Is_this_correct_Prolog?_[_André_is_proven_olcott
|  |      |`- Re: Is this correct Prolog?olcott
|  |      `- Re: Is this correct Prolog?Richard Damon
|  `* Re: Is this correct Prolog?olcott
|   `- Re: Is this correct Prolog?André G. Isaak
+* Re: Is this correct Prolog?olcott
|`* Re: Is this correct Prolog?Richard Damon
| `* Re: Is this correct Prolog?olcott
|  `* Re: Is this correct Prolog?Richard Damon
|   `* Re: Is this correct Prolog?olcott
|    `- Re: Is this correct Prolog?Richard Damon
+* Re: Is this correct Prolog?olcott
|`* Re: Is this correct Prolog?Aleksy Grabowski
| `* Re: Is this correct Prolog?olcott
|  `* Re: Is this correct Prolog?Aleksy Grabowski
|   `* Re: Is this correct Prolog?olcott
|    `* Re: Is this correct Prolog?Aleksy Grabowski
|     `* Re: Is this correct Prolog?olcott
|      +* Re: Is this correct Prolog?Aleksy Grabowski
|      |`* Re: Is this correct Prolog?olcott
|      | `* Re: Is this correct Prolog?Aleksy Grabowski
|      |  `- Re: Is this correct Prolog?olcott
|      `* Re: Is this correct Prolog?Jeff Barnett
|       +* Re: Is this correct Prolog?Mr Flibble
|       |`- Re: Is this correct Prolog?olcott
|       `* Re: Is this correct Prolog?olcott
|        `* Re: Is this correct Prolog?Richard Damon
|         `* Re: Is this correct Prolog?Aleksy Grabowski
|          +* Re: Is this correct Prolog?Ben
|          |`* Re: Is this correct Prolog?olcott
|          | +* Re: Is this correct Prolog?Ben
|          | |`* Re: Is this correct Prolog?olcott
|          | | +* Re: Is this correct Prolog?Richard Damon
|          | | |`* Re: Is this correct Prolog? [ Tarski ]olcott
|          | | | `* Re: Is this correct Prolog? [ Tarski ]Richard Damon
|          | | |  +* Re: Is this correct Prolog? [ Tarski ]olcott
|          | | |  |`- Re: Is this correct Prolog? [ Tarski ]Richard Damon
|          | | |  `* Re: Is this correct Prolog? [ Tarski ]olcott
|          | | |   +* Re: Is this correct Prolog? [ Tarski ]André G. Isaak
|          | | |   |`- Re: Is this correct Prolog? [ Tarski ]olcott
|          | | |   `* Re: Is this correct Prolog? [ Tarski ]Richard Damon
|          | | `- Re: Is this correct Prolog?Ben
|          | `* Re: Is this correct Prolog?André G. Isaak
|          `* Re: Is this correct Prolog?olcott
`* Re: Is this correct Prolog?olcott

Pages:123456
Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Forte - www.forteinc.com
Date: Mon, 2 May 2022 11:10 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!hirsch.in-berlin.de!bolzen.all.de!npeer.as286.net!npeer-ng0.as286.net!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx13.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<FdSdnWijBKlSIfP_nZ2dnUU7_8xh4p2d@giganews.com>
<20220501185933.000045ad@reddwarf.jmc>
<d9KdnQdt_bnfTPP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4mjq0$7nf$1@dont-email.me>
<hYKdnb4ZyYB0RfP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mmmg$t4u$1@dont-email.me>
<APOdndfNnIH7ffP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mnu6$96k$1@dont-email.me>
<GYmdnUXY8oBkfvP_nZ2dnUU7_83NnZ2d@giganews.com> <t4moi2$cct$1@dont-email.me>
<Z6edncOlEsUXevP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mr1h$1q0$1@dont-email.me>
<SJGdnZf-9cUobfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mrsh$871$1@dont-email.me>
<Q56dnS17EP9PnvL_nZ2dnUU7_8xh4p2d@giganews.com>
<xxDbK.161779$Kdf.72054@fx96.iad> <t4n275$mr8$1@dont-email.me>
<2zEbK.452500$t2Bb.336668@fx98.iad> <t4nabt$5s4$2@dont-email.me>
<CwGbK.162528$Kdf.21366@fx96.iad> <t4ndjk$sn3$1@dont-email.me>
<n8HbK.388178$f2a5.198381@fx48.iad> <t4nf25$51n$1@dont-email.me>
<HCHbK.487830$SeK9.17961@fx97.iad> <t4nho0$ks6$1@dont-email.me>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <t4nho0$ks6$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 310
Message-ID: <G_ObK.690634$LN2.672813@fx13.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Mon, 2 May 2022 07:10:32 -0400
X-Received-Bytes: 15482
View all headers
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.

You see words which are not there and don't see the words that are there.

Godel talks of a way to use the form of any epistemological antinomy to build a similar argument to his G.

I think one thing that maybe you don't understand about G and the Liar Paradox is that this G IS built on the Liar Paradox so I think part of your issue is that you are trying to argue about the possibility to make a different G but from the Liar's Paradox, when this one was. The fact you don't see that G, as is, as being based on the Liar's Paradox, means you don't understand the way it is actually formed on the Liar's paradox.


What he is denying, that seems beyound your ability to understand, so much so tha that you remove it from your messages, that this fact doesn't make the G itself a "Liar Paradox" that isn't a Truth Bearing like you claim.

Maybe YOU should be looking at the actual facts of who said what, and see who is guilty of lying.

I think you are getting very close to that Lake of Fire.

Click here to read the complete article
Subject: Re: Is this correct Prolog?
From: Aleksy Grabowski
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 11:49 UTC
References: 1 2 3 4 5 6
Path: i2pn2.org!i2pn.org!news.swapon.de!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: hur...@gmail.com (Aleksy Grabowski)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 13:49:17 +0200
Organization: A noiseless patient Spider
Lines: 104
Message-ID: <t4ogft$8dt$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 11:49:17 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="a6568d70f53fb3c7501baf4d09c7115e";
logging-data="8637"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/zV2Nc1AZaTeQYW6TFIFIr"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:98.0) Gecko/20100101
Thunderbird/98.0
Cancel-Lock: sha1:AsdMwJbtGegnYnPf6pHthjpqY5g=
In-Reply-To: <KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com>
Content-Language: en-US
View all headers
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



Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 13:09 UTC
References: 1 2 3 4 5 6 7
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 08:09:50 -0500
Organization: A noiseless patient Spider
Lines: 140
Message-ID: <t4ol6v$hpr$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 13:09:51 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="18235"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18NNRR566tDoHZvzh8WRdJJ"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:AhMS0rPE6lS3GLbx9MYhM1yjdq8=
In-Reply-To: <t4ogft$8dt$1@dont-email.me>
Content-Language: en-US
View all headers
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


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 13:19 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 08:19:07 -0500
Organization: A noiseless patient Spider
Lines: 295
Message-ID: <t4olod$mce$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<20220501185933.000045ad@reddwarf.jmc>
<d9KdnQdt_bnfTPP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4mjq0$7nf$1@dont-email.me>
<hYKdnb4ZyYB0RfP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mmmg$t4u$1@dont-email.me>
<APOdndfNnIH7ffP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mnu6$96k$1@dont-email.me>
<GYmdnUXY8oBkfvP_nZ2dnUU7_83NnZ2d@giganews.com> <t4moi2$cct$1@dont-email.me>
<Z6edncOlEsUXevP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mr1h$1q0$1@dont-email.me>
<SJGdnZf-9cUobfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mrsh$871$1@dont-email.me>
<Q56dnS17EP9PnvL_nZ2dnUU7_8xh4p2d@giganews.com>
<xxDbK.161779$Kdf.72054@fx96.iad> <t4n275$mr8$1@dont-email.me>
<2zEbK.452500$t2Bb.336668@fx98.iad> <t4nabt$5s4$2@dont-email.me>
<CwGbK.162528$Kdf.21366@fx96.iad> <t4ndjk$sn3$1@dont-email.me>
<n8HbK.388178$f2a5.198381@fx48.iad> <t4nf25$51n$1@dont-email.me>
<HCHbK.487830$SeK9.17961@fx97.iad> <t4nho0$ks6$1@dont-email.me>
<G_ObK.690634$LN2.672813@fx13.iad>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 13:19:09 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="22926"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+4elBXpV+pbWAb2TSd/Ptx"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:3wf7cQhVTpuPnn7LqK8zw+yFq4I=
In-Reply-To: <G_ObK.690634$LN2.672813@fx13.iad>
Content-Language: en-US
View all headers
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.


I trim so that we can stay focused on the point at hand and not diverge into many unrelated points. The main way that all of the rebuttals of my work are formed is changing the subject to another different subject and the rebutting this different subject. I cut all that bullshit out.

You see words which are not there and don't see the words that are there.

Godel talks of a way to use the form of any epistemological antinomy to build a similar argument to his G.

I think one thing that maybe you don't understand about G and the Liar Paradox is that this G IS built on the Liar Paradox

That is well put. G takes the exact same idea as the liar paradox and then implements this liar paradox with 100,000-fold of additional purely extraneous complexity.

so I think part of your issue is that you are trying to argue about the possibility to make a different G but from the Liar's Paradox, when this one was. The fact you don't see that G, as is, as being based on the Liar's Paradox, means you don't understand the way it is actually formed on the Liar's paradox.

Click here to read the complete article
Subject: Re: Is this correct Prolog?
From: Aleksy Grabowski
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 13:35 UTC
References: 1 2 3 4 5 6 7 8
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: hur...@gmail.com (Aleksy Grabowski)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 15:35:08 +0200
Organization: A noiseless patient Spider
Lines: 28
Message-ID: <t4ommc$8dt$2@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 13:35:08 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="a6568d70f53fb3c7501baf4d09c7115e";
logging-data="8637"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18M1VHVRvzFxrULEKobWn8n"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:98.0) Gecko/20100101
Thunderbird/98.0
Cancel-Lock: sha1:Bun09XZq42EOuu7bcWK4Lrlzhyw=
In-Reply-To: <t4ol6v$hpr$1@dont-email.me>
Content-Language: en-US
View all headers
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



Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 13:55 UTC
References: 1 2 3 4 5 6 7 8 9
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 08:55:55 -0500
Organization: A noiseless patient Spider
Lines: 49
Message-ID: <t4ontc$93n$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 13:55:57 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="9335"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/qv4G7UWCOi2AsvBQYjtdm"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:9uK15UptDORiZ/+3aUBMh+dBoQE=
In-Reply-To: <t4ommc$8dt$2@dont-email.me>
Content-Language: en-US
View all headers
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


Subject: Re: Is this correct Prolog?
From: Aleksy Grabowski
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 14:28 UTC
References: 1 2 3 4 5 6 7 8 9 10
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: hur...@gmail.com (Aleksy Grabowski)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 16:28:40 +0200
Organization: A noiseless patient Spider
Lines: 57
Message-ID: <t4opqo$g2g$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 14:28:40 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="a6568d70f53fb3c7501baf4d09c7115e";
logging-data="16464"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18fc50Fh0nxTUt2ilf87J/i"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:98.0) Gecko/20100101
Thunderbird/98.0
Cancel-Lock: sha1:Eu5e++AXeJZLTZfus1ajE/tfeXY=
In-Reply-To: <t4ontc$93n$1@dont-email.me>
Content-Language: en-US
View all headers
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).



Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 15:24 UTC
References: 1 2 3 4 5 6 7 8 9 10 11
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 10:24:09 -0500
Organization: A noiseless patient Spider
Lines: 70
Message-ID: <t4ot2r$o65$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 15:24:11 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="24773"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18DluTA1Fsu6xZtro1q/GjY"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:TxF4jnz2wsjuEjkxIakxzIPoXpg=
In-Reply-To: <t4opqo$g2g$1@dont-email.me>
Content-Language: en-US
View all headers
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


Subject: Re: Is this correct Prolog?
From: Aleksy Grabowski
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 15:44 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: hur...@gmail.com (Aleksy Grabowski)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 17:44:41 +0200
Organization: A noiseless patient Spider
Lines: 65
Message-ID: <t4ou99$g2g$3@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 15:44:41 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="a6568d70f53fb3c7501baf4d09c7115e";
logging-data="16464"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/GjwcenpcrN9vlDg0AeK0b"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:98.0) Gecko/20100101
Thunderbird/98.0
Cancel-Lock: sha1:JeTPHJqg+F1giQGVMHcqnhbmSGs=
In-Reply-To: <t4ot2r$o65$1@dont-email.me>
Content-Language: en-US
View all headers
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



Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 16:04 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 11:04:26 -0500
Organization: A noiseless patient Spider
Lines: 111
Message-ID: <t4ovec$duq$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4ou99$g2g$3@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 16:04:28 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="14298"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18A0KegbROcWs9TtESxd9/J"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:6YdmzisbFtm+JWht2MU36GGhBsE=
In-Reply-To: <t4ou99$g2g$3@dont-email.me>
Content-Language: en-US
View all headers
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


Subject: Re: Is this correct Prolog?
From: Aleksy Grabowski
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 16:38 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: hur...@gmail.com (Aleksy Grabowski)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 18:38:08 +0200
Organization: A noiseless patient Spider
Lines: 41
Message-ID: <t4p1dg$5pd$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4ou99$g2g$3@dont-email.me>
<t4ovec$duq$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 16:38:08 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="a6568d70f53fb3c7501baf4d09c7115e";
logging-data="5933"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18pzOrd9ugwVkza3+okbReh"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:98.0) Gecko/20100101
Thunderbird/98.0
Cancel-Lock: sha1:1JftXFmfDXeQrXVlEv6cenGWvO8=
In-Reply-To: <t4ovec$duq$1@dont-email.me>
Content-Language: en-US
View all headers
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



Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 16:49 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 11:49:51 -0500
Organization: A noiseless patient Spider
Lines: 51
Message-ID: <t4p23h$m0f$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4ou99$g2g$3@dont-email.me>
<t4ovec$duq$1@dont-email.me> <t4p1dg$5pd$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 May 2022 16:49:53 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="22543"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18i0YG1H8Wip+fNITji/kKZ"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:GeZRweFyqazQd2fg+Q0Go93WJ+Y=
In-Reply-To: <t4p1dg$5pd$1@dont-email.me>
Content-Language: en-US
View all headers
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


Subject: Re: Is this correct Prolog?
From: Jeff Barnett
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 17:28 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: jbb...@notatt.com (Jeff Barnett)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 11:28:23 -0600
Organization: A noiseless patient Spider
Lines: 26
Message-ID: <t4p4br$b81$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 2 May 2022 17:28:27 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="ed778c511e6ee7d3960b96da8b859b29";
logging-data="11521"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+HIg/dthGFhQ4WytfKSnXALnS3jzzmj9I="
User-Agent: Mozilla/5.0 (Windows NT 6.1; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:gd1t4Dmbfs02v6I2PYKdQMBaNh4=
In-Reply-To: <t4ot2r$o65$1@dont-email.me>
Content-Language: en-US
View all headers
On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE


I will attempt to summarize the level of the idiot's understanding of Prolog: The level is the same as of his understanding of math, logic, C, C++, software engineering, programming, programming methodology, Turing Machines, and other specific topics in these general categories. He is capable of moving his eyes through a few paragraphs but not reading anything. This is a common learning disability. He can cut and paste from what little is eyes scan but, in general, he can neither comprehend the little he's seen nor can he amalgamate concepts from the bits and pieces he has visited.

His approach to gaining and demonstrating understanding is best represented by a comic's view of monkeys exploring objects new to them: biting things, hitting other objects with the new one, stirring feces and seeing if it will stick and can be thrown etc. The problem with this metaphor is that monkeys are intelligent and our idiot is not. When the monkey is done with initial exploration, it has an idea whether the new object can serve some useful purpose; in any event, the monkey had fun. The idiot, on the other hand, never discoveries the usefulness of the potential new knowledge because he doesn't have the attention span or curiosity to do so. That's why he is an idiot and not as smart or as wise as the monkey though he too has fun.
--
Jeff Barnett


Subject: Re: Is this correct Prolog?
From: Mr Flibble
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: Jupiter Mining Corp
Date: Mon, 2 May 2022 18:41 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!fx03.ams4.POSTED!not-for-mail
From: flib...@reddwarf.jmc (Mr Flibble)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Message-ID: <20220502194142.00001a3c@reddwarf.jmc>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me>
<t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com>
<t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me>
<t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me>
<t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me>
<t4p4br$b81$1@dont-email.me>
Organization: Jupiter Mining Corp
X-Newsreader: Claws Mail 3.17.8 (GTK+ 2.24.33; x86_64-w64-mingw32)
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Lines: 36
X-Complaints-To: abuse@eweka.nl
NNTP-Posting-Date: Mon, 02 May 2022 18:41:42 UTC
Date: Mon, 2 May 2022 19:41:42 +0100
X-Received-Bytes: 2900
View all headers
On Mon, 2 May 2022 11:28:23 -0600
Jeff Barnett <jbb@notatt.com> wrote:

On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE


I will attempt to summarize the level of the idiot's understanding of
Prolog: The level is the same as of his understanding of math, logic,
C, C++, software engineering, programming, programming methodology,
Turing Machines, and other specific topics in these general
categories. He is capable of moving his eyes through a few paragraphs
but not reading anything. This is a common learning disability. He
can cut and paste from what little is eyes scan but, in general, he
can neither comprehend the little he's seen nor can he amalgamate
concepts from the bits and pieces he has visited.

His approach to gaining and demonstrating understanding is best
represented by a comic's view of monkeys exploring objects new to
them: biting things, hitting other objects with the new one, stirring
feces and seeing if it will stick and can be thrown etc. The problem
with this metaphor is that monkeys are intelligent and our idiot is
not. When the monkey is done with initial exploration, it has an idea
whether the new object can serve some useful purpose; in any event,
the monkey had fun. The idiot, on the other hand, never discoveries
the usefulness of the potential new knowledge because he doesn't have
the attention span or curiosity to do so. That's why he is an idiot
and not as smart or as wise as the monkey though he too has fun.

The ad hominem attack is a logical fallacy: so it is in fact YOU who is
throwing excrement at the walls, not Olcott. Attack the argument not the
person, dear.

https://en.wikipedia.org/wiki/Ad_hominem

/Flibble



Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 19:26 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 14:26:38 -0500
Organization: A noiseless patient Spider
Lines: 45
Message-ID: <t4pb9e$al3$3@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<20220502194142.00001a3c@reddwarf.jmc>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 2 May 2022 19:26:38 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="10915"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/8bqDZnfKadFVZ4qaZfaEB"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:iDaIWJOWHNRQr9TWcqc3Zvk0+3k=
In-Reply-To: <20220502194142.00001a3c@reddwarf.jmc>
Content-Language: en-US
View all headers
On 5/2/2022 1:41 PM, Mr Flibble wrote:
On Mon, 2 May 2022 11:28:23 -0600
Jeff Barnett <jbb@notatt.com> wrote:

On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE


I will attempt to summarize the level of the idiot's understanding of
Prolog: The level is the same as of his understanding of math, logic,
C, C++, software engineering, programming, programming methodology,
Turing Machines, and other specific topics in these general
categories. He is capable of moving his eyes through a few paragraphs
but not reading anything. This is a common learning disability. He
can cut and paste from what little is eyes scan but, in general, he
can neither comprehend the little he's seen nor can he amalgamate
concepts from the bits and pieces he has visited.

His approach to gaining and demonstrating understanding is best
represented by a comic's view of monkeys exploring objects new to
them: biting things, hitting other objects with the new one, stirring
feces and seeing if it will stick and can be thrown etc. The problem
with this metaphor is that monkeys are intelligent and our idiot is
not. When the monkey is done with initial exploration, it has an idea
whether the new object can serve some useful purpose; in any event,
the monkey had fun. The idiot, on the other hand, never discoveries
the usefulness of the potential new knowledge because he doesn't have
the attention span or curiosity to do so. That's why he is an idiot
and not as smart or as wise as the monkey though he too has fun.

The ad hominem attack is a logical fallacy: so it is in fact YOU who is
throwing excrement at the walls, not Olcott. Attack the argument not the
person, dear.

https://en.wikipedia.org/wiki/Ad_hominem

/Flibble


Yes Jeff is mostly a Jackass. Once in a very great while he says something interesting. This is very rare yet thankfully more often than never.

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


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 19:32 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 14:32:51 -0500
Organization: A noiseless patient Spider
Lines: 44
Message-ID: <t4pbl5$g28$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 2 May 2022 19:32:53 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d3e0e423381921f0d6386f2137e81510";
logging-data="16456"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18BhnYi/zbhFQ3E0e7mAWrh"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:bKHak64qOzLGs8OVZn5MWSykWd8=
In-Reply-To: <t4p4br$b81$1@dont-email.me>
Content-Language: en-US
View all headers
On 5/2/2022 12:28 PM, Jeff Barnett wrote:
On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE


I will attempt to summarize the level of the idiot's understanding of Prolog: The level is the same as of his understanding of math, logic, C, C++, software engineering, programming, programming methodology, Turing Machines, and other specific topics in these general categories. He is capable of moving his eyes through a few paragraphs but not reading anything. This is a common learning disability. He can cut and paste from what little is eyes scan but, in general, he can neither comprehend the little he's seen nor can he amalgamate concepts from the bits and pieces he has visited.

His approach to gaining and demonstrating understanding is best represented by a comic's view of monkeys exploring objects new to them: biting things, hitting other objects with the new one, stirring feces and seeing if it will stick and can be thrown etc. The problem with this metaphor is that monkeys are intelligent and our idiot is not. When the monkey is done with initial exploration, it has an idea whether the new object can serve some useful purpose; in any event, the monkey had fun. The idiot, on the other hand, never discoveries the usefulness of the potential new knowledge because he doesn't have the attention span or curiosity to do so. That's why he is an idiot and not as smart or as wise as the monkey though he too has fun.

My key more important understanding of the fundamental architecture of Prolog is that it is anchored in sound deductive inference thus correctly all of the errors that have crept into logic since Aristotle's syllogism.

Start with known truths (Prolog facts) and only apply truth preserving operations (Prolog rules) to derive conclusions that can be relied on as true.

Also helpful is Prolog's negation as failure that does not make the huge mistake of assuming that every expression that is not true must be false.




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


Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Mon, 2 May 2022 22:28 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!news.swapon.de!news.uzoreto.com!npeer.as286.net!npeer-ng0.as286.net!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx41.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <t4pbl5$g28$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Lines: 52
Message-ID: <pWYbK.48$UWx1.17@fx41.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Mon, 2 May 2022 18:28:39 -0400
X-Received-Bytes: 4111
View all headers
On 5/2/22 3:32 PM, olcott wrote:
On 5/2/2022 12:28 PM, Jeff Barnett wrote:
On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE


I will attempt to summarize the level of the idiot's understanding of Prolog: The level is the same as of his understanding of math, logic, C, C++, software engineering, programming, programming methodology, Turing Machines, and other specific topics in these general categories. He is capable of moving his eyes through a few paragraphs but not reading anything. This is a common learning disability. He can cut and paste from what little is eyes scan but, in general, he can neither comprehend the little he's seen nor can he amalgamate concepts from the bits and pieces he has visited.

His approach to gaining and demonstrating understanding is best represented by a comic's view of monkeys exploring objects new to them: biting things, hitting other objects with the new one, stirring feces and seeing if it will stick and can be thrown etc. The problem with this metaphor is that monkeys are intelligent and our idiot is not. When the monkey is done with initial exploration, it has an idea whether the new object can serve some useful purpose; in any event, the monkey had fun. The idiot, on the other hand, never discoveries the usefulness of the potential new knowledge because he doesn't have the attention span or curiosity to do so. That's why he is an idiot and not as smart or as wise as the monkey though he too has fun.

My key more important understanding of the fundamental architecture of Prolog is that it is anchored in sound deductive inference thus correctly all of the errors that have crept into logic since Aristotle's syllogism.

Start with known truths (Prolog facts) and only apply truth preserving operations (Prolog rules) to derive conclusions that can be relied on as true.

Also helpful is Prolog's negation as failure that does not make the huge mistake of assuming that every expression that is not true must be false.


IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.

I am pretty sure that Prolog is NOT up to handling the logic needed to handle the mathematics needed to express Godel's G, or the Halting Problem.

Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you have only proven that your limited logic system can't reach them in expressibility.



Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Forte - www.forteinc.com
Date: Mon, 2 May 2022 22:38 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!news.uzoreto.com!npeer.as286.net!npeer-ng0.as286.net!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx04.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<20220501185933.000045ad@reddwarf.jmc>
<d9KdnQdt_bnfTPP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4mjq0$7nf$1@dont-email.me>
<hYKdnb4ZyYB0RfP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mmmg$t4u$1@dont-email.me>
<APOdndfNnIH7ffP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mnu6$96k$1@dont-email.me>
<GYmdnUXY8oBkfvP_nZ2dnUU7_83NnZ2d@giganews.com> <t4moi2$cct$1@dont-email.me>
<Z6edncOlEsUXevP_nZ2dnUU7_83NnZ2d@giganews.com> <t4mr1h$1q0$1@dont-email.me>
<SJGdnZf-9cUobfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mrsh$871$1@dont-email.me>
<Q56dnS17EP9PnvL_nZ2dnUU7_8xh4p2d@giganews.com>
<xxDbK.161779$Kdf.72054@fx96.iad> <t4n275$mr8$1@dont-email.me>
<2zEbK.452500$t2Bb.336668@fx98.iad> <t4nabt$5s4$2@dont-email.me>
<CwGbK.162528$Kdf.21366@fx96.iad> <t4ndjk$sn3$1@dont-email.me>
<n8HbK.388178$f2a5.198381@fx48.iad> <t4nf25$51n$1@dont-email.me>
<HCHbK.487830$SeK9.17961@fx97.iad> <t4nho0$ks6$1@dont-email.me>
<G_ObK.690634$LN2.672813@fx13.iad> <t4olod$mce$1@dont-email.me>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <t4olod$mce$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 321
Message-ID: <34ZbK.18092$h6X.14491@fx04.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Mon, 2 May 2022 18:38:57 -0400
X-Received-Bytes: 16199
View all headers
On 5/2/22 9:19 AM, olcott wrote:
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.


I trim so that we can stay focused on the point at hand and not diverge into many unrelated points. The main way that all of the rebuttals of my work are formed is changing the subject to another different subject and the rebutting this different subject. I cut all that bullshit out.

TRANSLATION: I trim out what will prove me wrong because I don't have time to think up other excuses.

You are just admitting failure, if not to yourself, to anyone with a real brain.


You see words which are not there and don't see the words that are there.

Godel talks of a way to use the form of any epistemological antinomy to build a similar argument to his G.

I think one thing that maybe you don't understand about G and the Liar Paradox is that this G IS built on the Liar Paradox

That is well put. G takes the exact same idea as the liar paradox and then implements this liar paradox with 100,000-fold of additional purely extraneous complexity.

Click here to read the complete article
Subject: Re: Is this correct Prolog?
From: Aleksy Grabowski
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 22:41 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Path: i2pn2.org!i2pn.org!aioe.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: hur...@gmail.com (Aleksy Grabowski)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 00:41:16 +0200
Organization: A noiseless patient Spider
Lines: 24
Message-ID: <t4pmmd$4f6$3@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 2 May 2022 22:41:17 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="4b907a72124f2b1ddcabbea6b8d013f1";
logging-data="4582"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/F5+Xq4vkxQOgbSkWmurvW"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:98.0) Gecko/20100101
Thunderbird/98.0
Cancel-Lock: sha1:xlHUFUkMef4L7b+Lu6S5PoHKYYw=
In-Reply-To: <pWYbK.48$UWx1.17@fx41.iad>
Content-Language: en-US
View all headers
IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.

I am pretty sure that Prolog is NOT up to handling the logic needed to handle the mathematics needed to express Godel's G, or the Halting Problem.

Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you have only proven that your limited logic system can't reach them in expressibility.


Thanks for confirmation, that's what exactly what I was trying to tell to topic poster in one of my previous posts. Prolog in it's bare form is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq theorem prover, I've never used it by myself, but it looks like one of the best proving assistants out there.

--
Alex Grabowski



Subject: Re: Is this correct Prolog?
From: Ben
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Followup: comp.theory
Organization: A noiseless patient Spider
Date: Mon, 2 May 2022 23:43 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Followup-To: comp.theory
Date: Tue, 03 May 2022 00:43:40 +0100
Organization: A noiseless patient Spider
Lines: 22
Message-ID: <87a6bzfqkz.fsf@bsb.me.uk>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com>
<t4ogft$8dt$1@dont-email.me> <t4ol6v$hpr$1@dont-email.me>
<t4ommc$8dt$2@dont-email.me> <t4ontc$93n$1@dont-email.me>
<t4opqo$g2g$1@dont-email.me> <t4ot2r$o65$1@dont-email.me>
<t4p4br$b81$1@dont-email.me> <t4pbl5$g28$1@dont-email.me>
<pWYbK.48$UWx1.17@fx41.iad> <t4pmmd$4f6$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="c3b430b0661d1b9b2cecb246d558f065";
logging-data="31813"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX182kUopmJ7i+N93Luz0iZPhGs0PPJG73Co="
Cancel-Lock: sha1:Z1mZgnHVQB0JsjKhVLadO0fIndA=
sha1:fLFWte0sQR4nQLWyAz2jcJiCJGI=
X-BSB-Auth: 1.f455c024d4cd63ab6cbb.20220503004340BST.87a6bzfqkz.fsf@bsb.me.uk
View all headers
Aleksy Grabowski <hurufu@gmail.com> writes:

IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your
logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.
I am pretty sure that Prolog is NOT up to handling the logic needed to
handle the mathematics needed to express Godel's G, or the Halting Problem.
Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
have only proven that your limited logic system can't reach them in expressibility.

Thanks for confirmation, that's what exactly what I was trying to tell
to topic poster in one of my previous posts. Prolog in it's bare form
is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq
theorem prover, I've never used it by myself, but it looks like one of
the best proving assistants out there.

And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).

--
Ben.


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Tue, 3 May 2022 00:11 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Path: i2pn2.org!i2pn.org!aioe.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 19:11:26 -0500
Organization: A noiseless patient Spider
Lines: 37
Message-ID: <t4prvg$oc2$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 3 May 2022 00:11:28 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="e4ddfd19553b2d0386451423b6459edd";
logging-data="24962"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19uE/jGHc59zf+9APs4iR0/"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:s58uUmpTj2wogxf9BwhSyHJz8hM=
In-Reply-To: <t4pmmd$4f6$3@dont-email.me>
Content-Language: en-US
View all headers
On 5/2/2022 5:41 PM, Aleksy Grabowski wrote:
IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.

I am pretty sure that Prolog is NOT up to handling the logic needed to handle the mathematics needed to express Godel's G, or the Halting Problem.

Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you have only proven that your limited logic system can't reach them in expressibility.


Thanks for confirmation, that's what exactly what I was trying to tell to topic poster in one of my previous posts. Prolog in it's bare form is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq theorem prover, I've never used it by myself, but it looks like one of the best proving assistants out there.


I might take a look at it. The key advantage of Prolog that that by basing its analysis on facts and rules and having negation as failure it corrects all of the errors of formal logic systems.

Prolog does not make the mistake of assuming that when an expression is not true that it must be false. Because of this Prolog can detect semantically ill-formed expressions that formal logic simply assumes are correct.

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


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Tue, 3 May 2022 00:35 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Path: i2pn2.org!i2pn.org!aioe.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 19:35:25 -0500
Organization: A noiseless patient Spider
Lines: 50
Message-ID: <t4ptcf$287$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <t4prvg$oc2$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 3 May 2022 00:35:27 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="e4ddfd19553b2d0386451423b6459edd";
logging-data="2311"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18Sa40RrkryfxgJRHpwCLGn"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:ExKwwDr9uDxTIhYpowe7etjUDwg=
In-Reply-To: <t4prvg$oc2$1@dont-email.me>
Content-Language: en-US
View all headers
On 5/2/2022 7:11 PM, olcott wrote:
On 5/2/2022 5:41 PM, Aleksy Grabowski wrote:
IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.

I am pretty sure that Prolog is NOT up to handling the logic needed to handle the mathematics needed to express Godel's G, or the Halting Problem.

Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you have only proven that your limited logic system can't reach them in expressibility.


Thanks for confirmation, that's what exactly what I was trying to tell to topic poster in one of my previous posts. Prolog in it's bare form is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq theorem prover, I've never used it by myself, but it looks like one of the best proving assistants out there.


I might take a look at it.

Coq is not an automated theorem prover
https://en.wikipedia.org/wiki/Coq

The key advantage of Prolog that that by basing its analysis on facts and rules

In other words it is based on the sound deductive inference model.

and having negation as failure it corrects all of the errors of formal logic systems.


Prolog does not make the mistake of assuming that when an expression is not true that it must be false. Because of this Prolog can detect semantically ill-formed expressions that formal logic simply assumes are correct.



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


Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Tue, 3 May 2022 00:47 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx96.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.lang.prolog,comp.theory,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <t4prvg$oc2$1@dont-email.me>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <t4prvg$oc2$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Lines: 51
Message-ID: <uY_bK.184231$Kdf.118513@fx96.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Mon, 2 May 2022 20:47:24 -0400
X-Received-Bytes: 3816
View all headers
On 5/2/22 8:11 PM, olcott wrote:
On 5/2/2022 5:41 PM, Aleksy Grabowski wrote:
IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.

I am pretty sure that Prolog is NOT up to handling the logic needed to handle the mathematics needed to express Godel's G, or the Halting Problem.

Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you have only proven that your limited logic system can't reach them in expressibility.


Thanks for confirmation, that's what exactly what I was trying to tell to topic poster in one of my previous posts. Prolog in it's bare form is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq theorem prover, I've never used it by myself, but it looks like one of the best proving assistants out there.


I might take a look at it. The key advantage of Prolog that that by basing its analysis on facts and rules and having negation as failure it corrects all of the errors of formal logic systems.

Prolog does not make the mistake of assuming that when an expression is not true that it must be false. Because of this Prolog can detect semantically ill-formed expressions that formal logic simply assumes are correct.


Except that, I believe, in Prolog, all expression are considered to be either True or False (and default to being called false if they aren't given as True or provable by the system as True.

Yes, there is a Unification test that allows you to ask if a statement would create a recursive loop, but that is NOT the same as an ill-formed expression.

Also, just because Prolog can't prove something doesn't mean it is not actually provable.

As I said, if you want to limit your logic to what Prolog can determine, go ahead, but realize you are leaving a lot of logical space as outside your domain of discussion, and that doesn't mean all that outside is "ill-formed", unless you are willing to say that Mathematics is ill-formed.


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Tue, 3 May 2022 00:57 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Path: i2pn2.org!i2pn.org!aioe.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Mon, 2 May 2022 19:57:28 -0500
Organization: A noiseless patient Spider
Lines: 42
Message-ID: <t4pulq$bci$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 3 May 2022 00:57:30 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="e4ddfd19553b2d0386451423b6459edd";
logging-data="11666"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/rKz15ID2+lxs+F3gvg+Gs"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:A9ZUerKywMzFseXRszdFALzv5yU=
In-Reply-To: <87a6bzfqkz.fsf@bsb.me.uk>
Content-Language: en-US
View all headers
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:

IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your
logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.
I am pretty sure that Prolog is NOT up to handling the logic needed to
handle the mathematics needed to express Godel's G, or the Halting Problem.
Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
have only proven that your limited logic system can't reach them in expressibility.

Thanks for confirmation, that's what exactly what I was trying to tell
to topic poster in one of my previous posts. Prolog in it's bare form
is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq
theorem prover, I've never used it by myself, but it looks like one of
the best proving assistants out there.

And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).


It is true that G is not provable. G is not provable because it is semantically incorrect in the exactly same way that the Liar Paradox is semantically incorrect.

Gödel says:
14 Every epistemological antinomy can likewise be used for a similar undecidability proof

André denied this six times yesterday
The Liar Paradox is an epistemological antinomy, thus can likewise be used for a similar undecidability proof.

Which means that the Liar Paradox is sufficiently equivalent to Gödel's G. Which means if the basic mechanism of epistemological antinomy is shown to be semantically incorrect then Gödel's G is shown to be semantically incorrect.

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


Subject: Re: Is this correct Prolog?
From: Ben
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Followup: comp.theory
Organization: A noiseless patient Spider
Date: Tue, 3 May 2022 02:21 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: ben.use...@bsb.me.uk (Ben)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Followup-To: comp.theory
Date: Tue, 03 May 2022 03:21:04 +0100
Organization: A noiseless patient Spider
Lines: 25
Message-ID: <874k27fjan.fsf@bsb.me.uk>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com>
<t4ogft$8dt$1@dont-email.me> <t4ol6v$hpr$1@dont-email.me>
<t4ommc$8dt$2@dont-email.me> <t4ontc$93n$1@dont-email.me>
<t4opqo$g2g$1@dont-email.me> <t4ot2r$o65$1@dont-email.me>
<t4p4br$b81$1@dont-email.me> <t4pbl5$g28$1@dont-email.me>
<pWYbK.48$UWx1.17@fx41.iad> <t4pmmd$4f6$3@dont-email.me>
<87a6bzfqkz.fsf@bsb.me.uk> <t4pulq$bci$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org; posting-host="c3b430b0661d1b9b2cecb246d558f065";
logging-data="14509"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/sCwWryqF6ToGLOt5Buh1uAafAwYnHM1c="
Cancel-Lock: sha1:2aByxQatNGRAqJD+Ef15gck3S3M=
sha1:ODA7T6u9GKAKO8AxqL0Ud5BKoUU=
X-BSB-Auth: 1.af3ddda75f91325a9937.20220503032104BST.874k27fjan.fsf@bsb.me.uk
View all headers
olcott <polcott2@gmail.com> writes:

On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:

Thanks for confirmation, that's what exactly what I was trying to tell
to topic poster in one of my previous posts. Prolog in it's bare form
is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq
theorem prover, I've never used it by myself, but it looks like one of
the best proving assistants out there.

And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).

It is true that G is not provable.

G is provable.  Proofs abound.  I was pointing out one in a proper proof
assistant, Coq.

--
Ben.
"le génie humain a des limites, quand la bêtise humaine n’en a pas"
Alexandre Dumas (fils)


Pages:123456
rocksolid light 0.7.2
clearneti2ptor