Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

panic: can't find /


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: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Date: Sun, 1 May 2022 12:09 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 07:09:08 -0500
Date: Sun, 1 May 2022 07:09:07 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4lkro$dl6$1@dont-email.me>
<EtqdnT58XtlA8_P_nZ2dnUU7_83NnZ2d@giganews.com>
<3EubK.14817$6j9b.13866@fx36.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <3EubK.14817$6j9b.13866@fx36.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <tqadnT2XDsz55fP_nZ2dnUU7_8xh4p2d@giganews.com>
Lines: 94
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-sx3r6E9qnOQuT3vORpLSqvXjNd3MghhoGMqhLIHf0itytWa52COS5DI81WNP/83RaxJnI1FMdzlnUmS!9rdnMh55omNXHfdqkblL2efyhKWN8f6zxhRP8Bk6pb34vkH/NhSOgu99fDFbM8E7NzOSRkhxS3U=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5660
View all headers
On 5/1/2022 7:01 AM, Richard Damon wrote:

On 5/1/22 7:28 AM, olcott wrote:
On 5/1/2022 4:45 AM, Mikko wrote:
On 2022-05-01 03:15:56 +0000, olcott said:

Not in this case, it is very obvious that no theorem prover can possibly prove any infinite expression.

Doesn't matter as you can't give an infinite expression to a theorem
prover.

Mikko


*You can and Prolog can detect and reject it*

Which just shows PROLOG can't handle that sort of expression, not that it logically doens't have a meaning.


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.

<inserted for clarity>
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
</inserted for clarity>

Note that, whereas they may allow you to construct something like this, most Prolog systems will not be able to write it out at the end. According to the formal definition of Unification, this kind of “infinite term” should never come to exist. Thus Prolog systems that allow a term to match an uninstantiated subterm of itself do not act correctly as Resolution theorem provers. In order to make them do so, we would have to add a check that a variable cannot be instantiated to something containing itself. Such a check, an occurs check, would be straightforward to implement, but would slow down the execution of Prolog programs considerably. Since it would only affect very few programs, most implementors have simply left it out 1.

1 The Prolog standard states that the result is undefined if a Prolog system attempts to match a term against an uninstantiated subterm of itself, which means that programs which cause this  to happen will not be portable. A portable program should ensure that wherever an occurs check might be applicable the built-in predicate unify_with_occurs_check/2 is used explicitly instead of the normal unification operation of the Prolog implementation. As its name suggests, this predicate acts like =/2 except that it fails if an occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)

Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.


So all Clocksin & Melish is saying is that such an expression fails in PROLOG, not that it doesn't have a valid logical meaning.


It correctly says that this is what the expression means:
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
Which means that it does not have a valid logical meaning.

The world is NOT Prolog, and I suspect Prolog isn't sufficient to handle the logic needed to process the Godel Sentence, so can't be used to disprove it.

This says that G is logically equivalent to its own unprovability in F
G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in Prolog.

Because
14 Every epistemological antinomy can likewise be used for a similar undecidability proof
then G ↔ ¬Provable(F, G) can likewise be used for a similar undecidability proof.

--
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: Sun, 1 May 2022 12:11 UTC
References: 1 2 3 4 5 6 7
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!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!fx46.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> <iLednaGFd9stPfD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4lkei$acm$1@dont-email.me> <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>
<u7ubK.20174$HLy4.14606@fx38.iad>
<i4mdnQwhosJo6fP_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <i4mdnQwhosJo6fP_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 103
Message-ID: <9OubK.452731$iK66.239461@fx46.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: Sun, 1 May 2022 08:11:50 -0400
X-Received-Bytes: 4774
View all headers
On 5/1/22 7:54 AM, olcott wrote:
On 5/1/2022 6:26 AM, Richard Damon wrote:
On 5/1/22 7:06 AM, olcott wrote:
On 5/1/2022 4:38 AM, Mikko wrote:
On 2022-04-30 20:48:47 +0000, olcott said:

On 4/30/2022 4:31 AM, Mikko wrote:
On 2022-04-30 07:02:23 +0000, olcott said:

LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

This is correct but to fail would also be correct.

?- unify_with_occurs_check(LP, not(true(LP))).
false.

unify_with_occurs_check must fail if the unified data structure
would contain loops.

Mikko


The above is the actual execution of actual Prolog code using
(SWI-Prolog (threaded, 64 bits, version 7.6.4).

Another Prolog implementation might interprete LP = not(true(LP)) differently
and still conform to the prolog standard.

According to Clocksin & Mellish it is not a mere loop, it is an "infinite term" thus infinitely recursive definition.

When discussing data structures, "infinite" and "loop" mean the same.
The data structure is infinitely deep but contains only finitely many
distinct objects and occupies only a finite amount of memory.


That is incorrect. any structure that is infinitely deep would take all of the memory that is available yet specifies an infinite amount of memory.

Nope, a tree that one branch points into itself higher up represents a tree with infinite depth, but only needs a finite amount of memory. Building such a structure may require the ability to forward declare something or reference something not yet defined.


That is counter-factual. unify_with_occurs_check determines that it would require infinite memory and then aborts its evaluation.

You misunderstand what it says. It says that it can't figure how to express the statement without a cycle. That is different then taking infinite memory. It only possibly implies infinite memory in a naive expansion, which isn't the only method.

As was pointed out, the recursive factorial definition, if naively expanded, becomes unbounded in size, but the recursive factorial definition, to a logic system that understands recursion, is usable and has meaning.

So all you have shown is that these forms CAN cause failure to some forms of naive logic.

You are just stuck in your own false thinking, and have convinced youself of a lie.



foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
"..." indicates infinite depth, thus infinite string length.

Some infinities have finite representation. You don't seem able to understand that.

Yes, some naive ways of expanding them fail, but the answer to that is you just don't do that, but need to use a less naive method.




I am trying to validate whether or not my Prolog code encodes the Liar Paradox.

That cannot be inferred from Prolog rules. Prolog defines some encodings
like how to encode numbers with characters of Prolog character set but for
more complex things you must make your own encoding rules.

Mikko


This says that G is logically equivalent to its own unprovability in F
G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.








Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Date: Sun, 1 May 2022 12:15 UTC
References: 1 2 3 4 5 6 7 8
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 07:15:14 -0500
Date: Sun, 1 May 2022 07:15:13 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<t4ljjp$4ph$1@dont-email.me> <KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>
<IWtbK.40171$JaS8.23866@fx47.iad>
<lI-dneVDd-1V7_P_nZ2dnUU7_8xh4p2d@giganews.com>
<SJubK.452730$iK66.338793@fx46.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <SJubK.452730$iK66.338793@fx46.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <x9qdneGW2YFP5PP_nZ2dnUU7_8xh4p2d@giganews.com>
Lines: 100
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-46ap22GnrcLgw+uVPfsGGNeEpzgKM4kkBfLp4u7EoOW52nStwiAfElfKVNKGhplTFft0TGpGaIhCVEh!cePg2GatAW3oVMe2Qiw//1IfTLgZPj7XnWmVomLxexbLNijQVwYwsGFEPEU/TnJEUSZstTE559c=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5423
View all headers
On 5/1/2022 7:07 AM, Richard Damon wrote:
On 5/1/22 7:45 AM, olcott wrote:
On 5/1/2022 6:12 AM, Richard Damon wrote:
On 5/1/22 6:58 AM, olcott wrote:
On 5/1/2022 4:24 AM, Mikko wrote:
On 2022-04-30 18:15:19 +0000, Aleksy Grabowski said:

I just want to add some small note.

This "not(true(_))" thing is misleading.
Please note that it is *not* a negation.
Functionally it is equivalent to:

X = foo(bar(X)).

That's correct. Prolog language does not give any inherent semantics to
data structures. It only defines the execution semantics of language
structures and standard library symbols. Those same synbols can be used
in data structures with entirely different purposes.

Mikko


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.

http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/negation.html
This is actually a superior model to convention logic in that it only seeks to prove not true, thus detects expressions of language that are simply not truth bearers.


Expressions of (formal or natural) language that can possibly be resolved to a truth value are [truth bearers].

There are only two ways that an expression of language can be resolved to a truth value:
(1) An expression of language is assigned a truth value such as "cats are animals" is defined to be true.

(2) Truth preserving operations are applied to expressions of language that are known to be true. {cats are animals} and {animals are living things} therefore {cats are living things}. Copyright 2021 PL Olcott



So you are sort of answering your own question. The model of logic that Prolog handles isn't quite the same as "conventional" logic, in part due to the way it (doesn't) define Logical Negation.

This seems to fit into your standard misunderstanding of things.

Prolog has a better model in that it can detect semantic paradoxes.
LP ↔ ¬True(LP) is correctly assessed as neither true nor false.


"Better" is as subjective word unless you define an objective criteria.

Semantically incorrect expressions of language are totally invisible to conventional logic because conventional logic incorrectly assumes that every expression is true or false. Prolog can detect expressions that are neither true nor false, thus semantically erroneous.

