Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

There are never any bugs you haven't found yet.


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

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

Pages:123456
Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Wed, 4 May 2022 11:27 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
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
View all headers

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.


Subject: Re: Is this correct Prolog?
From: André G. Isaak
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Christians and Atheists United Against Creeping Agnosticism
Date: Wed, 4 May 2022 14:02 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: 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
View all headers
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.


Subject: Re: Is this correct Prolog?
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Wed, 4 May 2022 19:01 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
Path: i2pn2.org!i2pn.org!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
View all headers
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


Subject: Re: Is this correct Prolog?
From: Richard Damon
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Wed, 4 May 2022 23:48 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
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
View all headers
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.


Subject: Re: Is this correct Prolog? [ Tarski ]
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Thu, 5 May 2022 02:30 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
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
View all headers
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


Subject: Re: Is this correct Prolog? [ Tarski ]
From: Richard Damon
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Thu, 5 May 2022 02:46 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
Path: i2pn2.org!i2pn.org!weretis.net!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
View all headers
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.






Subject: Re: Is this correct Prolog? [ Tarski ]
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Thu, 5 May 2022 03:02 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: 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
View all headers
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


Subject: Re: Is this correct Prolog? [ Tarski ]
From: Richard Damon
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Thu, 5 May 2022 11:41 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
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
View all headers
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.









Subject: Re: Is this correct Prolog? [ Tarski ]
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Thu, 5 May 2022 17:57 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: 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
View all headers
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


Subject: Re: Is this correct Prolog? [ Tarski ]
From: André G. Isaak
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Christians and Atheists United Against Creeping Agnosticism
Date: Thu, 5 May 2022 18:06 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
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? [ 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
View all headers
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.


Subject: Re: Is this correct Prolog? [ Tarski ]
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Followup: comp.theory
Organization: A noiseless patient Spider
Date: Thu, 5 May 2022 21:23 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
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 ]
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
View all headers
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


Subject: Re: Is this correct Prolog? [ Tarski ]
From: Richard Damon
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Fri, 6 May 2022 02:24 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
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: Rich...@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
View all headers
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.









Subject: Re: Is this correct Prolog? [ Tarski ]
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Fri, 6 May 2022 02:37 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
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 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
View all headers
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


Subject: Re: Is this correct Prolog? [ Tarski ]
From: Richard Damon
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: Forte - www.forteinc.com
Date: Fri, 6 May 2022 11:43 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
Path: i2pn2.org!i2pn.org!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: Rich...@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
View all headers

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.


Subject: Re: Is this correct Prolog? [ Tarski ]
From: olcott
Newsgroups: comp.theory, comp.lang.prolog, comp.ai.philosophy
Organization: A noiseless patient Spider
Date: Fri, 6 May 2022 20:29 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
Path: i2pn2.org!i2pn.org!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: 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
View all headers
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


Pages:123456
rocksolid light 0.7.2
clearneti2ptor