Rocksolid Light

Welcome to RetroBBS

mail  files  register  newsreader  groups  login

Message-ID:  

I have hardly ever known a mathematician who was capable of reasoning. -- Plato


devel / comp.lang.prolog / Re: Is this correct Prolog?

SubjectAuthor
* Is this correct Prolog?olcott
+* Re: Is this correct Prolog?Mikko
|+* Re: Is this correct Prolog?Aleksy Grabowski
||+* Re: Is this correct Prolog?olcott
|||`* Re: Is this correct Prolog?Mikko
||| `* 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?Julio Di Egidio
|||     |  |   `* Re: Is this correct Prolog?Aleksy Grabowski
|||     |  |    +* Re: Is this correct Prolog?Julio Di Egidio
|||     |  |    |`- Re: Is this correct Prolog?olcott
|||     |  |    +- Re: Is this correct Prolog?olcott
|||     |  |    `* 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?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?Julio Di Egidio
|||     |      |`* Re: Is this correct Prolog?Aleksy Grabowski
|||     |      | `- Re: Is this correct Prolog?Julio Di Egidio
|||     |      +* Re: Is this correct Prolog?Ben
|||     |      |+- Re: Is this correct Prolog?Julio Di Egidio
|||     |      |`* Re: Is this correct Prolog?olcott
|||     |      | +* Re: Is this correct Prolog?Ben
|||     |      | |`* Re: Is this correct Prolog?olcott
|||     |      | | +- Re: Is this correct Prolog?Julio Di Egidio
|||     |      | | +* 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? [ Tarski ]olcott
|||     |      | | |     `* Re: Is this correct Prolog? [ Tarski ]Richard Damon
|||     |      | | |      `- Re: Is this correct Prolog? [ Tarski ]olcott
|||     |      | | `- 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?André G. Isaak
|||     |      |  | +* 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?André G. Isaak
|||     |      |  | |   `* 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?André G. Isaak
|||     |      |  | |      `- Re: Is this correct Prolog?Richard Damon
|||     |      |  | `- Re: Is this correct Prolog? [ André didn't lolcott
|||     |      |  `* Re: Is this correct Prolog?Jeff Barnett
|||     |      |   `* 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?André G. Isaak
|||     |      |    |     `* Re: Is this correct Prolog?olcott
|||     |      |    |      `- Re: Is this correct Prolog?Richard Damon
|||     |      |    `* Re: Is this correct Prolog?Jeff Barnett
|||     |      |     `- 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?Julio Di Egidio
|||      +- Re: Is this correct Prolog?Aleksy Grabowski
|||      `* Re: Is this correct Prolog?olcott
|||       `* Re: Is this correct Prolog?Julio Di Egidio
|||        `- Re: Is this correct Prolog?olcott
||`* Re: Is this correct Prolog?Mikko
|| `* 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?Richard Damon

Pages:1234567
Re: Is this correct Prolog?

<t4s9eh$js5$2@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1461&group=comp.lang.prolog#1461

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 17:13:37 -0500
Organization: A noiseless patient Spider
Lines: 65
Message-ID: <t4s9eh$js5$2@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4s8hk$b59$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 3 May 2022 22:13:37 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3f069846940d953f06eba1973f7ebc89";
logging-data="20357"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/ACJUKy27xkkvHcWVQ6Wda"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:b9nyT6Wbz0yj1Xgzsk+yZZhD5Gg=
In-Reply-To: <t4s8hk$b59$1@dont-email.me>
Content-Language: en-US
 by: olcott - Tue, 3 May 2022 22:13 UTC

On 5/3/2022 4:58 PM, Jeff Barnett wrote:
> On 5/3/2022 1:12 PM, olcott wrote:
>> On 5/3/2022 1:33 PM, Jeff Barnett wrote:
>>> On 5/3/2022 9:18 AM, André G. Isaak wrote:
>>>> On 2022-05-02 18:57, olcott wrote:
>>>
>>> IDIOT SNIPPED
>>>
>>>
>>>> No. The Liar can be used to construct an *identical* proof. Other
>>>> antinomies could be used for similar proofs. He's already talking
>>>> about The Liar.
>>>>
>>>>> Which means that the Liar Paradox is sufficiently equivalent to
>>>>> Gödel's G. Which means if the basic mechanism of epistemological
>>>>> antinomy is shown to be semantically incorrect then Gödel's G is
>>>>> shown to be semantically incorrect.
>>>>
>>>> You have some serious reading comprehension problems. I never denied
>>>> the things Gödel wrote. I denied your conclusion because it does not
>>>> follow.
>>>>
>>>> Gödel starts by claiming there is a close relationship (*not*
>>>> equivalence) between one particular antinomy, The Liar, and his G.
>>>>
>>>> He then states that similar proofs could be constructed using any
>>>> antinomy.
>>>>
>>>> That entails that other antinomies could be used to construct
>>>> similar proofs involving a similar close relation (again, *not*
>>>> equivalence).
>>>>
>>>> Gödel never claims *any* antinomy is equivalent to his G. Merely
>>>> that a close relationship holds.
>>>>
>>>> And all my comments concerned exactly what that relationship is.
>>> I think that you have provided the troll a similar explanation over
>>> 100 times. I admire your tenacity but I must ask you a question: Why
>>> do you think one more time will do either him or you any good? It's
>>> not like this is an educational or soul-improving opportunity for
>>> either of you; for you this must be frustrating no matter your
>>> intentions and for him he is what he is and this is his only
>>> amusement. Whether troll or buffoon, he's proud of his appearance as
>>> wasted space.
>>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>> I used the above as the precise measure of isomorphism.
>>
>> The whole error of the incompleteness theorem is entirely anchored in
>> that the official mathematical definition of incompleteness
>> incorrectly presumes that syntactically correct expressions of the
>> language of formal system T are necessarily also semantically incorrect.
>>
>> When T is the entire body of analytic knowledge and φ is the liar
>> paradox, the official mathematical definition of incompleteness
>> determines that the entire body of analytic knowledge is incomplete.
> Polly want a cracker?

In other words you have no rebuttal either because what I said is over
your head or you want to make sure to never agree that I correctly
proved my point. I vote for both.

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

Re: Is this correct Prolog?

<t4spqg$pv0$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1462&group=comp.lang.prolog#1462

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 21:53:01 -0500
Organization: A noiseless patient Spider
Lines: 37
Message-ID: <t4spqg$pv0$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 02:53:04 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3f069846940d953f06eba1973f7ebc89";
logging-data="26592"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19EG1eq42CT6cmTxgotXC76"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:3/8YeGRtN+d5pZ2HSvUVZ3ga/j4=
In-Reply-To: <t4rvd5$3ha$1@dont-email.me>
Content-Language: en-US
 by: olcott - Wed, 4 May 2022 02:53 UTC

On 5/3/2022 2:22 PM, André G. Isaak wrote:
> On 2022-05-03 13:12, olcott wrote:
>
>> When T is the entire body of analytic knowledge and φ is the liar
>> paradox, the official mathematical definition of incompleteness
>> determines that the entire body of analytic knowledge is incomplete.
>
> G is not a formalization of The Liar. There is no such formalization in
> the systems Gödel considers.
>
> The Liar results in inconsistency whereas G results in incompleteness.

Not according to the mathematical definition of incompleteness
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).

Anything and everything that is neither provable nor refutable in some
formal system proves that this formal system IS INCOMPLETE as long as φ
is an expession of language of T.

> This is a major difference between G and The Liar which is why you need
> to stop conflating the two. The Liar only exists in natural language,

That is not true, I think Tarski's way of formalizing the Liar Paradox
may be the best. He describes exactly how it would be formalized and
provides the exactly syntax for formalizing it. I will derive this and
post it sometime soon. I will keep working on this until I am sure that
I have it correctly.

> not in mathematics.
>
> 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

Re: Is this correct Prolog?

<HamcK.11$kgsb.5@fx97.iad>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1463&group=comp.lang.prolog#1463

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!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!fx97.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.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me> <t4spqg$pv0$1@dont-email.me>
From: Richard@Damon-Family.org (Richard Damon)
In-Reply-To: <t4spqg$pv0$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 46
Message-ID: <HamcK.11$kgsb.5@fx97.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: Tue, 3 May 2022 23:12:43 -0400
X-Received-Bytes: 3334
 by: Richard Damon - Wed, 4 May 2022 03:12 UTC

On 5/3/22 10:53 PM, olcott wrote:
> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>> On 2022-05-03 13:12, olcott wrote:
>>
>>> When T is the entire body of analytic knowledge and φ is the liar
>>> paradox, the official mathematical definition of incompleteness
>>> determines that the entire body of analytic knowledge is incomplete.
>>
>> G is not a formalization of The Liar. There is no such formalization
>> in the systems Gödel considers.
>>
>> The Liar results in inconsistency whereas G results in incompleteness.
>
> Not according to the mathematical definition of incompleteness
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>
> Anything and everything that is neither provable nor refutable in some
> formal system proves that this formal system IS INCOMPLETE as long as φ
> is an expession of language of T.

Your missing that he is meaning that if the Liar is TRUE, it shows the
logic system to be inconsistent.

While G being true just proves that the system is Incomplete.

(G not being False in a system shows that the system is Inconsistent, as
it says we can prove a false statement in the system)

>
>> This is a major difference between G and The Liar which is why you
>> need to stop conflating the two. The Liar only exists in natural
>> language,
>
> That is not true, I think Tarski's way of formalizing the Liar Paradox
> may be the best. He describes exactly how it would be formalized and
> provides the exactly syntax for formalizing it. I will derive this and
> post it sometime soon. I will keep working on this until I am sure that
> I have it correctly.
>
>> not in mathematics.
>>
>> André
>>
>
>