The fact that Prolog doesn't have the expresiability to actually write the Godel sentence, means it can't actually be used to disprove it.


This says that G is logically equivalent to its own unprovability in F
G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in Prolog.

Because
14 Every epistemological antinomy can likewise be used for a similar undecidability proof
then G ↔ ¬Provable(F, G) can likewise be used for a similar undecidability proof.

Prolog has a way to say {not provable} in its native tongue.

Misusing notations to show something is invalid logic.

I don't know Prolog well enough, but if the statement doesn't actaully mean what you want it to mean to Prolog (as others have said), then the fact that Prolog gives you the answer you want doesn't mean anything.


--
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: Sun, 1 May 2022 12:16 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!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!fx05.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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4lkro$dl6$1@dont-email.me>
<EtqdnT58XtlA8_P_nZ2dnUU7_83NnZ2d@giganews.com>
<3EubK.14817$6j9b.13866@fx36.iad>
<tqadnT2XDsz55fP_nZ2dnUU7_8xh4p2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <tqadnT2XDsz55fP_nZ2dnUU7_8xh4p2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 106
Message-ID: <uSubK.19642$aLT.14187@fx05.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: Sun, 1 May 2022 08:16:26 -0400
X-Received-Bytes: 5941
View all headers

On 5/1/22 8:09 AM, olcott wrote:
On 5/1/2022 7:01 AM, Richard Damon wrote:

On 5/1/22 7:28 AM, olcott wrote:
On 5/1/2022 4:45 AM, Mikko wrote:
On 2022-05-01 03:15:56 +0000, olcott said:

Not in this case, it is very obvious that no theorem prover can possibly prove any infinite expression.

Doesn't matter as you can't give an infinite expression to a theorem
prover.

Mikko


*You can and Prolog can detect and reject it*

Which just shows PROLOG can't handle that sort of expression, not that it logically doens't have a meaning.


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.

<inserted for clarity>
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
</inserted for clarity>

Note that, whereas they may allow you to construct something like this, most Prolog systems will not be able to write it out at the end. According to the formal definition of Unification, this kind of “infinite term” should never come to exist. Thus Prolog systems that allow a term to match an uninstantiated subterm of itself do not act correctly as Resolution theorem provers. In order to make them do so, we would have to add a check that a variable cannot be instantiated to something containing itself. Such a check, an occurs check, would be straightforward to implement, but would slow down the execution of Prolog programs considerably. Since it would only affect very few programs, most implementors have simply left it out 1.

1 The Prolog standard states that the result is undefined if a Prolog system attempts to match a term against an uninstantiated subterm of itself, which means that programs which cause this  to happen will not be portable. A portable program should ensure that wherever an occurs check might be applicable the built-in predicate unify_with_occurs_check/2 is used explicitly instead of the normal unification operation of the Prolog implementation. As its name suggests, this predicate acts like =/2 except that it fails if an occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)

Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.


So all Clocksin & Melish is saying is that such an expression fails in PROLOG, not that it doesn't have a valid logical meaning.


It correctly says that this is what the expression means:
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
Which means that it does not have a valid logical meaning.

So, factorials don't nave valid logical meaning? That is the logical conclusion of your statement since fact does the same expansion.

Shows the capability of your logic system.


The world is NOT Prolog, and I suspect Prolog isn't sufficient to handle the logic needed to process the Godel Sentence, so can't be used to disprove it.

This says that G is logically equivalent to its own unprovability in F
G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in Prolog.

"encoded in Prolog", nope, becuase G uses logic that is beyond the expression of Prolog, you have changed the meaning of the statement.

You statement even has an undefined term F.


Because
14 Every epistemological antinomy can likewise be used for a similar undecidability proof
then G ↔ ¬Provable(F, G) can likewise be used for a similar undecidability proof.


FAIL. You clearly don't understand the meaning of the words, in particular what it means to "use" something.


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Date: Sun, 1 May 2022 12:19 UTC
References: 1 2 3 4 5 6 7 8
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 07:19:39 -0500
Date: Sun, 1 May 2022 07:19:38 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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> <iLednaGFd9stPfD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4lkei$acm$1@dont-email.me> <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>
<u7ubK.20174$HLy4.14606@fx38.iad>
<i4mdnQwhosJo6fP_nZ2dnUU7_83NnZ2d@giganews.com>
<9OubK.452731$iK66.239461@fx46.iad>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <9OubK.452731$iK66.239461@fx46.iad>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <rsqdnZ_T5YtG5_P_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 128
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-gz2p2U4AJ4gS1tWE7jplOMzc/GGLQXP+G9o2Z32CrI5WzAJNMlZLS8t+KwIqNdbZA7TByTfOvtxNgeP!TxXSswzOU3+QYpvMKvUE/GtJkGfQ+6O4BS3xl7miVaf9roIxGZONEl44hke8GCXsGF0Wf3HGqr0=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5770
View all headers
On 5/1/2022 7:11 AM, Richard Damon wrote:
On 5/1/22 7:54 AM, olcott wrote:
On 5/1/2022 6:26 AM, Richard Damon wrote:
On 5/1/22 7:06 AM, olcott wrote:
On 5/1/2022 4:38 AM, Mikko wrote:
On 2022-04-30 20:48:47 +0000, olcott said:

On 4/30/2022 4:31 AM, Mikko wrote:
On 2022-04-30 07:02:23 +0000, olcott said:

LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

This is correct but to fail would also be correct.

?- unify_with_occurs_check(LP, not(true(LP))).
false.

unify_with_occurs_check must fail if the unified data structure
would contain loops.

Mikko


The above is the actual execution of actual Prolog code using
(SWI-Prolog (threaded, 64 bits, version 7.6.4).

Another Prolog implementation might interprete LP = not(true(LP)) differently
and still conform to the prolog standard.

According to Clocksin & Mellish it is not a mere loop, it is an "infinite term" thus infinitely recursive definition.

When discussing data structures, "infinite" and "loop" mean the same.
The data structure is infinitely deep but contains only finitely many
distinct objects and occupies only a finite amount of memory.


That is incorrect. any structure that is infinitely deep would take all of the memory that is available yet specifies an infinite amount of memory.

Nope, a tree that one branch points into itself higher up represents a tree with infinite depth, but only needs a finite amount of memory. Building such a structure may require the ability to forward declare something or reference something not yet defined.


That is counter-factual. unify_with_occurs_check determines that it would require infinite memory and then aborts its evaluation.

You misunderstand what it says. It says that it can't figure how to express the statement without a cycle.

The expression inherently has an infinite cycle, making it erroneous.

 That is different then taking infinite memory. It only possibly implies infinite memory in a naive expansion, which isn't the only method.

As was pointed out, the recursive factorial definition, if naively expanded, becomes unbounded in size, but the recursive factorial definition, to a logic system that understands recursion, is usable and has meaning.


Does not have an infinite cycle. It always begins with a finite integer that specifies the finite number of cycles.

So all you have shown is that these forms CAN cause failure to some forms of naive logic.


An infinite cycle is the same thing as an infinite loop inherently incorrect.

You are just stuck in your own false thinking, and have convinced youself of a lie.


You are simply ignoring key details. You are pretending that a finite thing is an infinite thing.



foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
"..." indicates infinite depth, thus infinite string length.

Some infinities have finite representation. You don't seem able to understand that.

Yes, some naive ways of expanding them fail, but the answer to that is you just don't do that, but need to use a less naive method.




I am trying to validate whether or not my Prolog code encodes the Liar Paradox.

That cannot be inferred from Prolog rules. Prolog defines some encodings
like how to encode numbers with characters of Prolog character set but for
more complex things you must make your own encoding rules.

Mikko


This says that G is logically equivalent to its own unprovability in F
G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded 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: Mr Flibble
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Jupiter Mining Corp
Date: Sun, 1 May 2022 12:19 UTC
References: 1 2 3 4 5 6 7 8 9 10
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!npeer.as286.net!npeer-ng0.as286.net!peer02.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!fx02.ams4.POSTED!not-for-mail
From: flib...@reddwarf.jmc (Mr Flibble)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Message-ID: <20220501131951.00000889@reddwarf.jmc>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
<t4l5hq$8bi$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=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Lines: 130
X-Complaints-To: abuse@eweka.nl
NNTP-Posting-Date: Sun, 01 May 2022 12:19:51 UTC
Date: Sun, 1 May 2022 13:19:51 +0100
X-Received-Bytes: 6526
View all headers
On Sat, 30 Apr 2022 23:24:05 -0600
Jeff Barnett <jbb@notatt.com> wrote:

On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote: 
On 4/30/22 10:56 PM, olcott wrote: 
On 4/30/2022 9:38 PM, Richard Damon wrote: 
On 4/30/22 10:21 PM, olcott wrote: 
On 4/30/2022 9:00 PM, Richard Damon wrote: 
On 4/30/22 9:42 PM, olcott wrote: 
On 4/30/2022 8:08 PM, Richard Damon wrote: 
On 4/30/22 3:02 AM, olcott wrote: 
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence


 

Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the
results is correct.

All that false means is that the statement


LP = not(true(LP))

is recursive and that Prolog can't actually evaluate it due
to its limited logic rules.
 

That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies
infinitely nested definition like this: 

No, that IS what they say, that this sort of recursion fails
the test of Unification, not that it is has no possible
logical meaning.

Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning
systems.

Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.

Note, for instance, at least some ways of writing factorial
for an unknown value can lead to an infinite expansion, but
the factorial is well defined for all positive integers. The
fact that a "prolog like" expansion operator might not be able
to handle the definition, doesn't mean it doesn't have meaning.
 

It is really dumb that you continue to take wild guesses again
the verified facts.

Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
 

I did. You just don't seem to understand what I am saying
because it is above your head.

Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of
those statements (a useful subset, but a subset).

The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog. 
In this case it does. I have spent thousands of hours on the
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of
Clocksin & Mellish does not count as reading it. 

And it appears that you don't understand it, because you still
make category errors when trying to talk about it.
 

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)

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
 

