Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Do molecular biologists wear designer genes?


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

SubjectAuthor
* Is this correct Prolog?olcott
+* Re: Is this correct Prolog?Richard Damon
|+* Re: Is this correct Prolog?olcott
||`* Re: Is this correct Prolog?Richard Damon
|| `* Re: Is this correct Prolog?olcott
||  `* Re: Is this correct Prolog?Richard Damon
||   `* Re: Is this correct Prolog?olcott
||    `* Re: Is this correct Prolog?Richard Damon
||     `* Re: Is this correct Prolog?olcott
||      +* Re: Is this correct Prolog?Jeff Barnett
||      |+* Re: Is this correct Prolog?olcott
||      ||`- Re: Is this correct Prolog?Richard Damon
||      |`* Re: Is this correct Prolog?Mr Flibble
||      | +- Re: Is this correct Prolog?polcott
||      | +- Re: Is this correct Prolog?Richard Damon
||      | `- Re: Is this correct Prolog?Jeff Barnett
||      +* Re: Is this correct Prolog?Richard Damon
||      |`* Re: Is this correct Prolog?olcott
||      | `- Re: Is this correct Prolog?Richard Damon
||      `* Re: Is this correct Prolog?olcott
||       `* Re: Is this correct Prolog?Richard Damon
||        `* Re: Is this correct Prolog?olcott
||         `- Re: Is this correct Prolog?Richard Damon
|`* Re: Is this correct Prolog?olcott
| `* Re: Is this correct Prolog?olcott
|  +* Re: Is this correct Prolog?olcott
|  |`* Re: Is this correct Prolog?olcott
|  | `* Re: Is this correct Prolog?olcott
|  |  +- Re: Is this correct Prolog?Richard Damon
|  |  `* Re: Is this correct Prolog?olcott
|  |   `* Re: Is this correct Prolog?André G. Isaak
|  |    `* Re: Is this correct Prolog?olcott
|  |     +- Re: Is this correct Prolog?Richard Damon
|  |     `* Re: Is this correct Prolog?olcott
|  |      +* Re: Is this correct Prolog?André G. Isaak
|  |      |+* Re: Is this correct Prolog?olcott
|  |      ||+* Re: Is this correct Prolog?Richard Damon
|  |      |||`* Re: Is this correct Prolog?olcott
|  |      ||| `* Re: Is this correct Prolog?Richard Damon
|  |      |||  +- Re: Is this correct Prolog?André G. Isaak
|  |      |||  `* Re: Is this correct Prolog?olcott
|  |      |||   `* Re: Is this correct Prolog?Richard Damon
|  |      |||    `* Re: Is this correct Prolog?olcott
|  |      |||     `* Re: Is this correct Prolog?Richard Damon
|  |      |||      `* Re: Is this correct Prolog?olcott
|  |      |||       +- Re: Is this correct Prolog?André G. Isaak
|  |      |||       `* Re: Is this correct Prolog?Richard Damon
|  |      |||        `* Re: Is this correct Prolog?olcott
|  |      |||         +- Re: Is this correct Prolog?André G. Isaak
|  |      |||         `* Re: Is this correct Prolog?Richard Damon
|  |      |||          `* Re: Is this correct Prolog?olcott
|  |      |||           `- Re: Is this correct Prolog?Richard Damon
|  |      ||`* Re: Is this correct Prolog?André G. Isaak
|  |      || +* Re: Is this correct Prolog?olcott
|  |      || |`* Re: Is this correct Prolog?André G. Isaak
|  |      || | `* Re: Is this correct Prolog? [ André is provenolcott
|  |      || |  `* Re: Is this correct Prolog? [ André is provenAndré G. Isaak
|  |      || |   `- Re: Is this correct Prolog? [ André is provenolcott
|  |      || `* Re: Is this correct Prolog? [ André is provenolcott
|  |      ||  `* Re: Is this correct Prolog? [ André is provenRichard Damon
|  |      ||   `- Re: Is this correct Prolog? [ André is provenolcott
|  |      |`- Re: Is this correct Prolog?olcott
|  |      `- Re: Is this correct Prolog?Richard Damon
|  `* Re: Is this correct Prolog?olcott
|   `- Re: Is this correct Prolog?André G. Isaak
+* Re: Is this correct Prolog?olcott
|`* Re: Is this correct Prolog?Richard Damon
| `* Re: Is this correct Prolog?olcott
|  `* Re: Is this correct Prolog?Richard Damon
|   `* Re: Is this correct Prolog?olcott
|    `- Re: Is this correct Prolog?Richard Damon
+* Re: Is this correct Prolog?olcott
|`* Re: Is this correct Prolog?Aleksy Grabowski
| `* Re: Is this correct Prolog?olcott
|  `* Re: Is this correct Prolog?Aleksy Grabowski
|   `* Re: Is this correct Prolog?olcott
|    `* Re: Is this correct Prolog?Aleksy Grabowski
|     `* Re: Is this correct Prolog?olcott
|      +* Re: Is this correct Prolog?Aleksy Grabowski
|      |`* Re: Is this correct Prolog?olcott
|      | `* Re: Is this correct Prolog?Aleksy Grabowski
|      |  `- Re: Is this correct Prolog?olcott
|      `* Re: Is this correct Prolog?Jeff Barnett
|       +* Re: Is this correct Prolog?Mr Flibble
|       |`- Re: Is this correct Prolog?olcott
|       `* Re: Is this correct Prolog?olcott
|        `* Re: Is this correct Prolog?Richard Damon
|         `* Re: Is this correct Prolog?Aleksy Grabowski
|          +* Re: Is this correct Prolog?Ben
|          |`* Re: Is this correct Prolog?olcott
|          | +* Re: Is this correct Prolog?Ben
|          | |`* Re: Is this correct Prolog?olcott
|          | | +* Re: Is this correct Prolog?Richard Damon
|          | | |`* Re: Is this correct Prolog? [ Tarski ]olcott
|          | | | `* Re: Is this correct Prolog? [ Tarski ]Richard Damon
|          | | |  +* Re: Is this correct Prolog? [ Tarski ]olcott
|          | | |  |`- Re: Is this correct Prolog? [ Tarski ]Richard Damon
|          | | |  `- Re: Is this correct Prolog? [ Tarski ]olcott
|          | | `- Re: Is this correct Prolog?Ben
|          | `* Re: Is this correct Prolog?André G. Isaak
|          |  +* Re: Is this correct Prolog?olcott
|          |  `* Re: Is this correct Prolog?Jeff Barnett
|          `* Re: Is this correct Prolog?olcott
`* Re: Is this correct Prolog?olcott

Pages:123456
Re: Is this correct Prolog?

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

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8655&group=comp.ai.philosophy#8655

 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: Rich...@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.novabbs.com/computers/article-flat.php?id=8657&group=comp.ai.philosophy#8657

 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: agis...@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.novabbs.com/computers/article-flat.php?id=8661&group=comp.ai.philosophy#8661

 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: polco...@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.novabbs.com/computers/article-flat.php?id=8663&group=comp.ai.philosophy#8663

 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: Rich...@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.novabbs.com/computers/article-flat.php?id=8664&group=comp.ai.philosophy#8664

 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: polco...@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.novabbs.com/computers/article-flat.php?id=8665&group=comp.ai.philosophy#8665

 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: Rich...@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.novabbs.com/computers/article-flat.php?id=8668&group=comp.ai.philosophy#8668

 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: polco...@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.novabbs.com/computers/article-flat.php?id=8678&group=comp.ai.philosophy#8678

 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: Rich...@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.novabbs.com/computers/article-flat.php?id=8681&group=comp.ai.philosophy#8681

 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: polco...@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

Pages:123456
server_pubkey.txt

rocksolid light 0.9.7
clearnet tor