Re: Is this correct Prolog?

<t4srko$445$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1464&group=comp.lang.prolog#1464

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 22:24:05 -0500
Organization: A noiseless patient Spider
Lines: 288
Message-ID: <t4srko$445$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rk2m$rei$1@dont-email.me> <t4rmkb$jrt$1@dont-email.me>
<t4rncl$qtf$1@dont-email.me> <t4ro31$1kc$1@dont-email.me>
<t4rp26$a70$1@dont-email.me> <t4rruh$557$1@dont-email.me>
<t4ru1s$mre$1@dont-email.me> <t4s1r5$n2b$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 03:24:08 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3f069846940d953f06eba1973f7ebc89";
logging-data="4229"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+zuvRxhFkR/Wcs8XgceYRN"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:3593X6aGCdFLIYCB5y/AhifUfRY=
In-Reply-To: <t4s1r5$n2b$1@dont-email.me>
Content-Language: en-US
 by: olcott - Wed, 4 May 2022 03:24 UTC

On 5/3/2022 3:03 PM, André G. Isaak wrote:
> On 2022-05-03 12:59, olcott wrote:
>> On 5/3/2022 1:23 PM, André G. Isaak wrote:
>>> On 2022-05-03 11:33, olcott wrote:
>>>> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>>>>> On 2022-05-03 11:05, olcott wrote:
>>>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>>
>>> <snippage>
>>>
>>>>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>>>>> explanation.
>>>>>>>
>>>>>>
>>>>>> When G is not provable in PA, how is it shown to be true?
>>>>>> If it is not shown to be true in PA then we have the strawman error.
>>>>>
>>>>> Here you're simply begging the question by assuming your own
>>>>> conclusion: that being true and being provable are the same.
>>>>
>>>> This is not any mere assumption.
>>>>
>>>> The only way that any analytic expressions of language are correctly
>>>> determined to be true is:
>>>
>>> 'True' and 'Correctly determined to be true' mean different things.
>>>
>>
>> Yes that seems to be correct.
>> On the other hand calling an expression of language true that has not
>> be 'Correctly determined to be true' is an error.
>
> But calling it a "non-truth bearer" simply because it has not been
> determined to be true would equally be an error.
>

That if correct. If is is impossibly true or false then it is not a
truth bearer.

> And it can be shown (i.e. correctly determined) that G is true, just not
> within the system for which it was constructed.
>

unprovable in the system entails untrue in the system.

>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>>
>>>> (a) They are defined to be true.
>>>> (b) They are derived from applying truth preserving operations to
>>>> (a) or (b). Prolog knows this on the basis of its facts and rules.
>>>> Facts are (a) and rules are (b). This is also known as sound
>>>> deductive inference.
>>>
>>> These are YOUR assumptions. They have not been demonstrated. And they
>>> are not consistent with the way in which the rest of the world talks
>>> about truth. You are talking about provability, not truth.
>>>
>>
>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>>
>>>>> The whole point of Gödel's proof is that they cannot be the same
>>>>> (at least not for non-trivial systems).
>>>>>
>>>>
>>>> When G is not provable in PA, how is it shown to be true (wild guess)?
>>>> What is the precise basis for assessing that G is true? please
>>>> provide ALL the steps.
>>>
>>> "True" and "Known to be true" are entirely different things.
>>>
>>
>> Yes, however:
>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>
> As I said, it can be shown in a higher order system.

Sure, yet it is only true in this system which also makes it provable in
that system.

> But even if it could not be, if we can show that G can only be true in
> cases where it is not provable in T, then there are only two possible
> conclusions:
>

It can't be true in T and unprovable in T.

> Either G is true and unprovable in T, in which case T is incomplete.
> Or G is false and provable in T, in which case T is inconsistent.
>

If G is provable in U then it is true in U.
If G is unprovable in T then it is untrue in T.
G is unprovable in T because it is semantically incorrect.

> Which is exactly what Gödel's theorem states: A system can be consistent
> or it can be complete but it cannot be both. An incomplete system is
> still useful. An inconsistent system is not. Ergo he phrases this as an
> consistent system must be incomplete [with the usual caveats about
> meeting some minimum threshold of expressive power].
>
>>> Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
>>> places)
>>>
>>
>> (2748 + 87)^3 = 22,785,532,875
>> What are you sorting with Srt()?
>
> That was obviously a type. Sqrt().
>
>>> That equation is true but it is unlikely anyone knew this to be true
>>> until now since I very much doubt anyone had previously considered
>>> that specific equation. That's doesn't mean it wasn't true all along.
>>> Just that no one knew it was true.
>>>
>>> There are all sorts of cases where we know one thing without knowing
>>> all things. I can know with certainty that (A ∨ B) is true meaning
>>> that I know that *at least* one of A or B must be true while still
>>> not knowing the truth value of either. These sorts of things occur
>>> all the time.
>>>
>>
>> That is not true. If A and B are syntactically correct expressions of
>> a formal language yet neither one is semantically correct then we have
>> the same case as the Liar Paradox not being a truth bearer, thus (A ∨
>> B) is neither true nor false.
>
> But your whole notion of 'semantically correct' is recognized by no one
> but you and is antithetical to the entire notion of a formal system. And
> what I describe above is a situation which *very* commonly arises in
> proofs. They're called proofs by dilemma and take the form:
>
> A → C
> B → C
> (A ∨ B)
>
> Therefore C
>
> We draw a conclusion from A or B without knowing the truth value of
> either. This strategy, for example, was used by Euclid in his proof that
> no largest prime exists.
>
> If you declare A and B to be 'non-truth bearers' simply because you
> don't know whether they are true or false, then this and many other
> proofs completely fall apart.

It is not because they have unknown truth values.

>
>>> And not being provable in PA and not being provable are also two
>>> different things.
>>>
>>
>> I know that. Yet not being provable in PA also means that G cannot be
>> derived in PA by applying truth preserving operations to the axioms Z
>> of PA or other expressions Y derived from Z or Y.
>>
>> If G is correctly determined to be true then there must be some
>> process detailing the steps of how it is 'Correctly determined to be
>> true'.
>
> Just not in PA.

OK great this is great progress!