Right. but some infinite structures might actually have meaning.  
Not in this case, it is very obvious that no theorem prover can
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop. 

Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.

Just like:

Fact(n) := (N == 1) ? 1 : N*Fact(n-1);

Are you mental? That definition isn't infinitely recursive as it
terminates when N equals 1 given a set of constraints on N (positive
integer greater or equal to 1).

/Flibble



Subject: Re: Is this correct Prolog?
From: polcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: A noiseless patient Spider
Date: Sun, 1 May 2022 12:51 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 (polcott)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Date: Sun, 1 May 2022 07:51:44 -0500
Organization: A noiseless patient Spider
Lines: 135
Message-ID: <t4lvp1$vr7$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4l5hq$8bi$1@dont-email.me>
<20220501131951.00000889@reddwarf.jmc>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 May 2022 12:51:45 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="c2520d0307b0b198e014f96ec09ab41a";
logging-data="32615"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19Nkg6qq92Y5DAE4uaiIk+h"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:8U/eaoyQUt2hziIqORVrl0GYumA=
In-Reply-To: <20220501131951.00000889@reddwarf.jmc>
Content-Language: en-US
View all headers
On 5/1/2022 7:19 AM, Mr Flibble wrote:
On Sat, 30 Apr 2022 23:24:05 -0600
Jeff Barnett <jbb@notatt.com> wrote:

On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence


 

Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the
results is correct.

All that false means is that the statement


LP = not(true(LP))

is recursive and that Prolog can't actually evaluate it due
to its limited logic rules.
 

That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies
infinitely nested definition like this:

No, that IS what they say, that this sort of recursion fails
the test of Unification, not that it is has no possible
logical meaning.

Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning
systems.

Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.

Note, for instance, at least some ways of writing factorial
for an unknown value can lead to an infinite expansion, but
the factorial is well defined for all positive integers. The
fact that a "prolog like" expansion operator might not be able
to handle the definition, doesn't mean it doesn't have meaning.
 

It is really dumb that you continue to take wild guesses again
the verified facts.

Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
 

I did. You just don't seem to understand what I am saying
because it is above your head.

Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of
those statements (a useful subset, but a subset).

The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
In this case it does. I have spent thousands of hours on the
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of
Clocksin & Mellish does not count as reading it.

And it appears that you don't understand it, because you still
make category errors when trying to talk about it.
 

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)

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
 

Right. but some infinite structures might actually have meaning.
Not in this case, it is very obvious that no theorem prover can
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.

Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.

Just like:

Fact(n) := (N == 1) ? 1 : N*Fact(n-1);

Are you mental? That definition isn't infinitely recursive as it
terminates when N equals 1 given a set of constraints on N (positive
integer greater or equal to 1).

/Flibble


Brilliantly well put.

--
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
Date: Sun, 1 May 2022 16:08 UTC
References: 1 2 3 4 5 6 7 8
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 11:08:56 -0500
Date: Sun, 1 May 2022 11:08:55 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4m2b2$kmn$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com>
Lines: 101
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-6C9k6uUVYzVZ7mERy32y++p50vD/67dZALJRjnDPEKLc3UrZjCmlTVAFj53Z2oQsbGuuoCQzW0k0BIH!KmZ5gI6si66lnhaW1TZeYzX3Sg8vpkhv47fUAppBIPFgx/tY51sxyLFzNHidHQ+jRqqSmPXKiTA=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4933
View all headers
On 5/1/2022 8:35 AM, André G. Isaak wrote:
On 2022-05-01 05:40, olcott wrote:
On 5/1/2022 12:34 AM, André G. Isaak wrote:
On 2022-04-30 22:49, olcott wrote:
On 4/30/2022 8:53 PM, André G. Isaak wrote:
On 2022-04-30 19:47, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

Since it isn't giving you a "syntax error", it is probably correct Prolog. Not sure if your interpretation of the results is correct.

I asked the question incorrectly, what I really needed to know is whether or not the Prolog correctly encodes this logic sentence:
LP := ~True(LP)

Since that isn't a 'logic sentence', no one can answer this.

André



What about this one?
LP ↔ ¬True(LP)  // Tarski uses something like this

That requires that you define some predicate 'True'. Presumably True(LP) must mean something other than LP or it would be purely redundant.


For the purpose of verifying that it is semantically incorrect True() can simply be an empty placeholder. The result is that no matter how True() is defined the above logic sentence is semantically incorrect.

You're missing my point. Unless you are claiming that there is a difference between 'x if and only if y' and 'x is true if and only if y is true', then there is no reason for such a predicate at all. The fact that you insist on including it suggests you *do* think there is a difference in meaning between these two examples. So what is that difference?

But whatever it means, LP ↔ ¬True(LP) is either simply true or simply false. It is *not* the liar paradox. Most likely it is simply false since I assume LP ↔ ¬True(LP) is simply the same as LP ↔ ¬LP.

LP ↔ ¬LP

is simply false. It is not a translation of 'This sentence is false'.

https://liarparadox.org/Tarski_275_276.pdf

or this one?
G ↔ ¬(F ⊢ G)

As a statement of logic, no. As a statement in the metalanguage of logic, sure. As a paraphrase of Gödel, not exactly.


G ↔ ¬Provable(F, G)

If you want to paraphrase Gödel, you need both G and ⌈G⌉ to be present in your statement.

André



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

G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is necessarily sufficient.

Likewise with this one: LP ↔ ¬True(LP)
It can be evaluated as semantically incorrect without the need to define True(). No matter how True() is defined LP ↔ ¬True(LP) is 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: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Date: Sun, 1 May 2022 16:57 UTC
References: 1 2 3 4 5 6 7 8 9 10
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 11:57:51 -0500
Date: Sun, 1 May 2022 11:57:49 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<t4malm$ned$1@dont-email.me> <t4mbmf$lu$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4mbmf$lu$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <FdSdnWmjBKmSIfP_nZ2dnUU7_8zNnZ2d@giganews.com>
Lines: 185
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-jYNSydnrZcARmyDE9jJRVJN/+hrya4JGESIjRuCrBp/KxcbMyYBQYGxGGgF0As18YyFVt8Tl5p3BjP9!eMyuj+nWEH2pKaIAfOf2w2hLzMxBeOZnToY/hjiks8iY8K7e8V3oTndwq3z7p7mCS0VCZvEvKms=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 7755
View all headers
On 5/1/2022 11:15 AM, André G. Isaak wrote:
On 2022-05-01 09:57, polcott wrote:
On 5/1/2022 8:35 AM, André G. Isaak wrote:
On 2022-05-01 05:40, olcott wrote:
On 5/1/2022 12:34 AM, André G. Isaak wrote:
On 2022-04-30 22:49, olcott wrote:
On 4/30/2022 8:53 PM, André G. Isaak wrote:
On 2022-04-30 19:47, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

Since it isn't giving you a "syntax error", it is probably correct Prolog. Not sure if your interpretation of the results is correct.

I asked the question incorrectly, what I really needed to know is whether or not the Prolog correctly encodes this logic sentence:
LP := ~True(LP)

Since that isn't a 'logic sentence', no one can answer this.

André



What about this one?
LP ↔ ¬True(LP)  // Tarski uses something like this

That requires that you define some predicate 'True'. Presumably True(LP) must mean something other than LP or it would be purely redundant.


For the purpose of verifying that it is semantically incorrect True() can simply be an empty placeholder. The result is that no matter how True() is defined the above logic sentence is semantically incorrect.

You're missing my point. Unless you are claiming that there is a difference between 'x if and only if y' and 'x is true if and only if y is true', then there is no reason for such a predicate at all. The fact that you insist on including it suggests you *do* think there is a difference in meaning between these two examples. So what is that difference?

But whatever it means, LP ↔ ¬True(LP) is either simply true or simply false. It is *not* the liar paradox. Most likely it is simply false since I assume LP ↔ ¬True(LP) is simply the same as LP ↔ ¬LP.

LP ↔ ¬LP

is simply false. It is not a translation of 'This sentence is false'.

https://liarparadox.org/Tarski_275_276.pdf

or this one?
G ↔ ¬(F ⊢ G)

As a statement of logic, no. As a statement in the metalanguage of logic, sure. As a paraphrase of Gödel, not exactly.


G ↔ ¬Provable(F, G)

If you want to paraphrase Gödel, you need both G and ⌈G⌉ to be present in your statement.

André


That it not what this says:
14 Every epistemological antinomy can likewise be used for a similar undecidability proof

That footnote says absolutely nothing about how to formalize Gödel's Theorem.


It says that Every epistemological antinomy can likewise be used for a similar undecidability proof

thus even English epistemological antinomies such as the Liar antinomy can be used.

Gödel says:
"There is also a close relationship with the “liar” antinomy"

G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is necessarily sufficient.

There is no antinomy involved in that formula, epistemological or otherwise.


Prolog disagrees.
To boil the Gödel proof down to its bare essence we use the simplest Liar epistemological antinomy: LP ↔ ¬True(LP)

This way we don't need dozens pages of hundreds of formulas and Prolog is smart enough to detect and reject it as erroneous.

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

False means that LP ↔ ¬True(LP) specifies: ¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(...))))))))))

(SWI-Prolog (threaded, 64 bits, version 7.6.4)


If you wish to know how to best formalize Gödel, simply read Gödel; he provides the proper formalization for you.

Likewise with this one: LP ↔ ¬True(LP)
It can be evaluated as semantically incorrect without the need to define True(). No matter how True() is defined LP ↔ ¬True(LP) is semantically incorrect.

There's nothing 'semantically incorrect' about it. It evaluates to false. It's not the Liar's Paradox.


?- unify_with_occurs_check(LP, not(true(LP))).
false.

false means that LP ↔ ¬True(LP) specifies: ¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(...))))))))))

The reason I keep asking you to define your 'True' predicate is simply that it seems utterly unnecessary and pointless.

Any logic sentence having the self-referential form of the Liar Paradox specifies infinitely recursive definition, thus is semantically incorrect.

 From Clocksin and Mellish:
equal(X, X).?-
equal(foo(Y), Y).

specifies:
foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))


If you believe otherwise, then please explain what the difference between the following formulae might possibly be:


I never waste time carefully examining every possible permutation of an idea because this would guarantee that I am dead long before my proof is complete. That I have proved my point with one is them is entirely sufficient. My example corresponds to the definitive example provided by the worlds best experts on the Prolog language.

(1) LP ↔ ¬True(LP)
(2) True(LP) ↔ ¬True(LP)
(3) LP ↔ ¬LP
(4) True(LP) ↔ ¬LP

André



--
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.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Forte - www.forteinc.com
Date: Sun, 1 May 2022 17:16 UTC
References: 1 2 3 4 5 6 7 8 9 10 11
Path: i2pn2.org!i2pn.org!aioe.org!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!fx48.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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4l5hq$8bi$1@dont-email.me>
<_v2dnUiL-Yjh7fP_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <_v2dnUiL-Yjh7fP_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 210
Message-ID: <tfzbK.388022$f2a5.287279@fx48.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: Sun, 1 May 2022 13:16:11 -0400
X-Received-Bytes: 10954
View all headers
On 5/1/22 7:35 AM, olcott wrote:
On 5/1/2022 12:24 AM, Jeff Barnett wrote:
On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

Since it isn't giving you a "syntax error", it is probably correct Prolog. Not sure if your interpretation of the results is correct.

All that false means is that the statement


LP = not(true(LP))

is recursive and that Prolog can't actually evaluate it due to its limited logic rules.


That is not what Clocksin & Mellish says. They say it is an erroneous "infinite term" meaning that it specifies infinitely nested definition like this:

No, that IS what they say, that this sort of recursion fails the test of Unification, not that it is has no possible logical meaning.

Prolog represents a somewhat basic form of logic, useful for many cases, but not encompassing all possible reasoning systems.

Maybe it can handle every one that YOU can understand, but it can't handle many higher order logical structures.

Note, for instance, at least some ways of writing factorial for an unknown value can lead to an infinite expansion, but the factorial is well defined for all positive integers. The fact that a "prolog like" expansion operator might not be able to handle the definition, doesn't mean it doesn't have meaning.


It is really dumb that you continue to take wild guesses again the verified facts.

Please read the Clocksin & Mellish (on page 3 of my paper) text and eliminate your ignorance.


I did. You just don't seem to understand what I am saying because it is above your head.

Prolog is NOT the defining authority for what is a valid logical statement, but a system of programming to handle a subset of those statements (a useful subset, but a subset).

The fact that Prolog doesn't allow something doesn't mean it doesn't have a logical meaning, only that it doesn't have a logical meaning in Prolog.
In this case it does. I have spent thousands of hours on the semantic error of infinitely recursive definition and written a dozen papers on it. Glancing at one of two of the words of Clocksin & Mellish does not count as reading it.

And it appears that you don't understand it, because you still make category errors when trying to talk about it.


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)

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))

Right. but some infinite structures might actually have meaning.
Not in this case, it is very obvious that no theorem prover can possibly prove any infinite expression. It is the same thing as a program that is stuck in an infinite loop.

Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The fact that Prolog uses certain limited method to figure out meaning doesn't mean that other methods can't find the meaning.


The question is not whether some infinite structures have meaning that is the dishonest dodge of the strawman error.

The question is whether on not the expression at hand has meaning or is simply semantically incoherent. I just posted all of the Clocksin & Mellish text in my prior post to make this more clear.


This example expanded from Clocksin & Mellish conclusively proves that some expressions of language are incorrect:

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))

No, not "incorrect", just "can't be handled by Prolog".

If foo is my fact() function, it is definitely "defined".


Just like:

Fact(n) := (N == 1) ? 1 : N*Fact(n-1);

if naively expanded has an infinite expansion.

But, based on mathematical knowledge, and can actually be proven from the definition, something like Fact(n+1)/fact(n), even for an unknown n, can be reduced without the need to actually expend infinite operations.

Note, this is actual shown in your case of H(H^,H^). Yes, if H doesn't abort its simulation, then for THAT H^, we have that H^(H^) is non-halting, but so is H(H^,H^), and thus THAT H / H^ pair fails to be a counter example

When you program H to abort its simulation of H^ at some point, and build your H^ on that H, then H(H^,H^), will return the non-halting answer, and H^(H^) when PROPERLY run or simulated halts, because H has the same "cut off" logic at the factorial above.

The naive expansion thinks it is infinite, but the correct expansion sees the cut off and sees that it is actually finite.
----------------------------------------------------------------------

A good symbolic manipulation system or a theorem prover with appropriate axioms and rules of inference could surely handle forms such as Fact(n+1)/fact(n) without breathing hard. It is only you, an ignorant fool, who seems to think that the unthinking infinite unrolling of a form must occur. Only you would think that a solver system would completely unroll a form before analyzing it and applying transformations to it.

Son, it don't work that way (unless you are defining and making a mess trying to write the system yourself). Systems usually have rules that make small incremental transformations and usually search breadth first with perhaps a limited amount of depth first interludes. If they don't use a breadth first strategy, they will not be able to claim the completeness property. (See resolution theorem prover literature for some explanation. You wont understand it but you can cite as if you did!)

Richard was trying to explain this to you in the snipped portion I recited just above. Question for Peter holding his pecker: How do you always and I mean always manage to delete the part of a message you respond too that addresses the point you now try to make?

A typically subsequence you might see in the trace: would include in order but not necessarily consecutively:
    Fact(n+1)/Fact(n)
    (n+1)*Fact(n)/Fact(n)
    (n+1)
Some interspersed terms such as Fact(n+1)/(n*Fact(n-1)) would be found too. In some circumstances, these other terms might be helpful. A theorem prover or manipulator does all of this, breadth first, hoping to blindly stumble on a solution. You can provide heuristics that might speed up the process but no advice short of an oracle will get you even one more result. (Another manifestation of HP.) It's the slow grinding through the possibilities that guarantees that if a result can be found, it will be found. And all the theory that you don't understand says that's the best you can do.

Ben and I disagree on reasons for your type of total dishonesty. He thinks that you are so self deluded that you actual believe what you are saying; that you are so self deluded that the dishonest utterances are just your subconscious protecting your already damaged ego. To that, I say phooey; you are just a long term troll who lies a lot about math, about your history and health, and about your accomplishments.

I don't believe that you will read this before you start to respond but that's okay. Understanding is not required. Neither is respect in either direction.





Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Forte - www.forteinc.com
Date: Sun, 1 May 2022 17:19 UTC
References: 1 2 3 4 5 6 7 8 9 10 11
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!ecngs!feeder2.ecngs.de!178.20.174.213.MISMATCH!feeder1.feed.usenet.farm!feed.usenet.farm!peer03.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx08.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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4l5hq$8bi$1@dont-email.me>
<20220501131951.00000889@reddwarf.jmc>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <20220501131951.00000889@reddwarf.jmc>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 138
Message-ID: <0jzbK.10506$_Ol4.1836@fx08.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: Sun, 1 May 2022 13:19:57 -0400
X-Received-Bytes: 7073
View all headers
On 5/1/22 8:19 AM, Mr Flibble wrote:
On Sat, 30 Apr 2022 23:24:05 -0600
Jeff Barnett <jbb@notatt.com> wrote:

On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence


 

Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the
results is correct.

All that false means is that the statement


LP = not(true(LP))

is recursive and that Prolog can't actually evaluate it due
to its limited logic rules.
 

That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies
infinitely nested definition like this:

No, that IS what they say, that this sort of recursion fails
the test of Unification, not that it is has no possible
logical meaning.

Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning
systems.

Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.

Note, for instance, at least some ways of writing factorial
for an unknown value can lead to an infinite expansion, but
the factorial is well defined for all positive integers. The
fact that a "prolog like" expansion operator might not be able
to handle the definition, doesn't mean it doesn't have meaning.
 

It is really dumb that you continue to take wild guesses again
the verified facts.

Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
 

I did. You just don't seem to understand what I am saying
because it is above your head.

Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of
those statements (a useful subset, but a subset).

The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
In this case it does. I have spent thousands of hours on the
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of
Clocksin & Mellish does not count as reading it.

And it appears that you don't understand it, because you still
make category errors when trying to talk about it.
 

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)

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
 

Right. but some infinite structures might actually have meaning.
Not in this case, it is very obvious that no theorem prover can
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.

Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.

Just like:

Fact(n) := (N == 1) ? 1 : N*Fact(n-1);

Are you mental? That definition isn't infinitely recursive as it
terminates when N equals 1 given a set of constraints on N (positive
integer greater or equal to 1).

/Flibble


But if you don't know N, you don't know when to terminate the expansion.

If all you know is that N is a positive integer, then you don't know when to stop.

That is the issue, Fact of N isn't just defined for know values of N, but you can do logic with unknow values (and especially with multiple instances of Fact with related parameters).


Subject: Re: Is this correct Prolog?
From: André G. Isaak
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Christians and Atheists United Against Creeping Agnosticism
Date: Sun, 1 May 2022 17:21 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: agis...@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Date: Sun, 1 May 2022 11:21:53 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 93
Message-ID: <t4mfjj$tr$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<t4malm$ned$1@dont-email.me> <t4mbmf$lu$1@dont-email.me>
<FdSdnWmjBKmSIfP_nZ2dnUU7_8zNnZ2d@giganews.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 May 2022 17:21:55 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="9aade08aa0eb94cd9b9879b12c2d9c29";
logging-data="955"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19rfguuBhfuUVu2FSU07vH3"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:6xY5rdWGdIeJjb9G7M2+k1kX6PE=
In-Reply-To: <FdSdnWmjBKmSIfP_nZ2dnUU7_8zNnZ2d@giganews.com>
Content-Language: en-US
View all headers
On 2022-05-01 10:57, olcott wrote:
On 5/1/2022 11:15 AM, André G. Isaak wrote:
On 2022-05-01 09:57, polcott wrote:

It says that Every epistemological antinomy can likewise be used for a similar undecidability proof

thus even English epistemological antinomies such as the Liar antinomy can be used.

Gödel says:
"There is also a close relationship with the “liar” antinomy"

Yes. There is a close *relationship* between his G and The Liar. That does *not* mean that G *is* The Liar. It is not. But you refuse to read Gödel's actual math to see the *very* significant differences between the two.

Similarly one can construct sentences which bear a close relationship to other antinomies. Again, that does not mean those sentences *are* those antinomies.

You need to stop trying to analyze Gödel's footnotes as if this were some exercise in literary analysis and focus on the actual math.

G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is necessarily sufficient.

There is no antinomy involved in that formula, epistemological or otherwise.


Prolog disagrees.
To boil the Gödel proof down to its bare essence we use the simplest Liar epistemological antinomy: LP ↔ ¬True(LP)

Again, that formula is not The Liar. That says that LP is true if and only if LP is not true. Even a simple truth table suffices to show that this statement is false. There is no self-reference involved in that formula, and the self-reference is the key to The Liar.

This way we don't need dozens pages of hundreds of formulas and Prolog is smart enough to detect and reject it as erroneous.

Whether Prolog likes something or not is irrelevant. Prolog can't even deal with first order logic, let alone higher order logic. Prolog deals with Horn clauses. It is a very simple system designed to deal with very simple proofs. It's the wrong tool for dealing with substantive theorems of math or logic.

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Where in the above have you encoded the ↔ ?

As I note above, what Prolog has to say isn't particularly relevant, but it is even *less* relevant if your Prolog doesn't even encode the formula you're talking about.

<snip more junk about Prolog>


If you believe otherwise, then please explain what the difference between the following formulae might possibly be:


I never waste time carefully examining every possible permutation of an idea because this would guarantee that I am dead long before my proof is complete. That I have proved my point with one is them is entirely sufficient. My example corresponds to the definitive example provided by the worlds best experts on the Prolog language.

This is a really simple question. It should consume no time at all. Let me phrase my question in a more direct way: All I am asking is for you to clarify whether your True() predicate is anything other than syntactic sugar.

In logic an expression X evaluates to true if X is true. So True(X) and X would seem to be identical. So why bother with this predicate at all?

(1) LP ↔ ¬True(LP)
(2) True(LP) ↔ ¬True(LP)
(3) LP ↔ ¬LP
(4) True(LP) ↔ ¬LP

André

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


Subject: Re: Is this correct Prolog?
From: Jeff Barnett
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: A noiseless patient Spider
Date: Sun, 1 May 2022 17:22 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: jbb...@notatt.com (Jeff Barnett)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Date: Sun, 1 May 2022 11:22:22 -0600
Organization: A noiseless patient Spider
Lines: 115
Message-ID: <t4mfkg$185$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com> <t4l5hq$8bi$1@dont-email.me>
<20220501131951.00000889@reddwarf.jmc>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: base64
Injection-Date: Sun, 1 May 2022 17:22:25 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="dfa4a43240a45544272de93b7ef2f48d";
logging-data="1285"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18bVCmF76vAO5gg5hQFwDufkMN1TuT59bw="
User-Agent: Mozilla/5.0 (Windows NT 6.1; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Cancel-Lock: sha1:C3AlKjsSUpXsVBd6SuuVCrnXaw4=
In-Reply-To: <20220501131951.00000889@reddwarf.jmc>
Content-Language: en-US
View all headers
On 5/1/2022 6:19 AM, Mr Flibble wrote:
On Sat, 30 Apr 2022 23:24:05 -0600
Jeff Barnett <jbb@notatt.com> wrote:

On 4/30/2022 9:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence


 

Since it isn't giving you a "syntax error", it is probably
correct Prolog. Not sure if your interpretation of the
results is correct.

All that false means is that the statement


LP = not(true(LP))

is recursive and that Prolog can't actually evaluate it due
to its limited logic rules.
 

That is not what Clocksin & Mellish says. They say it is an
erroneous "infinite term" meaning that it specifies
infinitely nested definition like this:

No, that IS what they say, that this sort of recursion fails
the test of Unification, not that it is has no possible
logical meaning.

Prolog represents a somewhat basic form of logic, useful for
many cases, but not encompassing all possible reasoning
systems.

Maybe it can handle every one that YOU can understand, but it
can't handle many higher order logical structures.

Note, for instance, at least some ways of writing factorial
for an unknown value can lead to an infinite expansion, but
the factorial is well defined for all positive integers. The
fact that a "prolog like" expansion operator might not be able
to handle the definition, doesn't mean it doesn't have meaning.
 

It is really dumb that you continue to take wild guesses again
the verified facts.

Please read the Clocksin & Mellish (on page 3 of my paper) text
and eliminate your ignorance.
 

I did. You just don't seem to understand what I am saying
because it is above your head.

Prolog is NOT the defining authority for what is a valid logical
statement, but a system of programming to handle a subset of
those statements (a useful subset, but a subset).

The fact that Prolog doesn't allow something doesn't mean it
doesn't have a logical meaning, only that it doesn't have a
logical meaning in Prolog.
In this case it does. I have spent thousands of hours on the
semantic error of infinitely recursive definition and written a
dozen papers on it. Glancing at one of two of the words of
Clocksin & Mellish does not count as reading it.

And it appears that you don't understand it, because you still
make category errors when trying to talk about it.
 

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)

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))
 

Right. but some infinite structures might actually have meaning.
Not in this case, it is very obvious that no theorem prover can
possibly prove any infinite expression. It is the same thing as a
program that is stuck in an infinite loop.

Richard wrote and the asshole (PO) snipped
------------------------------------------
Right. but some infinite structures might actually have meaning. The
fact that Prolog uses certain limited method to figure out meaning
doesn't mean that other methods can't find the meaning.

Just like:

Fact(n) := (N == 1) ? 1 : N*Fact(n-1);

I see that you, like the asshole, are snipping too. there was another
line just above: "if naively expanded has an infinite expansion." That
was the context of my remarks.

Also note that there isn't anything left that I wrote (other than the
partial quote of someone else above). So what does your remark apply to?
Your contribution sounds like a wounded Parrot squawking in the night. A
horrible sound, especially when trying to imitate human communications.