>> Lacking these steps one cannot correctly assert that G is true, only
>> that G might possibly be true.
>>
>>>>> The question is not whether it is true but whether it is a truth
>>>>> *bearer*.
>>>>>
>>>>> You make the claim that The Liar is not a truth bearer (a plausible
>>>>> claim depending on one's definitions).
>>>>>
>>>>> You then jump to the conclusion that G is not a truth bearer based
>>>>> on your assertion that it is "equivalent" to The Liar. But it is
>>>>> *NOT* equivalent. It merely bears a close relationship. But you
>>>>> refuse to actually consider what the nature of that relationship;
>>>>> there are both similiarites and differences.
>>>>>
>>>>
>>>> Precise equivalence is defined by this:
>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>
>>>> The Liar Paradox can be neither proven nor refuted where T is the
>>>> entire body of analytic knowledge and φ is LP.
>>>
>>> The Liar Paradox is a self-contradiction. The Gödel sentence is not.
>>
>> Until you understand that G can only be correctly asserted to be true
>> in X if G is provable in X. G may be true in X without a proof in X,
>> yet it cannot be correctly asserted to be true in X without such a proof.
>
> This is your confusion, not mine. We can assert that G is not provable
> and that ¬G is also not provable without asserting anything at all about
> whether G is true and still conclude that X is incomplete.


Click here to read the complete article
Re: Is this correct Prolog?

<t4stbd$d3a$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1465&group=comp.lang.prolog#1465

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 22:53:15 -0500
Organization: A noiseless patient Spider
Lines: 64
Message-ID: <t4stbd$d3a$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me> <t4spqg$pv0$1@dont-email.me>
<HamcK.11$kgsb.5@fx97.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 03:53:17 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3f069846940d953f06eba1973f7ebc89";
logging-data="13418"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18OWHal13au89GGoDDFQaZ3"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:RKLvZ1I+HEJ3xat1+M0j1d09xtI=
In-Reply-To: <HamcK.11$kgsb.5@fx97.iad>
Content-Language: en-US
 by: olcott - Wed, 4 May 2022 03:53 UTC

On 5/3/2022 10:12 PM, Richard Damon wrote:
> On 5/3/22 10:53 PM, olcott wrote:
>> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>>> On 2022-05-03 13:12, olcott wrote:
>>>
>>>> When T is the entire body of analytic knowledge and φ is the liar
>>>> paradox, the official mathematical definition of incompleteness
>>>> determines that the entire body of analytic knowledge is incomplete.
>>>
>>> G is not a formalization of The Liar. There is no such formalization
>>> in the systems Gödel considers.
>>>
>>> The Liar results in inconsistency whereas G results in incompleteness.
>>
>> Not according to the mathematical definition of incompleteness
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>> Anything and everything that is neither provable nor refutable in some
>> formal system proves that this formal system IS INCOMPLETE as long as
>> φ is an expession of language of T.
>
> Your missing that he is meaning that if the Liar is TRUE, it shows the
> logic system to be inconsistent.
>

No the LP is semantically incorrect.

> While G being true just proves that the system is Incomplete.
>

Someone here (I think its Andre) now seems to understand that if G is
not provable in F then it is not true in F. If G is true it can only be
true in an other different formal system than F. Tarski says this as
theory and meta-theory.

> (G not being False in a system shows that the system is Inconsistent, as
> it says we can prove a false statement in the system)

G is semantically incorrect thus logically incoherent.

>
>>
>>> This is a major difference between G and The Liar which is why you
>>> need to stop conflating the two. The Liar only exists in natural
>>> language,
>>
>> That is not true, I think Tarski's way of formalizing the Liar Paradox
>> may be the best. He describes exactly how it would be formalized and
>> provides the exactly syntax for formalizing it. I will derive this and
>> post it sometime soon. I will keep working on this until I am sure
>> that I have it correctly.
>>
>>> not in mathematics.
>>>
>>> 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

Re: Is this correct Prolog?

<t4stef$djo$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1466&group=comp.lang.prolog#1466

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: agisaak@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 21:54:53 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 322
Message-ID: <t4stef$djo$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rk2m$rei$1@dont-email.me> <t4rmkb$jrt$1@dont-email.me>
<t4rncl$qtf$1@dont-email.me> <t4ro31$1kc$1@dont-email.me>
<t4rp26$a70$1@dont-email.me> <t4rruh$557$1@dont-email.me>
<t4ru1s$mre$1@dont-email.me> <t4s1r5$n2b$1@dont-email.me>
<t4srko$445$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 03:54:55 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="ab2835e1a019a70ccf6aefd886b80f45";
logging-data="13944"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18r0G9DooeQbnGcMNXdocZ7"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:SMzTmQrARCcZwgXbouilkQx5zvY=
In-Reply-To: <t4srko$445$1@dont-email.me>
Content-Language: en-US
 by: André G. Isaak - Wed, 4 May 2022 03:54 UTC

On 2022-05-03 21:24, olcott wrote:
> On 5/3/2022 3:03 PM, André G. Isaak wrote:
>> On 2022-05-03 12:59, olcott wrote:
>>> On 5/3/2022 1:23 PM, André G. Isaak wrote:
>>>> On 2022-05-03 11:33, olcott wrote:
>>>>> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>>>>>> On 2022-05-03 11:05, olcott wrote:
>>>>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>>>
>>>> <snippage>
>>>>
>>>>>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>>>>>> explanation.
>>>>>>>>
>>>>>>>
>>>>>>> When G is not provable in PA, how is it shown to be true?
>>>>>>> If it is not shown to be true in PA then we have the strawman error.
>>>>>>
>>>>>> Here you're simply begging the question by assuming your own
>>>>>> conclusion: that being true and being provable are the same.
>>>>>
>>>>> This is not any mere assumption.
>>>>>
>>>>> The only way that any analytic expressions of language are
>>>>> correctly determined to be true is:
>>>>
>>>> 'True' and 'Correctly determined to be true' mean different things.
>>>>
>>>
>>> Yes that seems to be correct.
>>> On the other hand calling an expression of language true that has not
>>> be 'Correctly determined to be true' is an error.
>>
>> But calling it a "non-truth bearer" simply because it has not been
>> determined to be true would equally be an error.
>>
>
> That if correct. If is is impossibly true or false then it is not a
> truth bearer.

Neither 'impossibly true' nor 'impossibly false' are meaningful English.
I really wish you would stop using this adverb as if it somehow made
sense. It doesn't.

G is definitely a truth bearer. It states that a specific polynomial
equation has at least one integer solution. Any statement of that form
is either true or false. It is not possible for it to be both. It is not
possible for it to be neither.

>> And it can be shown (i.e. correctly determined) that G is true, just
>> not within the system for which it was constructed.
>>
>
> unprovable in the system entails untrue in the system.

Maybe you should read the actual proof. We proof in some higher order
system T' that G is unprovable in T and that G is true in T.

>>> If G is claimed to be true then this assertion must be supported by:
>>> 'Correctly determined to be true' otherwise the assessment of its
>>> truth is no more than a wild guess.
>>>
>>>>> (a) They are defined to be true.
>>>>> (b) They are derived from applying truth preserving operations to
>>>>> (a) or (b). Prolog knows this on the basis of its facts and rules.
>>>>> Facts are (a) and rules are (b). This is also known as sound
>>>>> deductive inference.
>>>>
>>>> These are YOUR assumptions. They have not been demonstrated. And
>>>> they are not consistent with the way in which the rest of the world
>>>> talks about truth. You are talking about provability, not truth.
>>>>
>>>
>>> If G is claimed to be true then this assertion must be supported by:
>>> 'Correctly determined to be true' otherwise the assessment of its
>>> truth is no more than a wild guess.
>>>
>>>>>> The whole point of Gödel's proof is that they cannot be the same
>>>>>> (at least not for non-trivial systems).
>>>>>>
>>>>>
>>>>> When G is not provable in PA, how is it shown to be true (wild guess)?
>>>>> What is the precise basis for assessing that G is true? please
>>>>> provide ALL the steps.
>>>>
>>>> "True" and "Known to be true" are entirely different things.
>>>>
>>>
>>> Yes, however:
>>> If G is claimed to be true then this assertion must be supported by:
>>> 'Correctly determined to be true' otherwise the assessment of its
>>> truth is no more than a wild guess.
>>
>> As I said, it can be shown in a higher order system.
>
> Sure, yet it is only true in this system which also makes it provable in
> that system.

Again, try reading the actual proof. I mean the math part, not the text
part.

>> But even if it could not be, if we can show that G can only be true in
>> cases where it is not provable in T, then there are only two possible
>> conclusions:
>>
>
> It can't be true in T and unprovable in T.

Yes. It can. That is the entire point of the proof which you have not
actually read. The problem is that you seem to have a personal
definition of 'true' which essentially is the same as 'provable'. Yes,
it can't be both provable in T and unprovable in T, but that's a truism.
Not Gödel's theorem.

>> Either G is true and unprovable in T, in which case T is incomplete.
>> Or G is false and provable in T, in which case T is inconsistent.
>>
>
> If G is provable in U then it is true in U.
> If G is unprovable in T then it is untrue in T.
> G is unprovable in T because it is semantically incorrect.

No one besides you recognizes this whole 'semantic incorrectness'
notion. Until you can get people to accept that there is such a thing,
there is no point bringing it up.

>> Which is exactly what Gödel's theorem states: A system can be
>> consistent or it can be complete but it cannot be both. An incomplete
>> system is still useful. An inconsistent system is not. Ergo he phrases
>> this as an consistent system must be incomplete [with the usual
>> caveats about meeting some minimum threshold of expressive power].
>>
>>>> Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
>>>> places)
>>>>
>>>
>>> (2748 + 87)^3 = 22,785,532,875
>>> What are you sorting with Srt()?
>>
>> That was obviously a type. Sqrt().
>>
>>>> That equation is true but it is unlikely anyone knew this to be true
>>>> until now since I very much doubt anyone had previously considered
>>>> that specific equation. That's doesn't mean it wasn't true all
>>>> along. Just that no one knew it was true.
>>>>
>>>> There are all sorts of cases where we know one thing without knowing
>>>> all things. I can know with certainty that (A ∨ B) is true meaning
>>>> that I know that *at least* one of A or B must be true while still
>>>> not knowing the truth value of either. These sorts of things occur
>>>> all the time.
>>>>
>>>
>>> That is not true. If A and B are syntactically correct expressions of
>>> a formal language yet neither one is semantically correct then we
>>> have the same case as the Liar Paradox not being a truth bearer, thus
>>> (A ∨ B) is neither true nor false.
>>
>> But your whole notion of 'semantically correct' is recognized by no
>> one but you and is antithetical to the entire notion of a formal
>> system. And what I describe above is a situation which *very* commonly
>> arises in proofs. They're called proofs by dilemma and take the form:
>>
>> A → C
>> B → C
>> (A ∨ B)
>>
>> Therefore C
>>
>> We draw a conclusion from A or B without knowing the truth value of
>> either. This strategy, for example, was used by Euclid in his proof
>> that no largest prime exists.
>>
>> If you declare A and B to be 'non-truth bearers' simply because you
>> don't know whether they are true or false, then this and many other
>> proofs completely fall apart.
>
> It is not because they have unknown truth values.

So then what is it? In the case of The Liar I am willing to accept your
claim that it is not a truth-bearer on the grounds that The Liar
effectively has no actual content apart from its own self-referential
claim. That's about the only case I can see it being legitimate to refer
to a declarative sentence as a non-truth bearer (under standard
definitions, truth-bearer and declarative sentence are simply synonyms).

Gödel's G is not like that. It is not self-referential and it does have
actual content.


Click here to read the complete article
Re: Is this correct Prolog?

<t4su4k$hj4$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1467&group=comp.lang.prolog#1467

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: agisaak@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 22:06:43 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 41
Message-ID: <t4su4k$hj4$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me> <t4spqg$pv0$1@dont-email.me>
<HamcK.11$kgsb.5@fx97.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 04:06:44 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="ab2835e1a019a70ccf6aefd886b80f45";
logging-data="18020"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19Nvn+m1F8I6YPkIIIoHjHQ"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:Gr2kqL3+4cptFNizT4rQU9ragWc=
In-Reply-To: <HamcK.11$kgsb.5@fx97.iad>
Content-Language: en-US
 by: André G. Isaak - Wed, 4 May 2022 04:06 UTC

On 2022-05-03 21:12, Richard Damon wrote:
> On 5/3/22 10:53 PM, olcott wrote:
>> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>>> On 2022-05-03 13:12, olcott wrote:
>>>
>>>> When T is the entire body of analytic knowledge and φ is the liar
>>>> paradox, the official mathematical definition of incompleteness
>>>> determines that the entire body of analytic knowledge is incomplete.
>>>
>>> G is not a formalization of The Liar. There is no such formalization
>>> in the systems Gödel considers.
>>>
>>> The Liar results in inconsistency whereas G results in incompleteness.
>>
>> Not according to the mathematical definition of incompleteness
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>> Anything and everything that is neither provable nor refutable in some
>> formal system proves that this formal system IS INCOMPLETE as long as
>> φ is an expession of language of T.
>
> Your missing that he is meaning that if the Liar is TRUE, it shows the
> logic system to be inconsistent.