Are you mental? That definition isn't infinitely recursive as it
terminates when N equals 1 given a set of constraints on N (positive
integer greater or equal to 1).
I take this as a sign that you might have a glimmer of understanding;
otherwise, why snip that particular line above? Ah! We know an other
jerk trolling for sport. I must say though, that I'm not ready to
upgrade you from ignoramus just yet - this was your first and only
visible sign of sentience so far. I'll reconsider if I see others.
--
Jeff Barnett


Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Forte - www.forteinc.com
Date: Sun, 1 May 2022 17:26 UTC
References: 1 2 3 4 5 6 7 8 9 10 11
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.uzoreto.com!newsfeed.xs4all.nl!newsfeed8.news.xs4all.nl!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx33.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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<3_OdnbuxKP_vePD_nZ2dnUU7_83NnZ2d@giganews.com>
<AQlbK.11129$lX6b.2320@fx33.iad>
<39adnR-AIvg5c_D_nZ2dnUU7_81g4p2d@giganews.com>
<uombK.379436$Gojc.287190@fx99.iad>
<pPSdnSU56NRla_D_nZ2dnUU7_8zNnZ2d@giganews.com>
<VTmbK.655548$mF2.416033@fx11.iad>
<Apidnc59pLnwZvD_nZ2dnUU7_8zNnZ2d@giganews.com>
<10ubK.688746$LN2.71023@fx13.iad>
<npSdnachY_1p7vP_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <npSdnachY_1p7vP_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 148
Message-ID: <OozbK.11131$lX6b.4393@fx33.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: Sun, 1 May 2022 13:26:08 -0400
X-Received-Bytes: 7779
View all headers
On 5/1/22 7:50 AM, olcott wrote:
On 5/1/2022 6:18 AM, Richard Damon wrote:
On 4/30/22 11:15 PM, olcott wrote:
On 4/30/2022 10:11 PM, Richard Damon wrote:
On 4/30/22 10:56 PM, olcott wrote:
On 4/30/2022 9:38 PM, Richard Damon wrote:
On 4/30/22 10:21 PM, olcott wrote:
On 4/30/2022 9:00 PM, Richard Damon wrote:
On 4/30/22 9:42 PM, olcott wrote:
On 4/30/2022 8:08 PM, Richard Damon wrote:
On 4/30/22 3:02 AM, olcott wrote:
LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

(SWI-Prolog (threaded, 64 bits, version 7.6.4)

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence

Since it isn't giving you a "syntax error", it is probably correct Prolog. Not sure if your interpretation of the results is correct.

All that false means is that the statement


LP = not(true(LP))

is recursive and that Prolog can't actually evaluate it due to its limited logic rules.


That is not what Clocksin & Mellish says. They say it is an erroneous "infinite term" meaning that it specifies infinitely nested definition like this:

No, that IS what they say, that this sort of recursion fails the test of Unification, not that it is has no possible logical meaning.

Prolog represents a somewhat basic form of logic, useful for many cases, but not encompassing all possible reasoning systems.

Maybe it can handle every one that YOU can understand, but it can't handle many higher order logical structures.

Note, for instance, at least some ways of writing factorial for an unknown value can lead to an infinite expansion, but the factorial is well defined for all positive integers. The fact that a "prolog like" expansion operator might not be able to handle the definition, doesn't mean it doesn't have meaning.


It is really dumb that you continue to take wild guesses again the verified facts.

Please read the Clocksin & Mellish (on page 3 of my paper) text and eliminate your ignorance.


I did. You just don't seem to understand what I am saying because it is above your head.

Prolog is NOT the defining authority for what is a valid logical statement, but a system of programming to handle a subset of those statements (a useful subset, but a subset).

The fact that Prolog doesn't allow something doesn't mean it doesn't have a logical meaning, only that it doesn't have a logical meaning in Prolog.
In this case it does. I have spent thousands of hours on the semantic error of infinitely recursive definition and written a dozen papers on it. Glancing at one of two of the words of Clocksin & Mellish does not count as reading it.

And it appears that you don't understand it, because you still make category errors when trying to talk about it.


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)

foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))))))

Right. but some infinite structures might actually have meaning.
Not in this case, it is very obvious that no theorem prover can possibly prove any infinite expression. It is the same thing as a program that is stuck in an infinite loop.


As Jeff pointed out, your claim is shown false, that some statements with infinite expansions can be worked with by some automatic solvers.

That is the dishonest dodge of the strawman error. The particular expression at hand is inherently incorrect and thus any system that proves it is a broken system.

This just proves that you don't really understand the effects of "recursion" and "self-reference", and perhaps a source of your error in trying to reason about thing like this Halting Problem proof or Godels Incompleteness Theory and his expression "G".


foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
The "..." indicates infinite expansion, thus this expression can never be proved by any system.

You think? depends on what you know about the definition of foo.

Perhaps you can't do anything with the infinitely expanded version, since you can't actually express it, but the self-referential version might be able to be analyzed.

You problem is you seem to think if YOU can't understand it, it doesn't have meaning, but that is NOT an actual fact. There seems to be MANY things that you do not understand that are actually well established. Maybe you need to get off your incorrect assumption that you are the source of Truth.


If something that is obviously undoable is your mind is shown to be in fact doable, the problem isn't in the ability to do it, but in the ability of your mind to understand. Your misconceptions don't change the nature of reality, but reality proves you wrong.





Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Sun, 1 May 2022 17:49 UTC
References: 1 2 3 4 5 6 7 8 9
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.mixmin.net!npeer.as286.net!npeer-ng0.as286.net!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx02.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>
<t4ljjp$4ph$1@dont-email.me> <KtadnUZsIcRP-vP_nZ2dnUU7_8zNnZ2d@giganews.com>
<IWtbK.40171$JaS8.23866@fx47.iad>
<lI-dneVDd-1V7_P_nZ2dnUU7_8xh4p2d@giganews.com>
<SJubK.452730$iK66.338793@fx46.iad>
<x9qdneGW2YFP5PP_nZ2dnUU7_8xh4p2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <x9qdneGW2YFP5PP_nZ2dnUU7_8xh4p2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 115
Message-ID: <UKzbK.2223$IQK.135@fx02.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: Sun, 1 May 2022 13:49:41 -0400
X-Received-Bytes: 5871
View all headers
On 5/1/22 8:15 AM, olcott wrote:
On 5/1/2022 7:07 AM, Richard Damon wrote:
On 5/1/22 7:45 AM, olcott wrote:
On 5/1/2022 6:12 AM, Richard Damon wrote:
On 5/1/22 6:58 AM, olcott wrote:
On 5/1/2022 4:24 AM, Mikko wrote:
On 2022-04-30 18:15:19 +0000, Aleksy Grabowski said:

I just want to add some small note.

This "not(true(_))" thing is misleading.
Please note that it is *not* a negation.
Functionally it is equivalent to:

X = foo(bar(X)).

That's correct. Prolog language does not give any inherent semantics to
data structures. It only defines the execution semantics of language
structures and standard library symbols. Those same synbols can be used
in data structures with entirely different purposes.

Mikko


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.

http://www.cse.unsw.edu.au/~billw/dictionaries/prolog/negation.html
This is actually a superior model to convention logic in that it only seeks to prove not true, thus detects expressions of language that are simply not truth bearers.


Expressions of (formal or natural) language that can possibly be resolved to a truth value are [truth bearers].

There are only two ways that an expression of language can be resolved to a truth value:
(1) An expression of language is assigned a truth value such as "cats are animals" is defined to be true.

(2) Truth preserving operations are applied to expressions of language that are known to be true. {cats are animals} and {animals are living things} therefore {cats are living things}. Copyright 2021 PL Olcott



So you are sort of answering your own question. The model of logic that Prolog handles isn't quite the same as "conventional" logic, in part due to the way it (doesn't) define Logical Negation.

This seems to fit into your standard misunderstanding of things.

Prolog has a better model in that it can detect semantic paradoxes.
LP ↔ ¬True(LP) is correctly assessed as neither true nor false.


"Better" is as subjective word unless you define an objective criteria.

Semantically incorrect expressions of language are totally invisible to conventional logic because conventional logic incorrectly assumes that every expression is true or false. Prolog can detect expressions that are neither true nor false, thus semantically erroneous.

Incorrect, conventional logic understand that some statements are not truth bearers. Now, a lot of rules are pre-conditioned on the assumption that their inputs ARE truth bearers, so you need to be careful in just applying rules to statements that they do not apply to.


The fact that Prolog doesn't have the expresiability to actually write the Godel sentence, means it can't actually be used to disprove it.


This says that G is logically equivalent to its own unprovability in F
G ↔ ¬Provable(F, G) and fails unify_with_occurs_check when encoded in Prolog.

No, that is NOT what G says.


Because
14 Every epistemological antinomy can likewise be used for a similar undecidability proof
then G ↔ ¬Provable(F, G) can likewise be used for a similar undecidability proof.

except that isn't G, so you are just starting from a false start, so your logic doesn't mean anything (not that much of your logic ever means anything because this seems a common error, you assume things that just are not).