Actually, it doesn't matter whether it is true or false.

What's relevant here is that it is trivially easy to prove The Liar
using a simple reductio ad absurdum. Unfortunately, it is equally
trivially easy to prove ¬(The Liar) using a reductio of the same form.

That's very different from G, where no proof exists of either G or of ¬G.

The Liar leads to inconsistency.
The sentence 'This sentence is true' would be a natural language example
which leads to incompleteness.

André

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

Re: Is this correct Prolog?

<t4t5p1$va1$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1468&group=comp.lang.prolog#1468

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Wed, 4 May 2022 01:17:03 -0500
Organization: A noiseless patient Spider
Lines: 49
Message-ID: <t4t5p1$va1$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me> <t4spqg$pv0$1@dont-email.me>
<HamcK.11$kgsb.5@fx97.iad> <t4su4k$hj4$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 06:17:05 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3f069846940d953f06eba1973f7ebc89";
logging-data="32065"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18qi0DidPReiJDCY8EGcU2p"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:a26sRzfEg/jI3JfWSoO03b4VGW8=
In-Reply-To: <t4su4k$hj4$1@dont-email.me>
Content-Language: en-US
 by: olcott - Wed, 4 May 2022 06:17 UTC

On 5/3/2022 11:06 PM, André G. Isaak wrote:
> On 2022-05-03 21:12, Richard Damon wrote:
>> On 5/3/22 10:53 PM, olcott wrote:
>>> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>>>> On 2022-05-03 13:12, olcott wrote:
>>>>
>>>>> When T is the entire body of analytic knowledge and φ is the liar
>>>>> paradox, the official mathematical definition of incompleteness
>>>>> determines that the entire body of analytic knowledge is incomplete.
>>>>
>>>> G is not a formalization of The Liar. There is no such formalization
>>>> in the systems Gödel considers.
>>>>
>>>> The Liar results in inconsistency whereas G results in incompleteness.
>>>
>>> Not according to the mathematical definition of incompleteness
>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>
>>> Anything and everything that is neither provable nor refutable in
>>> some formal system proves that this formal system IS INCOMPLETE as
>>> long as φ is an expession of language of T.
>>
>> Your missing that he is meaning that if the Liar is TRUE, it shows the
>> logic system to be inconsistent.
>
> Actually, it doesn't matter whether it is true or false.
>
> What's relevant here is that it is trivially easy to prove The Liar
> using a simple reductio ad absurdum. Unfortunately, it is equally
> trivially easy to prove ¬(The Liar) using a reductio of the same form.
>

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox plugs right in to this
making it equivalent to Gödel's G.

> That's very different from G, where no proof exists of either G or of ¬G.
>
> The Liar leads to inconsistency.
> The sentence 'This sentence is true' would be a natural language example
> which leads to incompleteness.
>
> 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

Re: Is this correct Prolog?

<xqtcK.828001$oF2.145551@fx10.iad>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1469&group=comp.lang.prolog#1469

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.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.theory,comp.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rk2m$rei$1@dont-email.me> <t4rmkb$jrt$1@dont-email.me>
<t4rncl$qtf$1@dont-email.me> <t4ro31$1kc$1@dont-email.me>
<t4rp26$a70$1@dont-email.me> <t4rruh$557$1@dont-email.me>
<t4ru1s$mre$1@dont-email.me> <t4s1r5$n2b$1@dont-email.me>
<t4srko$445$1@dont-email.me>
From: Richard@Damon-Family.org (Richard Damon)
In-Reply-To: <t4srko$445$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Lines: 26
Message-ID: <xqtcK.828001$oF2.145551@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: Wed, 4 May 2022 07:27:28 -0400
X-Received-Bytes: 2860
 by: Richard Damon - Wed, 4 May 2022 11:27 UTC

On 5/3/22 11:24 PM, olcott wrote:
>
> unprovable in the system entails untrue in the system.

Your fundamental error!

Unless the system has define Truth to require provable, which
mathematics hasn't, this is an error, as it isn't a fundamental error.

There are many things that we know have a truth value, but are not
provable or refutable.

And one big effect of your statement is that you effectively disallow
the reasoning about a statement unless you happen to know if it is true
or not. Your logic system precludes thinking about the unknown.

As an aside, it also means you your are declairing that the Bible, that
you like to quote out of is untrue, as is God, because they are not
actually provable in any accepted logic system. This means that by your
own definition, you are now a liar, as you have made assertions based on
a known untrue statement.

Actually, your problem is you don't think your idea out far enough to se
their actually consequences, because your mind is just to simple to
understand things this complicated.

Re: Is this correct Prolog?

<t4u10q$7h7$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1470&group=comp.lang.prolog#1470

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: agisaak@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Wed, 4 May 2022 08:02:00 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 15
Message-ID: <t4u10q$7h7$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me> <t4spqg$pv0$1@dont-email.me>
<HamcK.11$kgsb.5@fx97.iad> <t4su4k$hj4$1@dont-email.me>
<t4t5p1$va1$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 14:02:02 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="d9ca40689cc1496bdce2ef668e2210b1";
logging-data="7719"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+3srCBH0kcwOYdWm9o2pxe"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:TmWWsDi4BpgWTR3ec7ppb4Og/sw=
In-Reply-To: <t4t5p1$va1$1@dont-email.me>
Content-Language: en-US
 by: André G. Isaak - Wed, 4 May 2022 14:02 UTC

On 2022-05-04 00:17, olcott wrote:

> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
> The Liar Paradox plugs right in to this

How exactly does it 'plug right into the above'? As I just said, LP *is*
provable. ¬LP is also provable.

That's what it means to be a contradiction.

André

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

Re: Is this correct Prolog?

<t4uihr$268$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1472&group=comp.lang.prolog#1472

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Wed, 4 May 2022 14:01:13 -0500
Organization: A noiseless patient Spider
Lines: 22
Message-ID: <t4uihr$268$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me> <t4spqg$pv0$1@dont-email.me>
<HamcK.11$kgsb.5@fx97.iad> <t4su4k$hj4$1@dont-email.me>
<t4t5p1$va1$1@dont-email.me> <t4u10q$7h7$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 19:01:15 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3f069846940d953f06eba1973f7ebc89";
logging-data="2248"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/ZLvj/xKEgMnKZYlQiuHQe"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:5gp8QAkRkM3F9sCXCMO+gTm61Fg=
In-Reply-To: <t4u10q$7h7$1@dont-email.me>
Content-Language: en-US
 by: olcott - Wed, 4 May 2022 19:01 UTC

On 5/4/2022 9:02 AM, André G. Isaak wrote:
> On 2022-05-04 00:17, olcott wrote:
>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>> The Liar Paradox plugs right in to this
>
> How exactly does it 'plug right into the above'? As I just said, LP *is*
> provable. ¬LP is also provable.
>
> That's what it means to be a contradiction.
>
> André
>

LP exactly meets the mathematical definition of incompleteness, this
will not be clear until after I correctly formalize it and specify the
formal system to which it belongs. Tarski seems to provide the best head
start on formalizing the LP.

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

Re: Is this correct Prolog?

<LgEcK.94$SOP1.80@fx46.iad>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1473&group=comp.lang.prolog#1473

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!newsreader4.netcologne.de!news.netcologne.de!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.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.theory,comp.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rshj$a86$1@dont-email.me> <t4ruq5$tme$1@dont-email.me>
<t4rvd5$3ha$1@dont-email.me> <t4spqg$pv0$1@dont-email.me>
<HamcK.11$kgsb.5@fx97.iad> <t4su4k$hj4$1@dont-email.me>
<t4t5p1$va1$1@dont-email.me> <t4u10q$7h7$1@dont-email.me>
<t4uihr$268$1@dont-email.me>
From: Richard@Damon-Family.org (Richard Damon)
In-Reply-To: <t4uihr$268$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 32
Message-ID: <LgEcK.94$SOP1.80@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: Wed, 4 May 2022 19:48:00 -0400
X-Received-Bytes: 2917
 by: Richard Damon - Wed, 4 May 2022 23:48 UTC

On 5/4/22 3:01 PM, olcott wrote:
> On 5/4/2022 9:02 AM, André G. Isaak wrote:
>> On 2022-05-04 00:17, olcott wrote:
>>
>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>> The Liar Paradox plugs right in to this
>>
>> How exactly does it 'plug right into the above'? As I just said, LP
>> *is* provable. ¬LP is also provable.
>>
>> That's what it means to be a contradiction.
>>
>> André
>>
>
> LP exactly meets the mathematical definition of incompleteness, this
> will not be clear until after I correctly formalize it and specify the
> formal system to which it belongs. Tarski seems to provide the best head
> start on formalizing the LP.
>

No, because it doesn't meet the requirements to be a φ

As you have mentioned elsewhere, the statement of the Liar Paradox isn't
a Truth Beared, which is part of the requirements built into what φ
needs to be.

Note, your statement of Incompleteness is incomplete without the
defintion of what the various terms mean.

This seems to be a common problem with you, you remove the conditions
and defintions from statements and the misuse them.

Re: Is this correct Prolog? [ Tarski ]

<t4vcsa$g9o$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1474&group=comp.lang.prolog#1474

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog? [ Tarski ]
Date: Wed, 4 May 2022 21:30:30 -0500
Organization: A noiseless patient Spider
Lines: 83
Message-ID: <t4vcsa$g9o$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 5 May 2022 02:30:34 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="919615384a8d329db60bdf86eb51f131";
logging-data="16696"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1819qtQeIAbIhXOS5iMI7zC"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:qglQyTyTXTq6GPE8US4Q/91MFv0=
In-Reply-To: <vU8cK.2577$ATo1.2258@fx33.iad>
Content-Language: en-US
 by: olcott - Thu, 5 May 2022 02:30 UTC

On 5/3/2022 7:05 AM, Richard Damon wrote:
> On 5/2/22 11:01 PM, olcott wrote:
>> On 5/2/2022 9:21 PM, Ben wrote:
>>> olcott <polcott2@gmail.com> writes:
>>>
>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>
>>>>>> Thanks for confirmation, that's what exactly what I was trying to
>>>>>> tell
>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>
>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>> one of
>>>>>> the best proving assistants out there.
>>>>>
>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>
>>>> It is true that G is not provable.
>>>
>>> G is provable.  Proofs abound.  I was pointing out one in a proper proof
>>> assistant, Coq.
>>>
>>
>> It is OK that you are not a math guy.
>> If you were a math guy you would understand that if G is provable then
>> that makes Gödel totally wrong. G is not Gödel's theorem, it is a key
>> element of his theorem.
>>
>> Incomplete T means that there exists a φ such that φ is not provable
>> or refutable in formal system T.
>>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>>
>
> No, G IS provable, just not in the system F that G is described in, thus
> F is Incomplete by your definition above.
>
> Part of the key of the Godel proof is that while G sort of refers to
> itself, it does it in a way that F can't handle, so in F, G doesn't
> refer to itself but just "some statement", but in a 'more advanced'
> version of F, say F', we can see that relationship, and show that G must
> be true, proving it in F', but not in F, thus F is incomplete.
>

Tarski's hierarchy of languages.

It only works at a higher level language because the expression of
language at the next level is not self-contradictory.

All epistemological antinomies are self-contradictory making them
semantically invalid.

In his undefinability proof: (only two pages long)
https://liarparadox.org/Tarski_275_276.pdf

He defines these two levels as "the theory" and the next higher level is
called the "the metatheory". (see link).

> We can then show that we can make a G' in F' with the same property, and
> thus show that there exists a system F'' where we can prove G'.
>
> This is why you simplification doesn't work. In F, we can't convert G
> into the statement G says that G is unprovable, but we can in F', thus
> the statement in F' is that G says that G in unprovable in F, and that
> statement is provable in F'
>

Likewise for the liar Paradox. Apparently Tarski could prove the Liar
Paradox in his meta-theory.

> You don't seem to be able to handle the concept of layers of logic systems.
>

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

Re: Is this correct Prolog? [ Tarski ]

<4UGcK.11523$IQK.4635@fx02.iad>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1475&group=comp.lang.prolog#1475

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.uzoreto.com!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.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? [ Tarski ]
Content-Language: en-US
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me>
From: Richard@Damon-Family.org (Richard Damon)
In-Reply-To: <t4vcsa$g9o$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 96
Message-ID: <4UGcK.11523$IQK.4635@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: Wed, 4 May 2022 22:46:28 -0400
X-Received-Bytes: 5400
 by: Richard Damon - Thu, 5 May 2022 02:46 UTC

On 5/4/22 10:30 PM, olcott wrote:
> On 5/3/2022 7:05 AM, Richard Damon wrote:
>> On 5/2/22 11:01 PM, olcott wrote:
>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>> olcott <polcott2@gmail.com> writes:
>>>>
>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>
>>>>>>> Thanks for confirmation, that's what exactly what I was trying to
>>>>>>> tell
>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare
>>>>>>> form
>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>
>>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>> one of
>>>>>>> the best proving assistants out there.
>>>>>>
>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>
>>>>> It is true that G is not provable.
>>>>
>>>> G is provable.  Proofs abound.  I was pointing out one in a proper
>>>> proof
>>>> assistant, Coq.
>>>>
>>>
>>> It is OK that you are not a math guy.
>>> If you were a math guy you would understand that if G is provable
>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it is
>>> a key element of his theorem.
>>>
>>> Incomplete T means that there exists a φ such that φ is not provable
>>> or refutable in formal system T.
>>>
>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>
>>>
>>
>> No, G IS provable, just not in the system F that G is described in,
>> thus F is Incomplete by your definition above.
>>
>> Part of the key of the Godel proof is that while G sort of refers to
>> itself, it does it in a way that F can't handle, so in F, G doesn't
>> refer to itself but just "some statement", but in a 'more advanced'
>> version of F, say F', we can see that relationship, and show that G
>> must be true, proving it in F', but not in F, thus F is incomplete.
>>
>
> Tarski's hierarchy of languages.
>
> It only works at a higher level language because the expression of
> language at the next level is not self-contradictory.
>
> All epistemological antinomies are self-contradictory making them
> semantically invalid.
>
> In his undefinability proof: (only two pages long)
> https://liarparadox.org/Tarski_275_276.pdf
>
> He defines these two levels as "the theory" and the next higher level is
> called the "the metatheory".  (see link).

So we can prove G in the Metatheory, so it is True in the Theory too.

> since in this interpretation the sentence x, which contains no specific term of the metatheory, is its o\vn correlate, the proof of the sentence x given in the metatheory can automatically be carried over into the theory itself: the sentence x which is undecidable in the original theory becomes a decidable sentence in the enriched theory.

But if G is true in the Theory, it is BY DEFINITION not provable in the
Theory, so the space of the Theory is shown to have a True Statement
which is not provable, thus the system of the Theory in Incomplete.

>
>
>> We can then show that we can make a G' in F' with the same property,
>> and thus show that there exists a system F'' where we can prove G'.
>>
>> This is why you simplification doesn't work. In F, we can't convert G
>> into the statement G says that G is unprovable, but we can in F', thus
>> the statement in F' is that G says that G in unprovable in F, and that
>> statement is provable in F'
>>
>
> Likewise for the liar Paradox. Apparently Tarski could prove the Liar
> Paradox in his meta-theory.
>
>> You don't seem to be able to handle the concept of layers of logic
>> systems.
>>
>
>

Re: Is this correct Prolog? [ Tarski ]

<t4veo9$2d5$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1476&group=comp.lang.prolog#1476

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog? [ Tarski ]
Date: Wed, 4 May 2022 22:02:30 -0500
Organization: A noiseless patient Spider
Lines: 116
Message-ID: <t4veo9$2d5$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 5 May 2022 03:02:33 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="919615384a8d329db60bdf86eb51f131";
logging-data="2469"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX193nV85tezMFJaXQJeX2mIY"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:W7nKzgtXZTl12lrW4Xo91zb8F3A=
In-Reply-To: <4UGcK.11523$IQK.4635@fx02.iad>
Content-Language: en-US
 by: olcott - Thu, 5 May 2022 03:02 UTC

On 5/4/2022 9:46 PM, Richard Damon wrote:
> On 5/4/22 10:30 PM, olcott wrote:
>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>> On 5/2/22 11:01 PM, olcott wrote:
>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>> olcott <polcott2@gmail.com> writes:
>>>>>
>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>
>>>>>>>> Thanks for confirmation, that's what exactly what I was trying
>>>>>>>> to tell
>>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare
>>>>>>>> form
>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>
>>>>>>>> If you want to deal with such problems maybe it is better to use
>>>>>>>> Coq
>>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>>> one of
>>>>>>>> the best proving assistants out there.
>>>>>>>
>>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>
>>>>>> It is true that G is not provable.
>>>>>
>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper
>>>>> proof
>>>>> assistant, Coq.
>>>>>
>>>>
>>>> It is OK that you are not a math guy.
>>>> If you were a math guy you would understand that if G is provable
>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it is
>>>> a key element of his theorem.
>>>>
>>>> Incomplete T means that there exists a φ such that φ is not provable
>>>> or refutable in formal system T.
>>>>
>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>
>>>>
>>>
>>> No, G IS provable, just not in the system F that G is described in,
>>> thus F is Incomplete by your definition above.
>>>
>>> Part of the key of the Godel proof is that while G sort of refers to
>>> itself, it does it in a way that F can't handle, so in F, G doesn't
>>> refer to itself but just "some statement", but in a 'more advanced'
>>> version of F, say F', we can see that relationship, and show that G
>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>
>>
>> Tarski's hierarchy of languages.
>>
>> It only works at a higher level language because the expression of
>> language at the next level is not self-contradictory.
>>
>> All epistemological antinomies are self-contradictory making them
>> semantically invalid.
>>
>> In his undefinability proof: (only two pages long)
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>> He defines these two levels as "the theory" and the next higher level
>> is called the "the metatheory".  (see link).
>
> So we can prove G in the Metatheory, so it is True in the Theory too.

In the same way that having a cat in your attic is proof that your car
is leaking oil.

>> since in this interpretation the sentence x, which contains no
>> specific term of the metatheory, is its o\vn correlate, the proof of
>> the sentence x given in the metatheory can automatically be carried
>> over into the theory itself: the sentence x which is undecidable in
>> the original theory becomes a decidable sentence in the enriched theory.
>
> But if G is true in the Theory, it is BY DEFINITION not provable in the
> Theory, so the space of the Theory is shown to have a True Statement
> which is not provable, thus the system of the Theory in Incomplete.

It really has never made any sense how people can't understand that
self-contradictory expressions of language are necessary semantically
invalid. Back in 1974 mankind has had almost 2000 years to think about
the Liar Paradox and no one had a clue what the issue was.

Any unprovable expression of any formal or natural language is simply
untrue and nothing more.

>>
>>
>>> We can then show that we can make a G' in F' with the same property,
>>> and thus show that there exists a system F'' where we can prove G'.
>>>
>>> This is why you simplification doesn't work. In F, we can't convert G
>>> into the statement G says that G is unprovable, but we can in F',
>>> thus the statement in F' is that G says that G in unprovable in F,
>>> and that statement is provable in F'
>>>
>>
>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar
>> Paradox in his meta-theory.
>>
>>> You don't seem to be able to handle the concept of layers of logic
>>> systems.
>>>
>>
>>
>

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