Prolog has a way to say {not provable} in its native tongue.

Fine, but can it express the statement that Godel's G actually is, not your over-simplification is.


Misusing notations to show something is invalid logic.

I don't know Prolog well enough, but if the statement doesn't actaully mean what you want it to mean to Prolog (as others have said), then the fact that Prolog gives you the answer you want doesn't mean anything.





Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.lang.prolog, comp.theory, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Sun, 1 May 2022 18:00 UTC
References: 1 2 3 4 5 6 7 8 9
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!npeer.as286.net!npeer-ng0.as286.net!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx10.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> <iLednaGFd9stPfD_nZ2dnUU7_83NnZ2d@giganews.com>
<t4lkei$acm$1@dont-email.me> <IZCdnYlY2qst9PP_nZ2dnUU7_81g4p2d@giganews.com>
<u7ubK.20174$HLy4.14606@fx38.iad>
<i4mdnQwhosJo6fP_nZ2dnUU7_83NnZ2d@giganews.com>
<9OubK.452731$iK66.239461@fx46.iad>
<rsqdnZ_T5YtG5_P_nZ2dnUU7_83NnZ2d@giganews.com>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <rsqdnZ_T5YtG5_P_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 161
Message-ID: <lVzbK.816079$oF2.372227@fx10.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: Sun, 1 May 2022 14:00:50 -0400
X-Received-Bytes: 6994
View all headers
On 5/1/22 8:19 AM, olcott wrote:
On 5/1/2022 7:11 AM, Richard Damon wrote:
On 5/1/22 7:54 AM, olcott wrote:
On 5/1/2022 6:26 AM, Richard Damon wrote:
On 5/1/22 7:06 AM, olcott wrote:
On 5/1/2022 4:38 AM, Mikko wrote:
On 2022-04-30 20:48:47 +0000, olcott said:

On 4/30/2022 4:31 AM, Mikko wrote:
On 2022-04-30 07:02:23 +0000, olcott said:

LP := ~True(LP) is translated to Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

This is correct but to fail would also be correct.

?- unify_with_occurs_check(LP, not(true(LP))).
false.

unify_with_occurs_check must fail if the unified data structure
would contain loops.

Mikko


The above is the actual execution of actual Prolog code using
(SWI-Prolog (threaded, 64 bits, version 7.6.4).

Another Prolog implementation might interprete LP = not(true(LP)) differently
and still conform to the prolog standard.

According to Clocksin & Mellish it is not a mere loop, it is an "infinite term" thus infinitely recursive definition.

When discussing data structures, "infinite" and "loop" mean the same.
The data structure is infinitely deep but contains only finitely many
distinct objects and occupies only a finite amount of memory.


That is incorrect. any structure that is infinitely deep would take all of the memory that is available yet specifies an infinite amount of memory.

Nope, a tree that one branch points into itself higher up represents a tree with infinite depth, but only needs a finite amount of memory. Building such a structure may require the ability to forward declare something or reference something not yet defined.


That is counter-factual. unify_with_occurs_check determines that it would require infinite memory and then aborts its evaluation.

You misunderstand what it says. It says that it can't figure how to express the statement without a cycle.

The expression inherently has an infinite cycle, making it erroneous.

Maybe it just says that PROLOG can't express the statement without an infinite cycle due to the limitiations in Prologs logic system?

Better logic systems can handle and work with statements that are self-referential or recursive.

Your reliance on Prolog just limits the fields you can discuss. Like I think Prolog isn't able to express all the properties of the Natural Numbers, which means that it BY DEFINITION isn't capable of handling a full incompleteness prooof.


 That is different then taking infinite memory. It only possibly implies infinite memory in a naive expansion, which isn't the only method.

As was pointed out, the recursive factorial definition, if naively expanded, becomes unbounded in size, but the recursive factorial definition, to a logic system that understands recursion, is usable and has meaning.


Does not have an infinite cycle. It always begins with a finite integer that specifies the finite number of cycles.

Nope. I can write Fact(n), where n is an unknow integer and do logic with it.

Just like H(H^,H^) has a finite expansion if H will answer the question, and thus does not have infinite recursion, and thus H^(H^) does not either as it is a finite extension of the expansion of H(H^,H^).

Only your failure to inplement that limit makes it infinite, which just proves that such an H never answers.


So all you have shown is that these forms CAN cause failure to some forms of naive logic.


An infinite cycle is the same thing as an infinite loop inherently incorrect.


Yes, but a finite loop can expand infinitely if not done correctly or naively. The fact that one method expanse something infinitely doesn't mean the expression is in fact an infinte loop.


You are just stuck in your own false thinking, and have convinced youself of a lie.


You are simply ignoring key details. You are pretending that a finite thing is an infinite thing.

Yes, any expansion of fact for a KNOWN n will be finite, but if n is not known, generates what appears to be an infinite expansion that will colapse to finite once a value is known.

Tell me how many cycles your logic is going to expand fact, and I will give you an n that it didn't handle.




foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
"..." indicates infinite depth, thus infinite string length.

Some infinities have finite representation. You don't seem able to understand that.

Yes, some naive ways of expanding them fail, but the answer to that is you just don't do that, but need to use a less naive method.




I am trying to validate whether or not my Prolog code encodes the Liar Paradox.

That cannot be inferred from Prolog rules. Prolog defines some encodings
like how to encode numbers with characters of Prolog character set but for
more complex things you must make your own encoding rules.

Mikko


This says that G is logically equivalent to its own unprovability in F
G ↔ ¬(F ⊢ G) and fails unify_with_occurs_check when encoded in Prolog.











Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Date: Sun, 1 May 2022 18:28 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!1.us.feeder.erje.net!3.us.feeder.erje.net!feeder.erje.net!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 13:28:18 -0500
Date: Sun, 1 May 2022 13:28:16 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.8.1
Subject: Re: Is this correct Prolog?
Content-Language: en-US
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<FdSdnWijBKlSIfP_nZ2dnUU7_8xh4p2d@giganews.com>
<20220501185933.000045ad@reddwarf.jmc>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <20220501185933.000045ad@reddwarf.jmc>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <d9KdnQdt_bnfTPP_nZ2dnUU7_8zNnZ2d@giganews.com>
Lines: 41
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-8mWIWvK655cOFpaUHaQv5/+vjJc+a8978XxkeLf12HMb8XLex7We5E4uk9nGeQf3I90ts5haNFz7gc8!EbZk0v3hByRiFTIvWXChSFKU+8aXjHAbL1er6Uf2EzTZVVfnNuPVoih6D3CTqYZzKlZvu9xMUYU=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2943
View all headers
On 5/1/2022 12:59 PM, Mr Flibble wrote:
On Sun, 1 May 2022 12:01:01 -0500
olcott <NoOne@NoWhere.com> wrote:

On 5/1/2022 11:21 AM, André G. Isaak wrote:
On 2022-05-01 10:08, olcott wrote:

<snip>

Why are you making the same reply twice under two different
handles? A single reply should suffice.

André
  

I wanted Flibble to see what I said. He may have me on Plonk
  You are not in my kill file: I don't always reply to what you say
because I either agree with what you are saying or the point is
uninteresting to me.

/Flibble


I do think that your idea of "category error" is a brilliant new insight into pathological self-reference problems such as:
(1) The Halting Problem proofs
(2) Gödel's 1930 Incompleteness
(3) The 1936 Undefinability theorem

It very succinctly sums up the entire gist of the semantic error in all of these cases. When it is summed up so effectively it becomes much easier to see exactly what is going on. I have said that it is a semantic error, you pointed out exactly what kind of semantic error.

--
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
Date: Sun, 1 May 2022 19:00 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 14:00:57 -0500
Date: Sun, 1 May 2022 14:00:56 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<FdSdnWijBKlSIfP_nZ2dnUU7_8xh4p2d@giganews.com>
<20220501185933.000045ad@reddwarf.jmc>
<d9KdnQdt_bnfTPP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4mjq0$7nf$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4mjq0$7nf$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <hYKdnb4ZyYB0RfP_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 62
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-wEOGexVS+WMXhB6RdL3bVJ92RK5glgbQ0DMFCvQf0bLcBO7U3qJj+a0xYtQQFZejBb0+M1Zci/IOoT8!/zoaSYpHVqFYovZul+2lC+fHdwXgsVPV+Qn/9pWaiK/qJ227m+GbChVY2arnRSPPOOxGli9m4Rw=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3934
View all headers
On 5/1/2022 1:33 PM, André G. Isaak wrote:
On 2022-05-01 12:28, olcott wrote:
On 5/1/2022 12:59 PM, Mr Flibble wrote:
On Sun, 1 May 2022 12:01:01 -0500
olcott <NoOne@NoWhere.com> wrote:

On 5/1/2022 11:21 AM, André G. Isaak wrote:
On 2022-05-01 10:08, olcott wrote:

<snip>

Why are you making the same reply twice under two different
handles? A single reply should suffice.

André

I wanted Flibble to see what I said. He may have me on Plonk
You are not in my kill file: I don't always reply to what you say
because I either agree with what you are saying or the point is
uninteresting to me.

/Flibble


I do think that your idea of "category error" is a brilliant new insight into pathological self-reference problems such as:
(1) The Halting Problem proofs
(2) Gödel's 1930 Incompleteness
(3) The 1936 Undefinability theorem

It very succinctly sums up the entire gist of the semantic error in all of these cases. When it is summed up so effectively it becomes much easier to see exactly what is going on. I have said that it is a semantic error, you pointed out exactly what kind of semantic error.

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

https://liarparadox.org/Tarski_275_276.pdf

My current thinking on (1) is that a TM is smart enough to see this issue and report on it.

--
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.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Forte - www.forteinc.com
Date: Sun, 1 May 2022 19:19 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Path: i2pn2.org!i2pn.org!news.uzoreto.com!feeder1.feed.usenet.farm!feed.usenet.farm!peer02.ams4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx99.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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<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>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <hYKdnb4ZyYB0RfP_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 64
Message-ID: <i3BbK.379464$Gojc.108205@fx99.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: Sun, 1 May 2022 15:19:44 -0400
X-Received-Bytes: 3993
View all headers

On 5/1/22 3:00 PM, olcott wrote:
On 5/1/2022 1:33 PM, André G. Isaak wrote:
On 2022-05-01 12:28, olcott wrote:
On 5/1/2022 12:59 PM, Mr Flibble wrote:
On Sun, 1 May 2022 12:01:01 -0500
olcott <NoOne@NoWhere.com> wrote:

On 5/1/2022 11:21 AM, André G. Isaak wrote:
On 2022-05-01 10:08, olcott wrote:

<snip>

Why are you making the same reply twice under two different
handles? A single reply should suffice.

André

I wanted Flibble to see what I said. He may have me on Plonk
You are not in my kill file: I don't always reply to what you say
because I either agree with what you are saying or the point is
uninteresting to me.

/Flibble


I do think that your idea of "category error" is a brilliant new insight into pathological self-reference problems such as:
(1) The Halting Problem proofs
(2) Gödel's 1930 Incompleteness
(3) The 1936 Undefinability theorem

It very succinctly sums up the entire gist of the semantic error in all of these cases. When it is summed up so effectively it becomes much easier to see exactly what is going on. I have said that it is a semantic error, you pointed out exactly what kind of semantic error.

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

https://liarparadox.org/Tarski_275_276.pdf

My current thinking on (1) is that a TM is smart enough to see this issue and report on it.


Well, for Godel's G, since it is just that a statement that some statement x is provable, and the provability of a statement is ALWAYS a Truth Bearer, as you can't prove a non-sense sentence, so provable(x) would be false is x is not a valid statement, G is by definition a Truth Bearer.


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Date: Sun, 1 May 2022 19:32 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!1.us.feeder.erje.net!feeder.erje.net!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 14:32:54 -0500
Date: Sun, 1 May 2022 14:32:53 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<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>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4mmmg$t4u$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <APOdndfNnIH7ffP_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 56
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-LDTqngmBoZs8tanCru4XutsEnJ+/dI96AuqOcArbwgXgDBLFear5cXdLoN0fArYHo2PhysyG0mua4Ts!+Kr+Dymu9h+sGR3r0R68AyHS6r4rXI6cE443uN6tATJqASMNnomAhFOs6/LhjpmavOmjZJN2HeA=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3593
View all headers
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.


Gödels G asserts that a specific polynomial equation has a solution.

Since every polynomial equation either has a solution or doesn't have one, G *must* either be true or false which means it *must* be a truth bearer.

André



--
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: André G. Isaak
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Christians and Atheists United Against Creeping Agnosticism
Date: Sun, 1 May 2022 19:44 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: agis...@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Date: Sun, 1 May 2022 13:44:05 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 70
Message-ID: <t4mnu6$96k$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<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>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 May 2022 19:44:06 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="9aade08aa0eb94cd9b9879b12c2d9c29";
logging-data="9428"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/e4Xh0ts1ngi/NUSoxSaPz"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:mtyBIeozA+HbZhkVsx6d2LvicRE=
In-Reply-To: <APOdndfNnIH7ffP_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Language: en-US
View all headers
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.


Gödels G asserts that a specific polynomial equation has a solution.

This is the part you don't seem to get. Gödel's G does *not* assert its own unprovability. It asserts that a specific polynomial equation has a solution.

That's very different from The Liar which asserts its own falsity.

Gödel's theorem constructs a G such that it can be demonstrated that the polynomial which G asserts has a solution can only have a solution in cases where it cannot be proven that that polynomial has a solution.

There is no self-reference involved. G asserts nothing about itself.

More importantly, the polynomial in question *must* either have a solution or not. This means G *must* either be true or false, meaning G *must* be a truth-bearer.

André


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


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Date: Sun, 1 May 2022 19:48 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!weretis.net!feeder8.news.weretis.net!ecngs!feeder2.ecngs.de!178.20.174.213.MISMATCH!feeder1.feed.usenet.farm!feed.usenet.farm!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 14:48:09 -0500
Date: Sun, 1 May 2022 14:48:07 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<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>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4mnu6$96k$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <GYmdnUXY8oBkfvP_nZ2dnUU7_83NnZ2d@giganews.com>
Lines: 62
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-FeToPFnTSyPo6xo8T+SODkbN6COQS7KNTAgpnBPHy01ltyjoIhXOTzY8fC0cJb1Wj3Smo4XRuVXXWjz!UW5ucIj0s2AxkTODlnWnpj21qOHX/akDAxyDBsyAoub9jWS8QVQG/biXi8L4U4Tp5FovZr1UUc0=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4209
View all headers
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.


--
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.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Forte - www.forteinc.com
Date: Sun, 1 May 2022 20:01 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!feeder1.feed.usenet.farm!feed.usenet.farm!feeder.usenetexpress.com!tr3.eu1.usenetexpress.com!newsfeed.xs4all.nl!newsfeed9.news.xs4all.nl!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx98.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> <I4lbK.452483$t2Bb.96330@fx98.iad> <UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me> <EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me> <lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me> <AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me> <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>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <GYmdnUXY8oBkfvP_nZ2dnUU7_83NnZ2d@giganews.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 63
Message-ID: <vGBbK.452496$t2Bb.23163@fx98.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: Sun, 1 May 2022 16:01:32 -0400
X-Received-Bytes: 4154
View all headers
On 5/1/22 3:48 PM, 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.



So something based on another thing is that other thing?

Does that mean your automobile is just a pile of gasoline?

That IS the argument you are making boiled down to simple terms.


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Date: Sun, 1 May 2022 20:42 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.misty.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sun, 01 May 2022 15:42:29 -0500
Date: Sun, 1 May 2022 15:42:28 -0500
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; 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>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<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>
From: NoO...@NoWhere.com (olcott)
In-Reply-To: <t4mr1h$1q0$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Message-ID: <SJGdnZf-9cUobfP_nZ2dnUU7_8xh4p2d@giganews.com>
Lines: 86
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-Cizx665E3hxhaEi15VvppIw98yEaQbrfmWcKjKN31IBkeso5DXE11mJ4Co1mFZkRT0G8L4ROkkNIYLU!BQVNTZSpFuoHdSIJEvepYoQOyNDQ7A5zon8Fb1drxy7v4BGA8mnhBulMyVUZoAnMCbovyskZbeo=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5324
View all headers
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

14 Every epistemological antinomy can likewise be used for a similar
  undecidability proof

The Liar Paradox is an epistemological antinomy


--
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: André G. Isaak
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.prolog
Organization: Christians and Atheists United Against Creeping Agnosticism
Date: Sun, 1 May 2022 20:51 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
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: agis...@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.prolog
Subject: Re: Is this correct Prolog?
Date: Sun, 1 May 2022 14:51:28 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 104
Message-ID: <t4mrsh$871$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<I4lbK.452483$t2Bb.96330@fx98.iad>
<UOGdnc__htYie_D_nZ2dnUU7_83NnZ2d@giganews.com> <t4kp78$vuc$1@dont-email.me>
<EKKdnasbsInXjPP_nZ2dnUU7_83NnZ2d@giganews.com> <t4l65c$bqr$1@dont-email.me>
<lI-dnepDd-0n7PP_nZ2dnUU7_8zNnZ2d@giganews.com> <t4m2b2$kmn$1@dont-email.me>
<AuqdnTWXMZYFLfP_nZ2dnUU7_8xh4p2d@giganews.com> <t4mc2l$2q2$2@dont-email.me>
<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>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 1 May 2022 20:51:30 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="9aade08aa0eb94cd9b9879b12c2d9c29";
logging-data="8417"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/PXiu/6LY1TzH/jquqR7nX"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:o8Fwn2WeiBQptuhQHkPrsz4wzh4=
In-Reply-To: <SJGdnZf-9cUobfP_nZ2dnUU7_8xh4p2d@giganews.com>
Content-Language: en-US
View all headers
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é

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


Pages:123456
rocksolid light 0.7.2
clearneti2ptor