Re: Is this correct Prolog? [ Tarski ]

<XJOcK.720276$7F2.122603@fx12.iad>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1487&group=comp.lang.prolog#1487

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!aioe.org!feeder1.feed.usenet.farm!feed.usenet.farm!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx12.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? [ Tarski ]
Content-Language: en-US
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
<t4veo9$2d5$1@dont-email.me>
From: Richard@Damon-Family.org (Richard Damon)
In-Reply-To: <t4veo9$2d5$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 148
Message-ID: <XJOcK.720276$7F2.122603@fx12.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: Thu, 5 May 2022 07:41:46 -0400
X-Received-Bytes: 7492
 by: Richard Damon - Thu, 5 May 2022 11:41 UTC

On 5/4/22 11:02 PM, olcott wrote:
> On 5/4/2022 9:46 PM, Richard Damon wrote:
>> On 5/4/22 10:30 PM, olcott wrote:
>>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>>> On 5/2/22 11:01 PM, olcott wrote:
>>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>>> olcott <polcott2@gmail.com> writes:
>>>>>>
>>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>
>>>>>>>>> Thanks for confirmation, that's what exactly what I was trying
>>>>>>>>> to tell
>>>>>>>>> to topic poster in one of my previous posts. Prolog in it's
>>>>>>>>> bare form
>>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>>
>>>>>>>>> If you want to deal with such problems maybe it is better to
>>>>>>>>> use Coq
>>>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>>>> one of
>>>>>>>>> the best proving assistants out there.
>>>>>>>>
>>>>>>>> And indeed there is a fully formalised proof of GIT in Coq
>>>>>>>> (though I
>>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>
>>>>>>> It is true that G is not provable.
>>>>>>
>>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper
>>>>>> proof
>>>>>> assistant, Coq.
>>>>>>
>>>>>
>>>>> It is OK that you are not a math guy.
>>>>> If you were a math guy you would understand that if G is provable
>>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it
>>>>> is a key element of his theorem.
>>>>>
>>>>> Incomplete T means that there exists a φ such that φ is not
>>>>> provable or refutable in formal system T.
>>>>>
>>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>>
>>>>>
>>>>
>>>> No, G IS provable, just not in the system F that G is described in,
>>>> thus F is Incomplete by your definition above.
>>>>
>>>> Part of the key of the Godel proof is that while G sort of refers to
>>>> itself, it does it in a way that F can't handle, so in F, G doesn't
>>>> refer to itself but just "some statement", but in a 'more advanced'
>>>> version of F, say F', we can see that relationship, and show that G
>>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>>
>>>
>>> Tarski's hierarchy of languages.
>>>
>>> It only works at a higher level language because the expression of
>>> language at the next level is not self-contradictory.
>>>
>>> All epistemological antinomies are self-contradictory making them
>>> semantically invalid.
>>>
>>> In his undefinability proof: (only two pages long)
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>> He defines these two levels as "the theory" and the next higher level
>>> is called the "the metatheory".  (see link).
>>
>> So we can prove G in the Metatheory, so it is True in the Theory too.
>
> In the same way that having a cat in your attic is proof that your car
> is leaking oil.

Nope, shows you don't understand the proof. Have you actually read it,
or just the 'cliff notes' version. You know, the one with the actual

>
>>> since in this interpretation the sentence x, which contains no
>>> specific term of the metatheory, is its o\vn correlate, the proof of
>>> the sentence x given in the metatheory can automatically be carried
>>> over into the theory itself: the sentence x which is undecidable in
>>> the original theory becomes a decidable sentence in the enriched theory.
>>
>> But if G is true in the Theory, it is BY DEFINITION not provable in
>> the Theory, so the space of the Theory is shown to have a True
>> Statement which is not provable, thus the system of the Theory in
>> Incomplete.
>
> It really has never made any sense how people can't understand that
> self-contradictory expressions of language are necessary semantically
> invalid. Back in 1974 mankind has had almost 2000 years to think about
> the Liar Paradox and no one had a clue what the issue was.

Except that G isn't self-contradictory. The actual G makes a statement
of a mathematical problem and asks if it has a solution. That sort of
statement is ALWAYS a Truth Bearer.

I think your problem is you don't even uderstand that power and limits
of semantics.

>
> Any unprovable expression of any formal or natural language is simply
> untrue and nothing more.

Nope. Truth does not mean Provable. An Unproven statement (or even
unprovable statement) might still be True, it just can't be KNOWN. You
confuse truth with knowledge, maybe because you have too much ego and
think your knowledge defines what is.

By your statement, the Bible is untrue, and you are thus a Liar for
making statements based on it being true.

We can't beleive the words of a Liar, so we shouldn't beleive you when
you claim Truth implies Provable.

Yes, you can build a logic system that defines that, in that system, a
statement is only a Truth Bearer is it is provable or refutable, but
such a system can not handle our mathematics (at least not and stay
consistent).

All you are doing is showing you don't understand how logic actually works.

>
>>>
>>>
>>>> We can then show that we can make a G' in F' with the same property,
>>>> and thus show that there exists a system F'' where we can prove G'.
>>>>
>>>> This is why you simplification doesn't work. In F, we can't convert
>>>> G into the statement G says that G is unprovable, but we can in F',
>>>> thus the statement in F' is that G says that G in unprovable in F,
>>>> and that statement is provable in F'
>>>>
>>>
>>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar
>>> Paradox in his meta-theory.
>>>
>>>> You don't seem to be able to handle the concept of layers of logic
>>>> systems.
>>>>
>>>
>>>
>>
>
>

Re: Is this correct Prolog? [ Tarski ]

<t5136n$4j0$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1488&group=comp.lang.prolog#1488

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog? [ Tarski ]
Date: Thu, 5 May 2022 12:57:41 -0500
Organization: A noiseless patient Spider
Lines: 117
Message-ID: <t5136n$4j0$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 5 May 2022 17:57:43 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="919615384a8d329db60bdf86eb51f131";
logging-data="4704"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+hvuBQ+Mux6aNaKtHsP22Q"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:cM0lUvIl13FBq92R87jfClg+ms4=
In-Reply-To: <4UGcK.11523$IQK.4635@fx02.iad>
Content-Language: en-US
 by: olcott - Thu, 5 May 2022 17:57 UTC

On 5/4/2022 9:46 PM, Richard Damon wrote:
> On 5/4/22 10:30 PM, olcott wrote:
>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>> On 5/2/22 11:01 PM, olcott wrote:
>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>> olcott <polcott2@gmail.com> writes:
>>>>>
>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>
>>>>>>>> Thanks for confirmation, that's what exactly what I was trying
>>>>>>>> to tell
>>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare
>>>>>>>> form
>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>
>>>>>>>> If you want to deal with such problems maybe it is better to use
>>>>>>>> Coq
>>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>>> one of
>>>>>>>> the best proving assistants out there.
>>>>>>>
>>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>
>>>>>> It is true that G is not provable.
>>>>>
>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper
>>>>> proof
>>>>> assistant, Coq.
>>>>>
>>>>
>>>> It is OK that you are not a math guy.
>>>> If you were a math guy you would understand that if G is provable
>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it is
>>>> a key element of his theorem.
>>>>
>>>> Incomplete T means that there exists a φ such that φ is not provable
>>>> or refutable in formal system T.
>>>>
>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>
>>>>
>>>
>>> No, G IS provable, just not in the system F that G is described in,
>>> thus F is Incomplete by your definition above.
>>>
>>> Part of the key of the Godel proof is that while G sort of refers to
>>> itself, it does it in a way that F can't handle, so in F, G doesn't
>>> refer to itself but just "some statement", but in a 'more advanced'
>>> version of F, say F', we can see that relationship, and show that G
>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>
>>
>> Tarski's hierarchy of languages.
>>
>> It only works at a higher level language because the expression of
>> language at the next level is not self-contradictory.
>>
>> All epistemological antinomies are self-contradictory making them
>> semantically invalid.
>>
>> In his undefinability proof: (only two pages long)
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>> He defines these two levels as "the theory" and the next higher level
>> is called the "the metatheory".  (see link).
>
> So we can prove G in the Metatheory,

Yes.

> so it is True in the Theory too.
>

Not at all.
In the theory p is self-contradictory thus not a truth bearer.
In the meta-theory p is NOT self-contradictory.

>> since in this interpretation the sentence x, which contains no
>> specific term of the metatheory, is its o\vn correlate, the proof of
>> the sentence x given in the metatheory can automatically be carried
>> over into the theory itself: the sentence x which is undecidable in
>> the original theory becomes a decidable sentence in the enriched theory.
>
> But if G is true in the Theory, it is BY DEFINITION not provable in the
> Theory, so the space of the Theory is shown to have a True Statement
> which is not provable, thus the system of the Theory in Incomplete.

G is self-contradictory on the theory and non self-contradictory in the
meta-theory.

>>
>>
>>> We can then show that we can make a G' in F' with the same property,
>>> and thus show that there exists a system F'' where we can prove G'.
>>>
>>> This is why you simplification doesn't work. In F, we can't convert G
>>> into the statement G says that G is unprovable, but we can in F',
>>> thus the statement in F' is that G says that G in unprovable in F,
>>> and that statement is provable in F'
>>>
>>
>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar
>> Paradox in his meta-theory.
>>
>>> You don't seem to be able to handle the concept of layers of logic
>>> systems.
>>>
>>
>>
>

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

Re: Is this correct Prolog? [ Tarski ]

<t513mm$7em$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1489&group=comp.lang.prolog#1489

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: agisaak@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog? [ Tarski ]
Date: Thu, 5 May 2022 12:06:14 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 25
Message-ID: <t513mm$7em$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
<t5136n$4j0$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 5 May 2022 18:06:14 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="03a10ab673fa74b3fe7321cc8217bc91";
logging-data="7638"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19aJk4j+SQGIolkiT6USbgX"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:vDtlqJKwEV/9QYuC2hTYalBSQ1g=
In-Reply-To: <t5136n$4j0$1@dont-email.me>
Content-Language: en-US
 by: André G. Isaak - Thu, 5 May 2022 18:06 UTC

On 2022-05-05 11:57, olcott wrote:
> On 5/4/2022 9:46 PM, Richard Damon wrote:

>> But if G is true in the Theory, it is BY DEFINITION not provable in
>> the Theory, so the space of the Theory is shown to have a True
>> Statement which is not provable, thus the system of the Theory in
>> Incomplete.
>
> G is self-contradictory on the theory and non self-contradictory in the
> meta-theory.

G is not self-contradictory in either the theory or the meta-theory.

The Liar Paradox and G are not the same sentence. You keep treating them
as if they were based solely on Gödel's claim that there is a close
relationship between them. But saying two things are closely related
does not mean they are the same.

G asserts a claim about arithmetic. It asserts nothing about itself.

André

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

Re: Is this correct Prolog? [ Tarski ]

<t51f8k$5sc$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1490&group=comp.lang.prolog#1490

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Followup: comp.theory
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog? [ Tarski ]
Followup-To: comp.theory
Date: Thu, 5 May 2022 16:23:30 -0500
Organization: A noiseless patient Spider
Lines: 50
Message-ID: <t51f8k$5sc$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
<t5136n$4j0$1@dont-email.me> <t513mm$7em$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 5 May 2022 21:23:32 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="919615384a8d329db60bdf86eb51f131";
logging-data="6028"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19nxpM0tgYg7uznK1kCSx5v"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:sPXTeiCqnBdhNOQLDH+fdo9bZbM=
In-Reply-To: <t513mm$7em$1@dont-email.me>
Content-Language: en-US
 by: olcott - Thu, 5 May 2022 21:23 UTC

On 5/5/2022 1:06 PM, André G. Isaak wrote:
> On 2022-05-05 11:57, olcott wrote:
>> On 5/4/2022 9:46 PM, Richard Damon wrote:
>
>>> But if G is true in the Theory, it is BY DEFINITION not provable in
>>> the Theory, so the space of the Theory is shown to have a True
>>> Statement which is not provable, thus the system of the Theory in
>>> Incomplete.
>>
>> G is self-contradictory on the theory and non self-contradictory in
>> the meta-theory.
>
> G is not self-contradictory in either the theory or the meta-theory.
>
> The Liar Paradox and G are not the same sentence. You keep treating them
> as if they were based solely on Gödel's claim that there is a close
> relationship between them. But saying two things are closely related
> does not mean they are the same.
>
> G asserts a claim about arithmetic. It asserts nothing about itself.
>
> André
>

From the quote below:
We are therefore confronted with a proposition which asserts its own
unprovability.

Gödel says:
The analogy between this result and Richard’s antinomy leaps to the eye;
there is also a close relationship with the “liar” antinomy,14 since the
undecidable proposition [R(q); q] states precisely that q belongs to K,
i.e. according to (1), that [R(q); q] is not provable. We are therefore
confronted with a proposition which asserts its own unprovability.

Tarski proof is based on this exact same thing in its first step:
https://liarparadox.org/Tarski_275_276.pdf

(1) x ⋶ Pr if and only if p
where the symbol 'p' represents the whole sentence x
and Pr means Provable

This is a Tarski was of saying:
"a proposition which asserts its own unprovability."

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

Re: Is this correct Prolog? [ Tarski ]

<8F%cK.42$t72a.1@fx10.iad>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1491&group=comp.lang.prolog#1491

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!feeder1.feed.usenet.farm!feed.usenet.farm!news-out.netnews.com!news.alt.net!fdc2.netnews.com!peer01.ams1!peer.ams1.xlned.com!news.xlned.com!peer01.ams4!peer.am4.highwinds-media.com!peer03.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? [ Tarski ]
Content-Language: en-US
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
<t5136n$4j0$1@dont-email.me>
From: Richard@Damon-Family.org (Richard Damon)
In-Reply-To: <t5136n$4j0$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 131
Message-ID: <8F%cK.42$t72a.1@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: Thu, 5 May 2022 22:24:05 -0400
X-Received-Bytes: 6445
 by: Richard Damon - Fri, 6 May 2022 02:24 UTC

On 5/5/22 1:57 PM, olcott wrote:
> On 5/4/2022 9:46 PM, Richard Damon wrote:
>> On 5/4/22 10:30 PM, olcott wrote:
>>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>>> On 5/2/22 11:01 PM, olcott wrote:
>>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>>> olcott <polcott2@gmail.com> writes:
>>>>>>
>>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>
>>>>>>>>> Thanks for confirmation, that's what exactly what I was trying
>>>>>>>>> to tell
>>>>>>>>> to topic poster in one of my previous posts. Prolog in it's
>>>>>>>>> bare form
>>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>>
>>>>>>>>> If you want to deal with such problems maybe it is better to
>>>>>>>>> use Coq
>>>>>>>>> theorem prover, I've never used it by myself, but it looks like
>>>>>>>>> one of
>>>>>>>>> the best proving assistants out there.
>>>>>>>>
>>>>>>>> And indeed there is a fully formalised proof of GIT in Coq
>>>>>>>> (though I
>>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>
>>>>>>> It is true that G is not provable.
>>>>>>
>>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper
>>>>>> proof
>>>>>> assistant, Coq.
>>>>>>
>>>>>
>>>>> It is OK that you are not a math guy.
>>>>> If you were a math guy you would understand that if G is provable
>>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it
>>>>> is a key element of his theorem.
>>>>>
>>>>> Incomplete T means that there exists a φ such that φ is not
>>>>> provable or refutable in formal system T.
>>>>>
>>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>>
>>>>>
>>>>
>>>> No, G IS provable, just not in the system F that G is described in,
>>>> thus F is Incomplete by your definition above.
>>>>
>>>> Part of the key of the Godel proof is that while G sort of refers to
>>>> itself, it does it in a way that F can't handle, so in F, G doesn't
>>>> refer to itself but just "some statement", but in a 'more advanced'
>>>> version of F, say F', we can see that relationship, and show that G
>>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>>
>>>
>>> Tarski's hierarchy of languages.
>>>
>>> It only works at a higher level language because the expression of
>>> language at the next level is not self-contradictory.
>>>
>>> All epistemological antinomies are self-contradictory making them
>>> semantically invalid.
>>>
>>> In his undefinability proof: (only two pages long)
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>> He defines these two levels as "the theory" and the next higher level
>>> is called the "the metatheory".  (see link).
>>
>> So we can prove G in the Metatheory,
>
> Yes.
>
>> so it is True in the Theory too.
>>
>
> Not at all.
> In the theory p is self-contradictory thus not a truth bearer.
> In the meta-theory p is NOT self-contradictory.

How do you get that.

In the Theory, you can't even tell that G references itself, but is just
a statement about mathematics.

>
>>> since in this interpretation the sentence x, which contains no
>>> specific term of the metatheory, is its o\vn correlate, the proof of
>>> the sentence x given in the metatheory can automatically be carried
>>> over into the theory itself: the sentence x which is undecidable in
>>> the original theory becomes a decidable sentence in the enriched theory.
>>
>> But if G is true in the Theory, it is BY DEFINITION not provable in
>> the Theory, so the space of the Theory is shown to have a True
>> Statement which is not provable, thus the system of the Theory in
>> Incomplete.
>
> G is self-contradictory on the theory and non self-contradictory in the
> meta-theory.

No, because in the theory, G doesn't even reference itself, so it can't
be self-contradictory.

I think you don't even know what G is, but have only read the clift
notes edition that actually explain it in the meta-theory.

>
>>>
>>>
>>>> We can then show that we can make a G' in F' with the same property,
>>>> and thus show that there exists a system F'' where we can prove G'.
>>>>
>>>> This is why you simplification doesn't work. In F, we can't convert
>>>> G into the statement G says that G is unprovable, but we can in F',
>>>> thus the statement in F' is that G says that G in unprovable in F,
>>>> and that statement is provable in F'
>>>>
>>>
>>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar
>>> Paradox in his meta-theory.
>>>
>>>> You don't seem to be able to handle the concept of layers of logic
>>>> systems.
>>>>
>>>
>>>
>>
>
>

Re: Is this correct Prolog? [ Tarski ]

<t521m1$u43$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1492&group=comp.lang.prolog#1492

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog? [ Tarski ]
Date: Thu, 5 May 2022 21:37:51 -0500
Organization: A noiseless patient Spider
Lines: 151
Message-ID: <t521m1$u43$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
<t5136n$4j0$1@dont-email.me> <8F%cK.42$t72a.1@fx10.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 6 May 2022 02:37:53 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="fa499fb4eb95ee5c956e821cecab3aa5";
logging-data="30851"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+/HPLJYMSXu4ttEM9/wMkV"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:L8aW4tEbaC8liIC89T3xoUz9F40=
In-Reply-To: <8F%cK.42$t72a.1@fx10.iad>
Content-Language: en-US
 by: olcott - Fri, 6 May 2022 02:37 UTC

On 5/5/2022 9:24 PM, Richard Damon wrote:
> On 5/5/22 1:57 PM, olcott wrote:
>> On 5/4/2022 9:46 PM, Richard Damon wrote:
>>> On 5/4/22 10:30 PM, olcott wrote:
>>>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>>>> On 5/2/22 11:01 PM, olcott wrote:
>>>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>>>> olcott <polcott2@gmail.com> writes:
>>>>>>>
>>>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>>
>>>>>>>>>> Thanks for confirmation, that's what exactly what I was trying
>>>>>>>>>> to tell
>>>>>>>>>> to topic poster in one of my previous posts. Prolog in it's
>>>>>>>>>> bare form
>>>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>>>
>>>>>>>>>> If you want to deal with such problems maybe it is better to
>>>>>>>>>> use Coq
>>>>>>>>>> theorem prover, I've never used it by myself, but it looks
>>>>>>>>>> like one of
>>>>>>>>>> the best proving assistants out there.
>>>>>>>>>
>>>>>>>>> And indeed there is a fully formalised proof of GIT in Coq
>>>>>>>>> (though I
>>>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>>
>>>>>>>> It is true that G is not provable.
>>>>>>>
>>>>>>> G is provable.  Proofs abound.  I was pointing out one in a
>>>>>>> proper proof
>>>>>>> assistant, Coq.
>>>>>>>
>>>>>>
>>>>>> It is OK that you are not a math guy.
>>>>>> If you were a math guy you would understand that if G is provable
>>>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it
>>>>>> is a key element of his theorem.
>>>>>>
>>>>>> Incomplete T means that there exists a φ such that φ is not
>>>>>> provable or refutable in formal system T.
>>>>>>
>>>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>>>
>>>>>>
>>>>>
>>>>> No, G IS provable, just not in the system F that G is described in,
>>>>> thus F is Incomplete by your definition above.
>>>>>
>>>>> Part of the key of the Godel proof is that while G sort of refers
>>>>> to itself, it does it in a way that F can't handle, so in F, G
>>>>> doesn't refer to itself but just "some statement", but in a 'more
>>>>> advanced' version of F, say F', we can see that relationship, and
>>>>> show that G must be true, proving it in F', but not in F, thus F is
>>>>> incomplete.
>>>>>
>>>>
>>>> Tarski's hierarchy of languages.
>>>>
>>>> It only works at a higher level language because the expression of
>>>> language at the next level is not self-contradictory.
>>>>
>>>> All epistemological antinomies are self-contradictory making them
>>>> semantically invalid.
>>>>
>>>> In his undefinability proof: (only two pages long)
>>>> https://liarparadox.org/Tarski_275_276.pdf
>>>>
>>>> He defines these two levels as "the theory" and the next higher
>>>> level is called the "the metatheory".  (see link).
>>>
>>> So we can prove G in the Metatheory,
>>
>> Yes.
>>
>>> so it is True in the Theory too.
>>>
>>
>> Not at all.
>> In the theory p is self-contradictory thus not a truth bearer.
>> In the meta-theory p is NOT self-contradictory.
>
> How do you get that.
>

In Tarski's theory p <is> the formalized liar paradox.

> In the Theory, you can't even tell that G references itself, but is just
> a statement about mathematics.
>
>>
>>>> since in this interpretation the sentence x, which contains no
>>>> specific term of the metatheory, is its o\vn correlate, the proof of
>>>> the sentence x given in the metatheory can automatically be carried
>>>> over into the theory itself: the sentence x which is undecidable in
>>>> the original theory becomes a decidable sentence in the enriched
>>>> theory.
>>>
>>> But if G is true in the Theory, it is BY DEFINITION not provable in
>>> the Theory, so the space of the Theory is shown to have a True
>>> Statement which is not provable, thus the system of the Theory in
>>> Incomplete.
>>
>> G is self-contradictory on the theory and non self-contradictory in
>> the meta-theory.
>
> No, because in the theory, G doesn't even reference itself, so it can't
> be self-contradictory.
>

Gödel says:
....We are therefore confronted with a proposition which asserts its own
unprovability.

> I think you don't even know what G is, but have only read the clift
> notes edition that actually explain it in the meta-theory.

>>
>>>>
>>>>
>>>>> We can then show that we can make a G' in F' with the same
>>>>> property, and thus show that there exists a system F'' where we can
>>>>> prove G'.
>>>>>
>>>>> This is why you simplification doesn't work. In F, we can't convert
>>>>> G into the statement G says that G is unprovable, but we can in F',
>>>>> thus the statement in F' is that G says that G in unprovable in F,
>>>>> and that statement is provable in F'
>>>>>
>>>>
>>>> Likewise for the liar Paradox. Apparently Tarski could prove the
>>>> Liar Paradox in his meta-theory.
>>>>
>>>>> You don't seem to be able to handle the concept of layers of logic
>>>>> systems.
>>>>>
>>>>
>>>>
>>>
>>
>>
>

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

Re: Is this correct Prolog? [ Tarski ]

<aR7dK.408$Acq9.201@fx13.iad>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1494&group=comp.lang.prolog#1494

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!peer03.ams4!peer.am4.highwinds-media.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx13.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0)
Gecko/20100101 Thunderbird/91.9.0
Subject: Re: Is this correct Prolog? [ Tarski ]
Content-Language: en-US
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
<t5136n$4j0$1@dont-email.me> <8F%cK.42$t72a.1@fx10.iad>
<t521m1$u43$1@dont-email.me>
From: Richard@Damon-Family.org (Richard Damon)
In-Reply-To: <t521m1$u43$1@dont-email.me>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 30
Message-ID: <aR7dK.408$Acq9.201@fx13.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Fri, 6 May 2022 07:43:03 -0400
X-Received-Bytes: 2604
 by: Richard Damon - Fri, 6 May 2022 11:43 UTC

On 5/5/22 10:37 PM, olcott wrote:
> On 5/5/2022 9:24 PM, Richard Damon wrote:
>> On 5/5/22 1:57 PM, olcott wrote:

>>> G is self-contradictory on the theory and non self-contradictory in
>>> the meta-theory.
>>
>> No, because in the theory, G doesn't even reference itself, so it
>> can't be self-contradictory.
>>
>
> Gödel says:
> ...We are therefore confronted with a proposition which asserts its own
> unprovability.
>

Which is Godel making a comment about G, and not a statement in G itself.

G does not directly mention itself in the Theory.

>> I think you don't even know what G is, but have only read the clift
>> notes edition that actually explain it in the meta-theory.
>
>

So this comment of mine is now proven.

And you have prooved to be a Liar and an idiot, as you abolutely don't
know what you are talking about.

Re: Is this correct Prolog? [ Tarski ]

<t540g5$jst$1@dont-email.me>

  copy mid

https://www.rocksolidbbs.com/devel/article-flat.php?id=1495&group=comp.lang.prolog#1495

  copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polcott2@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog? [ Tarski ]
Date: Fri, 6 May 2022 15:29:55 -0500
Organization: A noiseless patient Spider
Lines: 62
Message-ID: <t540g5$jst$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <874k27fjan.fsf@bsb.me.uk>
<t4q5uo$veh$1@dont-email.me> <vU8cK.2577$ATo1.2258@fx33.iad>
<t4vcsa$g9o$1@dont-email.me> <4UGcK.11523$IQK.4635@fx02.iad>
<t5136n$4j0$1@dont-email.me> <8F%cK.42$t72a.1@fx10.iad>
<t521m1$u43$1@dont-email.me> <aR7dK.408$Acq9.201@fx13.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 6 May 2022 20:29:57 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="fa499fb4eb95ee5c956e821cecab3aa5";
logging-data="20381"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18NtRoqTkPseQeb94EUXY8P"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:Ixph37aLkbDPWtw674qf6dcILcA=
In-Reply-To: <aR7dK.408$Acq9.201@fx13.iad>
Content-Language: en-US
 by: olcott - Fri, 6 May 2022 20:29 UTC

On 5/6/2022 6:43 AM, Richard Damon wrote:
>
> On 5/5/22 10:37 PM, olcott wrote:
>> On 5/5/2022 9:24 PM, Richard Damon wrote:
>>> On 5/5/22 1:57 PM, olcott wrote:
>
>>>> G is self-contradictory on the theory and non self-contradictory in
>>>> the meta-theory.
>>>
>>> No, because in the theory, G doesn't even reference itself, so it
>>> can't be self-contradictory.
>>>
>>
>> Gödel says:
>> ...We are therefore confronted with a proposition which asserts its
>> own unprovability.
>>
>
> Which is Godel making a comment about G, and not a statement in G itself.
>
> G does not directly mention itself in the Theory.

Gödel says that it does with dodgy words that also says that it does not.

15 In spite of appearances, there is nothing circular about such a
proposition, since it begins by asserting the unprovability of a wholly
determinate formula (namely the q-th in the alphabetical arrangement
with a definite substitution), and only subsequently (and in some way by
accident)does it emerge that this formula is precisely that by which the
proposition was itself expressed.END:(Gödel 1931:39-41)

Gödel's footnote 15 is dodgy in that although it denies the circularity
of his proposition he affirms its circularity in the same paragraph that
he denies it:

Removing the dodgy words from the above.
a proposition...begins by asserting the unprovability of a wholly
determinate formula...this formula is precisely that by which the
proposition was itself expressed.

Paraphrasing the above using less clumsy words:
a proposition asserts the unprovability of a formula that expresses this
same proposition

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

>
>>> I think you don't even know what G is, but have only read the clift
>>> notes edition that actually explain it in the meta-theory.
>>
>>
>
> So this comment of mine is now proven.
>
> And you have prooved to be a Liar and an idiot, as you abolutely don't
> know what you are talking about.

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


devel / comp.lang.prolog / Re: Is this correct Prolog?

Pages:1234567
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor