Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Computer programmers do it byte by byte.


devel / comp.theory / Re: Gödel's 1931 incompleteness fails HOL

SubjectAuthor
* Gödel's_1931_incompleteness_fails_HOLolcott
+- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
+* _Gödel's_1931_incompleteness_fails_HOLolcott
|+- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
|`* _Gödel's_1931_incompleteness_fails_HOLolcott
| +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| `* _Gödel's_1931_incompleteness_fails_HOLolcott
|  `- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
+* _Gödel's_1931_incompleteness_fails_HOLJim Burns
|`* _Gödel's_1931_incompleteness_fails_HOLolcott
| +* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |`* _Gödel's_1931_incompleteness_fails_HOLolcott
| | `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  +* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |`* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  | `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |  `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |   `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |    `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     +* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |+- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |`* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     | `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |  `* _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |   `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |    +* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |    |+* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |    ||`* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |    || `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |    ||  `- _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |    |`- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |    `* _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |     `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |      `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |       `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |        `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |         `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |          `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |           `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |            +* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |            |`- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |            `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |             +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |             `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |              +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |              `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |               +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |               `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |                +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |                +* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |                |+- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |                |`* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |                | +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |                | `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |                |  +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |                |  `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |                |   +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |                |   `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |                |    +- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |                |    `- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     |                `* _Gödel's_1931_incompleteness_fails_HOLJim Burns
| |  |     |                 `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |     |                  `- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  |     `* _Gödel's_1931_incompleteness_fails_HOLolcott
| |  |      `- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
| |  `- _Gödel's_1931_incompleteness_fails_HOLolcott
| `- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
`* _Gödel's_1931_incompleteness_fails_HOLolcott
 +* _Gödel's_1931_incompleteness_fails_HOLolcott
 |`- _Gödel's_1931_incompleteness_fails_HOLRichard Damon
 `- _Gödel's_1931_incompleteness_fails_HOLRichard Damon

Pages:123
Re: Gödel's 1931 incompleteness fails HOL

<uklrug$3kd8a$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49869&group=comp.theory#49869

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Mon, 4 Dec 2023 18:47:12 -0600
Organization: A noiseless patient Spider
Lines: 29
Message-ID: <uklrug$3kd8a$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me> <uklpt4$3k6gl$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 00:47:12 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="395a5d53b4153ba20be0c11dc6943f7b";
logging-data="3814666"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX198kP8X3ZR7XjZNJ2XUr0du"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:u75PZLz4qSJnTkqCC4aWWLDybMw=
Content-Language: en-US
In-Reply-To: <uklpt4$3k6gl$1@dont-email.me>
 by: olcott - Tue, 5 Dec 2023 00:47 UTC

On 12/4/2023 6:12 PM, olcott wrote:
> On 12/2/2023 6:22 PM, olcott wrote:
>> When PA is the n level of logic and metamathematics is the n+1 level of
>> logic in the same formal system then G <is> provable in this formal
>> system and incompleteness cannot exist. HOL can do this.
>>
>> This sentence is not true: "This sentence is not true" is true.
>> The above is all there is to the Tarski Undefinability Theorem.
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>
> ...14 Every epistemological antinomy can likewise be used
> for a similar undecidability proof...(Gödel 1931:43-44)
>
> Dishonest people can "interpret" this as saying everyone
> knows that no one can ever base any formal proof on any
> epistemological antinomy.
>
> *the direct opposite of what he actually says*
>

If
epistemological antinomies are not members of most Formal Systems Language.

Then Gödel was that much more stupid for saying this.
--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

Re: Gödel's 1931 incompleteness fails HOL

<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49870&group=comp.theory#49870

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Mon, 4 Dec 2023 19:49:11 -0500
Organization: A noiseless patient Spider
Lines: 57
Message-ID: <a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="7daa99b37c1d7dd53a43f9bc7beed0ae";
logging-data="3816363"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+rWhjv0Kps1QduA8lS+Zmd3VGbsV1mXTw="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:JK1naWopuKXWsUMpk49Bip6XRyo=
Content-Language: en-US
In-Reply-To: <ukliag$3j59q$1@dont-email.me>
 by: Jim Burns - Tue, 5 Dec 2023 00:49 UTC

On 12/4/2023 5:02 PM, olcott wrote:
> On 12/4/2023 8:15 AM, Jim Burns wrote:
>> On 12/4/2023 12:01 AM, olcott wrote:

>>> *Thus proving a cycle in its evaluation graph*
>>
>> G(g)
>> Show me a cycle.

> One can make any idea sufficiently convoluted
> to make it incomprehensible.

I can try to make each step more comprehensible,
and take more, shorter steps.

Be aware that there may be a trade-off, though.
More short steps may well be less comprehensible
than fewer broad sweeps which clue one in on
how to think about this.

if
Subst("H(u)","H(u)",y)
is true, then
y = "H("H(u)")"

if
¬∃z:Provesˢᵗ(z,"H("H(u)")")
is true, then
H("H(u)") is not ST.provable.

if
∃y(Subst("H(u)","H(u)",y) ∧ ¬∃z:Provesˢᵗ(z,y)))
is true, then
y = "H("H(u)")" exists and
"H("H(u)") is not ST.provable

Abbreviate
G(u) := ∃y(Subst(u,u,y) ∧ ¬∃z:Provesˢᵗ(z,y)))

if
G("H(u)")
is true, then
y = "H("H(u)")" exists and
H("H(u)") is not ST.provable

if
G("G(u)")
is true, then
y = "G("G(u)")" exists and
G("G(u)") is not ST.provable

tl;dr
if G("G(u)") is true
then G("G(u)") is not ST.provable

Re: Gödel's 1931 incompleteness fails HOL

<uklsms$3khan$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49871&group=comp.theory#49871

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!paganini.bofh.team!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Mon, 4 Dec 2023 19:00:12 -0600
Organization: A noiseless patient Spider
Lines: 65
Message-ID: <uklsms$3khan$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 01:00:13 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="395a5d53b4153ba20be0c11dc6943f7b";
logging-data="3818839"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19BsmT/3n9n28AGaGc41adH"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:BYwG+oXOjbOs6oobSgKY7nJy/RM=
Content-Language: en-US
In-Reply-To: <a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net>
 by: olcott - Tue, 5 Dec 2023 01:00 UTC

On 12/4/2023 6:49 PM, Jim Burns wrote:
> On 12/4/2023 5:02 PM, olcott wrote:
>> On 12/4/2023 8:15 AM, Jim Burns wrote:
>>> On 12/4/2023 12:01 AM, olcott wrote:
>
>>>> *Thus proving a cycle in its evaluation graph*
>>>
>>> G(g)
>>> Show me a cycle.
>
>> One can make any idea sufficiently convoluted
>> to make it incomprehensible.
>
> I can try to make each step more comprehensible,
> and take more, shorter steps.
>
> Be aware that there may be a trade-off, though.
> More short steps may well be less comprehensible
> than fewer broad sweeps which clue one in on
> how to think about this.
>
> if
> Subst("H(u)","H(u)",y)
> is true, then
> y = "H("H(u)")"
>
> if
> ¬∃z:Provesˢᵗ(z,"H("H(u)")")
> is true, then
> H("H(u)") is not ST.provable.
>
> if
> ∃y(Subst("H(u)","H(u)",y) ∧ ¬∃z:Provesˢᵗ(z,y)))
> is true, then
> y = "H("H(u)")" exists  and
> "H("H(u)") is not ST.provable
>
> Abbreviate
> G(u) := ∃y(Subst(u,u,y) ∧ ¬∃z:Provesˢᵗ(z,y)))
>
> if
> G("H(u)")
> is true, then
> y = "H("H(u)")" exists  and
> H("H(u)") is not ST.provable
>
> if
> G("G(u)")
> is true, then
> y = "G("G(u)")" exists  and
> G("G(u)") is not ST.provable
>
>
> tl;dr
> if G("G(u)") is true
> then G("G(u)") is not ST.provable
>
>

Until you get down to "G is unprovable in F"
we cannot build its proof tree.
--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

Re: Gödel's 1931 incompleteness fails HOL

<uklv93$2trsp$1@i2pn2.org>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49872&group=comp.theory#49872

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!.POSTED!not-for-mail
From: rich...@damon-family.org (Richard Damon)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Mon, 4 Dec 2023 20:44:03 -0500
Organization: i2pn2 (i2pn.org)
Message-ID: <uklv93$2trsp$1@i2pn2.org>
References: <ukghnk$2i6q1$2@dont-email.me> <uklpt4$3k6gl$1@dont-email.me>
<uklrug$3kd8a$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 01:44:03 -0000 (UTC)
Injection-Info: i2pn2.org;
logging-data="3075993"; mail-complaints-to="usenet@i2pn2.org";
posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
In-Reply-To: <uklrug$3kd8a$1@dont-email.me>
Content-Language: en-US
 by: Richard Damon - Tue, 5 Dec 2023 01:44 UTC

On 12/4/23 7:47 PM, olcott wrote:
> On 12/4/2023 6:12 PM, olcott wrote:
>> On 12/2/2023 6:22 PM, olcott wrote:
>>> When PA is the n level of logic and metamathematics is the n+1 level of
>>> logic in the same formal system then G <is> provable in this formal
>>> system and incompleteness cannot exist. HOL can do this.
>>>
>>> This sentence is not true: "This sentence is not true" is true.
>>> The above is all there is to the Tarski Undefinability Theorem.
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>
>> ...14 Every epistemological antinomy can likewise be used
>> for a similar undecidability proof...(Gödel 1931:43-44)
>>
>> Dishonest people can "interpret" this as saying everyone
>> knows that no one can ever base any formal proof on any
>> epistemological antinomy.
>>
>> *the direct opposite of what he actually says*
>>
>
> If
> epistemological antinomies are not members of most Formal Systems Language.
>
> Then Gödel was that much more stupid for saying this.

He never said the epistemological antinomy was a member of the Formal
System Language.

Try to show where he did.

You are just apparently too stupid to understand wha the is saying,

Re: Gödel's 1931 incompleteness fails HOL

<uklv96$2trsp$2@i2pn2.org>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49873&group=comp.theory#49873

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!.POSTED!not-for-mail
From: rich...@damon-family.org (Richard Damon)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Mon, 4 Dec 2023 20:44:05 -0500
Organization: i2pn2 (i2pn.org)
Message-ID: <uklv96$2trsp$2@i2pn2.org>
References: <ukghnk$2i6q1$2@dont-email.me> <uklpt4$3k6gl$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 01:44:06 -0000 (UTC)
Injection-Info: i2pn2.org;
logging-data="3075993"; mail-complaints-to="usenet@i2pn2.org";
posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <uklpt4$3k6gl$1@dont-email.me>
 by: Richard Damon - Tue, 5 Dec 2023 01:44 UTC

On 12/4/23 7:12 PM, olcott wrote:
> On 12/2/2023 6:22 PM, olcott wrote:
>> When PA is the n level of logic and metamathematics is the n+1 level of
>> logic in the same formal system then G <is> provable in this formal
>> system and incompleteness cannot exist. HOL can do this.
>>
>> This sentence is not true: "This sentence is not true" is true.
>> The above is all there is to the Tarski Undefinability Theorem.
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>
> ...14 Every epistemological antinomy can likewise be used
> for a similar undecidability proof...(Gödel 1931:43-44)
>
> Dishonest people can "interpret" this as saying everyone
> knows that no one can ever base any formal proof on any
> epistemological antinomy.
>
> *the direct opposite of what he actually says*
>

So, you are agreing that your own "proof" is incorrect, as you can't
base a proof on an epistemological antinomy, which you just did (at
least to a similar degree as Godel did).

Re: Gödel's 1931 incompleteness fails HOL

<uklv98$2trsp$3@i2pn2.org>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49874&group=comp.theory#49874

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!.POSTED!not-for-mail
From: rich...@damon-family.org (Richard Damon)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Mon, 4 Dec 2023 20:44:07 -0500
Organization: i2pn2 (i2pn.org)
Message-ID: <uklv98$2trsp$3@i2pn2.org>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <uklplq$3k4ul$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 01:44:08 -0000 (UTC)
Injection-Info: i2pn2.org;
logging-data="3075993"; mail-complaints-to="usenet@i2pn2.org";
posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
In-Reply-To: <uklplq$3k4ul$1@dont-email.me>
Content-Language: en-US
 by: Richard Damon - Tue, 5 Dec 2023 01:44 UTC

On 12/4/23 7:08 PM, olcott wrote:
> On 12/4/2023 8:15 AM, Jim Burns wrote:
>> On 12/4/2023 12:01 AM, olcott wrote:
>>> On 12/3/2023 9:57 PM, Jim Burns wrote:
>>
>>>> [...]
>>>
>>> https://en.wikipedia.org/wiki/Quine%27s_paradox
>>> A convoluted mess that
>>> is indirectly rather than directly
>>> self-referential.
>>>
>>> | The statement
>>> | "'yields falsehood when preceded by its quotation'
>>> | yields falsehood when preceded by its quotation"
>>> | is false.
>>
>> G(x) :⇔ ∃y(Subst(x,x,y) ∧ ¬∃z:STProves(z,y)))
>>
>> ST is: Empty.Set, Adjunct, Extensionality.
>>
>> h := "H(x)"
>>
>> G(h) means
>> | H(x) preceded by its quotation
>> | is not ST.provable.
>>
>> g := "G(x)" ≠ "G(g)"
>>
>> G(g) means
>> | G(x) preceded by its quotation
>> | is not ST.provable.
>>
>> !
>> G(g) is G(x) preceded by its quotation.
>> or,
>> being cute,
>> | "preceded by its quotation
>> | is not ST.provable"
>> | preceded by its quotation
>> | is not ST.provable.
>>
>> If G(g) is true, G(g) is not ST.provable.
>> g refers to G(x) not G(g)
>>
>>> | In other words,
>>> | the sentence implies that it is false,
>>
>> G(g) implies that G(g) is not ST.provable.
>> false ≠ not ST.provable
>>
>>> | which is paradoxical
>>> | —for if it is false,
>>> | what it states is in fact true.
>>
>> Incomplete ST is not paradoxical,
>> not even if you say it is
>> a hundred times.
>>
>>> *Thus proving a cycle in its evaluation graph*
>>
>> G(g)
>> Show me a cycle.
>>
>>> All proves are directed paths
>>> from leaves to a root.
>>
>> ...which is what I've been saying,
>> calling the root
>> description of the topic-of-the-day and
>> calling the leaves
>> not-first-false claims augmenting
>> the description.
>>
>> The finiteness of paths from leaves
>> back to root is implicit in
>> their being attached.
>>
>>
>
> When we boil Gödel's 75 levels of indirection down to what he
> is expressing in a language woefully insufficiently expressive
> to say this he is saying:
>
> ...We are therefore confronted with a proposition which asserts its own
> unprovability. 15 ...(Gödel 1931:43-44)
>

Which you still don't understand what he is saying.

> This does have a cycle---> G := (F ⊬ G)
>

Which isn't what his G is, so you are just proving yourself to be a bald
face liar.

If you disagree, show where he ACTUALLY SAYS That is what G is.

If you quote that statement again, and don't show how its context
actually means what you claim, you will just contionuie to prove
yourself to be just a stupid liar.

Re: Gödel's 1931 incompleteness fails HOL

<uklv9a$2trsp$4@i2pn2.org>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49875&group=comp.theory#49875

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!.POSTED!not-for-mail
From: rich...@damon-family.org (Richard Damon)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Mon, 4 Dec 2023 20:44:09 -0500
Organization: i2pn2 (i2pn.org)
Message-ID: <uklv9a$2trsp$4@i2pn2.org>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 01:44:10 -0000 (UTC)
Injection-Info: i2pn2.org;
logging-data="3075993"; mail-complaints-to="usenet@i2pn2.org";
posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <uklsms$3khan$1@dont-email.me>
 by: Richard Damon - Tue, 5 Dec 2023 01:44 UTC

On 12/4/23 8:00 PM, olcott wrote:
> On 12/4/2023 6:49 PM, Jim Burns wrote:
>> On 12/4/2023 5:02 PM, olcott wrote:
>>> On 12/4/2023 8:15 AM, Jim Burns wrote:
>>>> On 12/4/2023 12:01 AM, olcott wrote:
>>
>>>>> *Thus proving a cycle in its evaluation graph*
>>>>
>>>> G(g)
>>>> Show me a cycle.
>>
>>> One can make any idea sufficiently convoluted
>>> to make it incomprehensible.
>>
>> I can try to make each step more comprehensible,
>> and take more, shorter steps.
>>
>> Be aware that there may be a trade-off, though.
>> More short steps may well be less comprehensible
>> than fewer broad sweeps which clue one in on
>> how to think about this.
>>
>> if
>> Subst("H(u)","H(u)",y)
>> is true, then
>> y = "H("H(u)")"
>>
>> if
>> ¬∃z:Provesˢᵗ(z,"H("H(u)")")
>> is true, then
>> H("H(u)") is not ST.provable.
>>
>> if
>> ∃y(Subst("H(u)","H(u)",y) ∧ ¬∃z:Provesˢᵗ(z,y)))
>> is true, then
>> y = "H("H(u)")" exists  and
>> "H("H(u)") is not ST.provable
>>
>> Abbreviate
>> G(u) := ∃y(Subst(u,u,y) ∧ ¬∃z:Provesˢᵗ(z,y)))
>>
>> if
>> G("H(u)")
>> is true, then
>> y = "H("H(u)")" exists  and
>> H("H(u)") is not ST.provable
>>
>> if
>> G("G(u)")
>> is true, then
>> y = "G("G(u)")" exists  and
>> G("G(u)") is not ST.provable
>>
>>
>> tl;dr
>> if G("G(u)") is true
>> then G("G(u)") is not ST.provable
>>
>>
>
> Until you get down to "G is unprovable in F"
> we cannot build its proof tree.

Except that since that ISN'T the statment of G, we don't need that
statement.

The statement of G is: "There does not exist a Natural Number g that
statisfies <a particular Primative Recursive Relationship>"

There exist a proof tree for that (which is infinite in length) in F,
since that relationship can be computed for every Natural Number, and it
turns out that all the answers are that none of the numbers satisfies
the relationship. Thus, the statement IS true.

The fact that none of the numbers satisfies the relationship can't be
determined in F, except by testing every number individually, which,
because there is an infinite number of numbers, says that can't be the
needed finite proof.

It DOES turn out that in Meta-F, because of its additional knowledge
about the Primitive Recursive Relationship, we can prove that there, in
fact, is no number that matches the relationship, and by the nature of
the meta-relationship between F and meta-F, we establish that it also
must be true in F itself (because the relationship doesn't change).

So, we do have the tree in F, but it is infinite, so not a proof (since
the incompleteness thereom is for Formal System, which as true for most
normal systems, define "Proofs" as FINITE arguments.

Re: Gödel's 1931 incompleteness fails HOL

<7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49876&group=comp.theory#49876

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Tue, 5 Dec 2023 12:52:34 -0500
Organization: A noiseless patient Spider
Lines: 67
Message-ID: <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="77fa17b2017a76d347ca8155aaa666e6";
logging-data="275426"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+duz62TN8uPeubbANjfd20SMBdDFwAHxY="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:mg8WmUG3z1lkfz/Odg+Om3zgn/k=
Content-Language: en-US
In-Reply-To: <uklv9a$2trsp$4@i2pn2.org>
 by: Jim Burns - Tue, 5 Dec 2023 17:52 UTC

On 12/4/2023 8:44 PM, Richard Damon wrote:
> On 12/4/23 8:00 PM, olcott wrote:
>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>> tl;dr
>>> if G("G(u)") is true
>>> then G("G(u)") is not ST.provable

ST has {}, x∪{y}, and set equality.

>> Until you get down to "G is unprovable in F"
>> we cannot build its proof tree.
>
> Except that since that ISN'T the statment of G,
> we don't need that statement.
>
> The statement of G is:
> "There does not exist
> a Natural Number g that statisfies
> <a particular Primative Recursive Relationship>"
>
> There exist a proof tree for that
> (which is infinite in length) in F,
> since that relationship can be computed
> for every Natural Number,
> and it turns out that
> all the answers are that
> none of the numbers satisfies the relationship.
> Thus, the statement IS true.
>
> The fact that
> none of the numbers satisfies the relationship
> can't be determined in F, except by
> testing every number individually, which,
> because there is an infinite number of numbers,
> says that can't be the needed finite proof.

What is F ?
Is F True Arithmetic?
https://en.wikipedia.org/wiki/True_arithmetic

True Arithmetic takes infinitely-many sentences
as axioms. True Arithmetic is not a counter-
example to Gödel's reasoning.

What Olcott wants still seems to be a
massive-database of all human knowledge,
complete, of course, and
PO sees Gödel's reasoning as what prevents that,
somehow, and
he sees that complete massive-database
as essential to True AI and
True AI as essential to humanity.

I do not guarantee that my recollection is
100% correct or thoroughly up-to-date.

However, assuming IRC,
True Arithmetic does not serve Olcott's purpose
because
the most massively massive of massive-databases
is still finite, unlike True Arithmetic.

However,
I'm not sure what F means here.

Re: Gödel's 1931 incompleteness fails HOL

<ukntos$c9d6$2@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49877&group=comp.theory#49877

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Tue, 5 Dec 2023 13:30:36 -0600
Organization: A noiseless patient Spider
Lines: 74
Message-ID: <ukntos$c9d6$2@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 19:30:37 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="395a5d53b4153ba20be0c11dc6943f7b";
logging-data="402854"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19PiMfF19bwfg+h7u3fMAHr"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:eY8ozIcurRDv9GnmYaOQy8ze2gw=
In-Reply-To: <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
Content-Language: en-US
 by: olcott - Tue, 5 Dec 2023 19:30 UTC

On 12/5/2023 11:52 AM, Jim Burns wrote:
> On 12/4/2023 8:44 PM, Richard Damon wrote:
>> On 12/4/23 8:00 PM, olcott wrote:
>>> On 12/4/2023 6:49 PM, Jim Burns wrote:
>
>>>> tl;dr
>>>> if G("G(u)") is true
>>>> then G("G(u)") is not ST.provable
>
> ST has {}, x∪{y}, and set equality.
>
>>> Until you get down to "G is unprovable in F"
>>> we cannot build its proof tree.
>>
>> Except that since that ISN'T the statment of G,
>> we don't need that statement.
>>
>> The statement of G is:
>> "There does not exist
>> a Natural Number g that statisfies
>> <a particular Primative Recursive Relationship>"
>>
>> There exist a proof tree for that
>> (which is infinite in length) in F, since that relationship can be
>> computed
>> for every Natural Number,
>> and it turns out that
>> all the answers are that
>> none of the numbers satisfies the relationship.
>> Thus, the statement IS true.
>>
>> The fact that
>> none of the numbers satisfies the relationship
>> can't be determined in F, except by
>> testing every number individually, which, because there is an infinite
>> number of numbers,
>> says that can't be the needed finite proof.
>
> What is F ?
> Is F True Arithmetic?
> https://en.wikipedia.org/wiki/True_arithmetic
>
> True Arithmetic takes infinitely-many sentences
> as axioms. True Arithmetic is not a counter-
> example to Gödel's reasoning.
>
> What Olcott wants still seems to be a
> massive-database of all human knowledge,
> complete, of course,  and
> PO sees Gödel's reasoning as what prevents that,
> somehow,  and
> he sees that complete massive-database
> as essential to True AI  and
> True AI as essential to humanity.

∀L ∈ Formal_System ∀x ∈ Language(L)
True(L,x) ≡ (T ⊢ x)
False(L,x) ≡ (T ⊢ ¬x)
Eliminates Tarski undefinability and Gödel incompleteness and forces the
concept of truth in math and logic to conform to the way that it works
everywhere else. True(x) ≡ (⊢ x)

The only way that we know that "cats are animals" is true is the
connection from the above expression to the definition of {cats} and
{animals}.

The lack of inference steps from axioms to an expression simply means
untrue. Incomplete(L) is merely a terribly misleading euphemism for
~True(L,x).

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

Re: Gödel's 1931 incompleteness fails HOL

<3c295e8f-39ec-45db-a95f-1183d46ecc0b@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49878&group=comp.theory#49878

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!rocksolid2!news.neodome.net!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Tue, 5 Dec 2023 14:58:55 -0500
Organization: A noiseless patient Spider
Lines: 28
Message-ID: <3c295e8f-39ec-45db-a95f-1183d46ecc0b@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<ukntos$c9d6$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="77fa17b2017a76d347ca8155aaa666e6";
logging-data="410999"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+FAE07+e+bq4MQa7sv43XfkSMH8QPXZbM="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:0MV+pLFE8ocoK3HtvcdLHGNExg0=
Content-Language: en-US
In-Reply-To: <ukntos$c9d6$2@dont-email.me>
 by: Jim Burns - Tue, 5 Dec 2023 19:58 UTC

On 12/5/2023 2:30 PM, olcott wrote:
> On 12/5/2023 11:52 AM, Jim Burns wrote:
>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>> On 12/4/23 8:00 PM, olcott wrote:
>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>>>> tl;dr
>>>>> if G("G(u)") is true
>>>>> then G("G(u)") is not ST.provable
>>
>> ST has {}, x∪{y}, and set equality.
>>
>>>> Until you get down to "G is unprovable in F"
>>>> we cannot build its proof tree.

>> he sees that complete massive-database
>> as essential to True AI  and
>> True AI as essential to humanity.
>
> ∀L ∈ Formal_System ∀x ∈ Language(L)
> True(L,x) ≡ (T ⊢ x)
> False(L,x) ≡ (T ⊢ ¬x)

What is F ?

Do I have your motivation correct?

Re: Gödel's 1931 incompleteness fails HOL

<uko023$ckmc$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49879&group=comp.theory#49879

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Tue, 5 Dec 2023 14:09:39 -0600
Organization: A noiseless patient Spider
Lines: 37
Message-ID: <uko023$ckmc$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<ukntos$c9d6$2@dont-email.me> <3c295e8f-39ec-45db-a95f-1183d46ecc0b@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 20:09:39 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="395a5d53b4153ba20be0c11dc6943f7b";
logging-data="414412"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18jAAH8VeuLr0jLe6NIW1EW"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:QSA+I68cA1Mv6DdbpAzfqEs7JOQ=
In-Reply-To: <3c295e8f-39ec-45db-a95f-1183d46ecc0b@att.net>
Content-Language: en-US
 by: olcott - Tue, 5 Dec 2023 20:09 UTC

On 12/5/2023 1:58 PM, Jim Burns wrote:
> On 12/5/2023 2:30 PM, olcott wrote:
>> On 12/5/2023 11:52 AM, Jim Burns wrote:
>>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>>> On 12/4/23 8:00 PM, olcott wrote:
>>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:
>
>>>>>> tl;dr
>>>>>> if G("G(u)") is true
>>>>>> then G("G(u)") is not ST.provable
>>>
>>> ST has {}, x∪{y}, and set equality.
>>>
>>>>> Until you get down to "G is unprovable in F"
>>>>> we cannot build its proof tree.
>
>>> he sees that complete massive-database
>>> as essential to True AI  and
>>> True AI as essential to humanity.
>>
>> ∀L ∈ Formal_System ∀x ∈ Language(L)
>> True(L,x) ≡ (T ⊢ x)
>> False(L,x) ≡ (T ⊢ ¬x)
>
> What is F ?
>
> Do I have your motivation correct?
>
>

F is the formal system that encodes Gödel’s G
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom

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

Re: Gödel's 1931 incompleteness fails HOL

<e009b720-9431-466c-a71c-dc6265196228@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49880&group=comp.theory#49880

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Tue, 5 Dec 2023 16:28:57 -0500
Organization: A noiseless patient Spider
Lines: 62
Message-ID: <e009b720-9431-466c-a71c-dc6265196228@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<ukntos$c9d6$2@dont-email.me> <3c295e8f-39ec-45db-a95f-1183d46ecc0b@att.net>
<uko023$ckmc$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="77fa17b2017a76d347ca8155aaa666e6";
logging-data="437961"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19pCJqrOhuPL342Zr6WuP/9KjXSwF9N1zA="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:NZUBPmgm78xUe1zwD47jPBtD1pY=
In-Reply-To: <uko023$ckmc$1@dont-email.me>
Content-Language: en-US
 by: Jim Burns - Tue, 5 Dec 2023 21:28 UTC

On 12/5/2023 3:09 PM, olcott wrote:
> On 12/5/2023 1:58 PM, Jim Burns wrote:
>> On 12/5/2023 2:30 PM, olcott wrote:
>>> On 12/5/2023 11:52 AM, Jim Burns wrote:
>>>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>>>> On 12/4/23 8:00 PM, olcott wrote:
>>>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>>>>>> tl;dr
>>>>>>> if G("G(u)") is true
>>>>>>> then G("G(u)") is not ST.provable
>>>>
>>>> ST has {}, x∪{y}, and set equality.

>>>>>> Until you get down to
>>>>>> "G is unprovable in F"
>>>>>> we cannot build its proof tree.

>> What is F ?

> F is the formal system that encodes Gödel’s G
> https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom

Thank you.

IIRC, the 1931 paper calls it P.
It is(?) a variation on the system PM in
_Principia Mathematica_

I'm not complaining about your calling it F
I just trying to to understand you.

I'm working with a much smaller axiom set,
the one for ST: {}, x∪{y}, and set equality.

ST is the system which I want to prove is
incomplete or inconsistent.

ST is still an important result, as small as
it is, because it is straightforward to
generalize the proof of ST's incompleteness
to a proof for systems which ST can describe.
And what ST can describe is Vast.

I know: that's not exactly how Godel's proof
goes. But the important thing is my proof goes.
My hope is that, shown multiple versions, you
will be able to triangulate on why it goes.

>>>> he sees that complete massive-database
>>>> as essential to True AI and
>>>> True AI as essential to humanity.
>>>
>>> ∀L ∈ Formal_System ∀x ∈ Language(L)
>>> True(L,x) ≡ (T ⊢ x)
>>> False(L,x) ≡ (T ⊢ ¬x)

>> Do I have your motivation correct?

Do I have your motivation correct?

Re: Gödel's 1931 incompleteness fails HOL

<uko88j$dsm2$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49881&group=comp.theory#49881

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Tue, 5 Dec 2023 16:29:38 -0600
Organization: A noiseless patient Spider
Lines: 99
Message-ID: <uko88j$dsm2$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<ukntos$c9d6$2@dont-email.me> <3c295e8f-39ec-45db-a95f-1183d46ecc0b@att.net>
<uko023$ckmc$1@dont-email.me> <e009b720-9431-466c-a71c-dc6265196228@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 22:29:40 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="395a5d53b4153ba20be0c11dc6943f7b";
logging-data="455362"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18OozWspf1clt8TBUSCTI4X"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:aCOQbjuv8RmOXk1Arso36VamCYc=
In-Reply-To: <e009b720-9431-466c-a71c-dc6265196228@att.net>
Content-Language: en-US
 by: olcott - Tue, 5 Dec 2023 22:29 UTC

On 12/5/2023 3:28 PM, Jim Burns wrote:
> On 12/5/2023 3:09 PM, olcott wrote:
>> On 12/5/2023 1:58 PM, Jim Burns wrote:
>>> On 12/5/2023 2:30 PM, olcott wrote:
>>>> On 12/5/2023 11:52 AM, Jim Burns wrote:
>>>>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>>>>> On 12/4/23 8:00 PM, olcott wrote:
>>>>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:
>
>>>>>>>> tl;dr
>>>>>>>> if G("G(u)") is true
>>>>>>>> then G("G(u)") is not ST.provable
>>>>>
>>>>> ST has {}, x∪{y}, and set equality.
>
>>>>>>> Until you get down to
>>>>>>> "G is unprovable in F"
>>>>>>> we cannot build its proof tree.
>
>>> What is F ?
>
>> F is the formal system that encodes Gödel’s G
>> https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
>
> Thank you.
>
> IIRC, the 1931 paper calls it P.
> It is(?) a variation on the system PM in
> _Principia Mathematica_
>
> I'm not complaining about your calling it F
> I just trying to to understand you.
>
> I'm working with a much smaller axiom set,
> the one for ST: {}, x∪{y}, and set equality.
>
> ST is the system which I want to prove is
> incomplete or inconsistent.
>
> ST is still an important result, as small as
> it is, because it is straightforward to
> generalize the proof of ST's incompleteness
> to a proof for systems which ST can describe.
> And what ST can describe is Vast.
>
> I know: that's not exactly how Godel's proof
> goes. But the important thing is my proof goes.
> My hope is that, shown multiple versions, you
> will be able to triangulate on why it goes.
>
>>>>> he sees that complete massive-database
>>>>> as essential to True AI  and
>>>>> True AI as essential to humanity.
>>>>
>>>> ∀L ∈ Formal_System ∀x ∈ Language(L)
>>>> True(L,x) ≡ (T ⊢ x)
>>>> False(L,x) ≡ (T ⊢ ¬x)
>
>>> Do I have your motivation correct?
>
> Do I have your motivation correct?

∀L ∈ Formal_System ∀x ∈ Language(L)
True(L,x) ≡ (T ⊢ x)
False(L,x) ≡ (T ⊢ ¬x)

Eliminates Tarski undefinability and Gödel incompleteness and forces the
concept of truth in math and logic to conform to the way that it works
everywhere else in the body of human knowledge: True(x) ≡ (⊢ x)

This makes it possible for a formal axiomatic system to eventually
get on social media and argue against the two most dangerous lies
about election fraud and climate change at every language level so
that the liars look like ridiculous fools even to themselves.

When everyone in the world believes that there is no objective
and consistent measure of True(x) (Tarski proof) this is impossible.

The reasonably possible alternative is that humanity becomes
extinct simply because some people wanted to chase after one
more dollar bill.

My paper bypasses most of the climate change lies by anchoring
itself in direct measurements of CO2 for the last 800,000 years,
These direct measurements cannot be biased.

My paper shows several different measure of a huge spike in CO2 since
1950. The next fastest spike in 800,000 years took 7,500 years.

Severe anthropogenic climate change proven entirely with verifiable facts

https://www.researchgate.net/publication/336568434_Severe_anthropogenic_climate_change_proven_entirely_with_verifiable_facts

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

Re: Gödel's 1931 incompleteness fails HOL

<ukocbu$2trsp$5@i2pn2.org>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49882&group=comp.theory#49882

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!.POSTED!not-for-mail
From: rich...@damon-family.org (Richard Damon)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Tue, 5 Dec 2023 18:39:42 -0500
Organization: i2pn2 (i2pn.org)
Message-ID: <ukocbu$2trsp$5@i2pn2.org>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<ukntos$c9d6$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 5 Dec 2023 23:39:42 -0000 (UTC)
Injection-Info: i2pn2.org;
logging-data="3075993"; mail-complaints-to="usenet@i2pn2.org";
posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <ukntos$c9d6$2@dont-email.me>
 by: Richard Damon - Tue, 5 Dec 2023 23:39 UTC

On 12/5/23 2:30 PM, olcott wrote:

> ∀L ∈ Formal_System ∀x ∈ Language(L)
> True(L,x) ≡ (T ⊢ x)
> False(L,x) ≡ (T ⊢ ¬x)
> Eliminates Tarski undefinability and Gödel incompleteness and forces the
> concept of truth in math and logic to conform to the way that it works
> everywhere else. True(x) ≡ (⊢ x)
>
> The only way that we know that "cats are animals" is true is the
> connection from the above expression to the definition of {cats} and
> {animals}.
>
> The lack of inference steps from axioms to an expression simply means
> untrue. Incomplete(L) is merely a terribly misleading euphemism for
> ~True(L,x).
>

And means that we can't have the Natural Numbers or anything higher.

So, you are just defining that Your idea of logic is too small to be useful.

Prove otherwise.

(Hint, if you have the Natural Numbers, then Godel's proof applies, and
proves there is either a statement that is True but not Provable, or
your system is inconsistent)

This just goes back your you lack of understand of how logic actually works.

Note, it also means you don't even know the meaning of the word "True"
in Natural Language, as things can be "True" even if not provable.

They can't be "Known True", but they can be "True"

You don't seem to understand the difference, probably because you don't
understand what Knowledge is.

Re: Gödel's 1931 incompleteness fails HOL

<TZQbN.95066$%d2c.83651@fx08.iad>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49883&group=comp.theory#49883

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!fx08.iad.POSTED!not-for-mail
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Content-Language: en-US
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
From: Rich...@Damon-Family.org (Richard Damon)
In-Reply-To: <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 88
Message-ID: <TZQbN.95066$%d2c.83651@fx08.iad>
X-Complaints-To: abuse@easynews.com
Organization: Forte - www.forteinc.com
X-Complaints-Info: Please be sure to forward a copy of ALL headers otherwise we will be unable to process your complaint properly.
Date: Tue, 5 Dec 2023 21:26:57 -0500
X-Received-Bytes: 4635
 by: Richard Damon - Wed, 6 Dec 2023 02:26 UTC

On 12/5/23 12:52 PM, Jim Burns wrote:
> On 12/4/2023 8:44 PM, Richard Damon wrote:
>> On 12/4/23 8:00 PM, olcott wrote:
>>> On 12/4/2023 6:49 PM, Jim Burns wrote:
>
>>>> tl;dr
>>>> if G("G(u)") is true
>>>> then G("G(u)") is not ST.provable
>
> ST has {}, x∪{y}, and set equality.
>
>>> Until you get down to "G is unprovable in F"
>>> we cannot build its proof tree.
>>
>> Except that since that ISN'T the statment of G,
>> we don't need that statement.
>>
>> The statement of G is:
>> "There does not exist
>> a Natural Number g that statisfies
>> <a particular Primative Recursive Relationship>"
>>
>> There exist a proof tree for that
>> (which is infinite in length) in F, since that relationship can be
>> computed
>> for every Natural Number,
>> and it turns out that
>> all the answers are that
>> none of the numbers satisfies the relationship.
>> Thus, the statement IS true.
>>
>> The fact that
>> none of the numbers satisfies the relationship
>> can't be determined in F, except by
>> testing every number individually, which, because there is an infinite
>> number of numbers,
>> says that can't be the needed finite proof.
>
> What is F ?
> Is F True Arithmetic?
> https://en.wikipedia.org/wiki/True_arithmetic
>
> True Arithmetic takes infinitely-many sentences
> as axioms. True Arithmetic is not a counter-
> example to Gödel's reasoning.
>
> What Olcott wants still seems to be a
> massive-database of all human knowledge,
> complete, of course,  and
> PO sees Gödel's reasoning as what prevents that,
> somehow,  and
> he sees that complete massive-database
> as essential to True AI  and
> True AI as essential to humanity.
>
> I do not guarantee that my recollection is
> 100% correct or thoroughly up-to-date.
>
> However, assuming IRC,
> True Arithmetic does not serve Olcott's purpose
> because
> the most massively massive of massive-databases
> is still finite, unlike True Arithmetic.
>
> However,
> I'm not sure what F means here.
>
>

F is the name of the Logic System used in the version of Godel's paper
that Olcott is using to (mis)understand Godel's proof. In F, we get a
statement of the form that G is the assertion that there does not exist
a Natuaral Number g that satisfies a particular Primative Recursive
Relationship. This relationship being derived in a meta-system of F that
enumerates the fundamental properties in F, and in which an encoding of
statements to numbers is defined, and the relationship is a Proof Tester
that accepts a number (and only those numbers) that encode a valid proof
of the statement G.

He seems to have a problem with the fact that SOME truths can't be
proven, and somehow thinks that means that this allows untruths to be
claimed as truth.

He seems to want there to be a massive database of all knowledge, and
then that will produce a list of everything that is actually True and
False, and thus somehow make lies go away. The irony is he atually uses
the methodology of the "fake news" crowd to try to push his idea to be
used to eliminate "fake news", because he just doesn't understand

Re: Gödel's 1931 incompleteness fails HOL

<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49884&group=comp.theory#49884

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!rocksolid2!news.neodome.net!usenet.network!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 12:21:30 -0500
Organization: A noiseless patient Spider
Lines: 85
Message-ID: <4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Info: dont-email.me; posting-host="0d741a6c128faa4a3bd094fa89ce188c";
logging-data="909864"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/6Id56v3/5gKlv6l8iEw/lje/h/8u1a3Y="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:im3KfXdRpUhI9NgYgjOoX/Xc29k=
In-Reply-To: <TZQbN.95066$%d2c.83651@fx08.iad>
Content-Language: en-US
 by: Jim Burns - Wed, 6 Dec 2023 17:21 UTC

On 12/5/2023 9:26 PM, Richard Damon wrote:
> On 12/5/23 12:52 PM, Jim Burns wrote:
>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>> On 12/4/23 8:00 PM, olcott wrote:
>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:

>>>>> tl;dr
>>>>> if G("G(u)") is true
>>>>> then G("G(u)") is not ST.provable

>>>> Until you get down to
>>>> "G is unprovable in F"
>>>> we cannot build its proof tree.

>>> There exist a proof tree for that
>>> (which is infinite in length) in F,

>> However,
>> I'm not sure what F means here.
>
> F is the name of the Logic System used in
> the version of Godel's paper that
> Olcott is using to (mis)understand
> Godel's proof.
> In F,
> we get a statement of the form that
> G is the assertion that
> there does not exist
> a Natuaral Number g that satisfies
> a particular Primative Recursive Relationship.
> This relationship being derived in
> a meta-system of F that enumerates
> the fundamental properties in F,
> and in which
> an encoding of statements to numbers
> is defined,
> and the relationship is
> a Proof Tester that accepts
> a number (and only those numbers) that
> encode
> a valid proof of the statement G.

Thank you.

I hope you don't mind
my screwing around with your whitespace.
I'm experimenting with
prettyprinting natural language
in a manner intended to be similar to
prettyprinting computer code.

It seems to me that
natural language would benefit even more
from prettyprinting than code does.
The semantic graphs of natural language
can be at least as tangled as (good) code, but
we are expected to chalk the lines
with only a handful of pronouns instead of
unlimited-many variable names.

Anyway, thank you for answering my question.

> He seems to have a problem with the fact that
> SOME truths can't be proven, and
> somehow thinks that means that
> this allows untruths to be claimed as truth.

I've seen this syndrome elsewhere, as well.
Maybe quantifier dyslexia?

> He seems to want there to be
> a massive database of all knowledge,
> and then that will produce a list of
> everything that is actually True and False,
> and thus somehow
> make lies go away.
> The irony is
> he atually uses the methodology of
> the "fake news" crowd to try to push
> his idea to be used to eliminate "fake news",
> because he just doesn't understand

<sigh>

Re: Gödel's 1931 incompleteness fails HOL

<ukqgs4$sp13$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49885&group=comp.theory#49885

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 13:08:50 -0600
Organization: A noiseless patient Spider
Lines: 118
Message-ID: <ukqgs4$sp13$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 6 Dec 2023 19:08:52 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="ca648a567184d0d58952e4f61d968677";
logging-data="943139"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/6FDA5qpWvzeEHOf/fcBCx"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:/zkavzUyycKgo511huXy+o6+dik=
Content-Language: en-US
In-Reply-To: <4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net>
 by: olcott - Wed, 6 Dec 2023 19:08 UTC

On 12/6/2023 11:21 AM, Jim Burns wrote:
> On 12/5/2023 9:26 PM, Richard Damon wrote:
>> On 12/5/23 12:52 PM, Jim Burns wrote:
>>> On 12/4/2023 8:44 PM, Richard Damon wrote:
>>>> On 12/4/23 8:00 PM, olcott wrote:
>>>>> On 12/4/2023 6:49 PM, Jim Burns wrote:
>
>>>>>> tl;dr
>>>>>> if G("G(u)") is true
>>>>>> then G("G(u)") is not ST.provable
>
>>>>> Until you get down to
>>>>> "G is unprovable in F"
>>>>> we cannot build its proof tree.
>
>>>> There exist a proof tree for that
>>>> (which is infinite in length) in F,
>
>>> However,
>>> I'm not sure what F means here.
>>
>> F is the name of the Logic System used in
>> the version of Godel's paper that
>> Olcott is using to (mis)understand
>> Godel's proof.
>> In F,
>> we get a statement of the form that
>> G is the assertion that
>> there does not exist
>> a Natuaral Number g that satisfies
>> a particular Primative Recursive Relationship.
>> This relationship being derived in
>> a meta-system of F that enumerates
>> the fundamental properties in F,
>> and in which
>> an encoding of statements to numbers
>> is defined,
>> and the relationship is
>> a Proof Tester that accepts
>> a number (and only those numbers) that
>> encode
>> a valid proof of the statement G.
>
> Thank you.
>
> I hope you don't mind
> my screwing around with your whitespace.
> I'm experimenting with
> prettyprinting natural language
> in a manner intended to be similar to
> prettyprinting computer code.
>
> It seems to me that
> natural language would benefit even more
> from prettyprinting than code does.
> The semantic graphs of natural language
> can be at least as tangled as (good) code, but
> we are expected to chalk the lines
> with only a handful of pronouns instead of
> unlimited-many variable names.
>
> Anyway, thank you for answering my question.
>
>> He seems to have a problem with the fact that
>> SOME truths can't be proven, and
>> somehow thinks that means that
>> this allows untruths to be claimed as truth.
>
> I've seen this syndrome elsewhere, as well.
> Maybe quantifier dyslexia?
>
>> He seems to want there to be
>> a massive database of all knowledge,
>> and then that will produce a list of
>> everything that is actually True and False,
>> and thus somehow
>> make lies go away.
>> The irony is
>> he atually uses the methodology of
>> the "fake news" crowd to try to push
>> his idea to be used to eliminate "fake news",
>> because he just doesn't understand
>
> <sigh>
>
>

Tarski incorrectly "proved" that there cannot be any
objective measure of True(x) that works consistently.
Whereas True(x) ≡ (⊢ x) does work consistently for
the entire body of analytical knowledge.

It includes everything known to be true on the basis
of its meaning and excludes unknown truths such as
the truth (or falsity) of the Goldbach conjecture.

Incomplete(L) is merely a terribly misleading euphemism for ~True(L,x).

....14 Every epistemological antinomy can likewise be used
for a similar undecidability proof...(Gödel 1931:43-44)

The most important thing that True(L,x) ≡ (L ⊢ x) excludes
are epistemological antinomies which form the essential
basis of Tarski's proof.

https://liarparadox.org/Tarski_275_276.pdf
(3) x ∉ Provable if and only if x ∈ True.
That is the false assumption step of the Tarski proof.

As soon as humans accept the correct measure of True(x)
then we can manually create formal proofs of English
statements. Until then all opinions including dangerous
lies are incorrectly thought to carry the same weight.

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

Re: Gödel's 1931 incompleteness fails HOL

<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49886&group=comp.theory#49886

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 15:33:16 -0500
Organization: A noiseless patient Spider
Lines: 73
Message-ID: <f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="0d741a6c128faa4a3bd094fa89ce188c";
logging-data="966626"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18ozYClHAuTyZid1jPkBJ1MUyDeMD0j/jA="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:RR7QmQQSWDB0OqQDujfvB5NZfLQ=
Content-Language: en-US
In-Reply-To: <ukqgs4$sp13$1@dont-email.me>
 by: Jim Burns - Wed, 6 Dec 2023 20:33 UTC

On 12/6/2023 2:08 PM, olcott wrote:
> On 12/6/2023 11:21 AM, Jim Burns wrote:

>> [...]
>
> True(x) ≡ (⊢ x)
> It includes everything known to be true on
> the basis of its meaning and excludes
> unknown truths

Unknown truths are at least as capable of
killing you as known truths.

That is something our tiger-dodging ancestors
would have been able to explain well to you,
if they didn't give up and kick you out
into the dark, to let you find out for yourself,
for a short, adrenalized period of time.

> As soon as humans accept
> the correct measure of True(x)
> then we can manually create
> formal proofs of English statements.

Consider the claim qnff =
| Q is not-first-false in
| ⟨… P∨Q ¬P Q …⟩
|     t   f t
|     t   t t
|     t   f f
|     f   t f
| True(qnff) ?
¬True(qnff) ?

Consider the claim finseq =
| For finite sequence ⟨foo … bar⟩
| if ⟨foo … bar⟩ holds a false claim,
| then it holds a first false claim.
| True(finseq) ?
¬True(finseq) ?

_Abbreviate_
| n ends ordered ⟨0,…,n⟩ such that,
| for each split Fᣔ<ᣔH of ⟨0,…,n⟩
| some i‖i+1 is last‖first in F‖H, and
| 0‖n is first‖last in ⟨0,…,n⟩
| for
| non-0 non-doppelgänger non-final i+1
as
| n is a natural number

Consider the claim natnum =
| n is a natural number
| if and only if
| n ends ordered ⟨0,…,n⟩ such that,
| for each split Fᣔ<ᣔH of ⟨0,…,n⟩
| some i‖i+1 is last‖first in F‖H, and
| 0‖n is first‖last in ⟨0,…,n⟩
| for
| non-0 non-doppelgänger non-final i+1
| True(natnum) ?
¬True(natnum) ?

Are you expecting these answers to change
if, for example, a proof of the Goldbach
conjecture is discovered?

Please explain.

Re: Gödel's 1931 incompleteness fails HOL

<ukqpi0$u330$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49887&group=comp.theory#49887

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 15:37:03 -0600
Organization: A noiseless patient Spider
Lines: 86
Message-ID: <ukqpi0$u330$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 6 Dec 2023 21:37:04 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="ca648a567184d0d58952e4f61d968677";
logging-data="986208"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/ckO5a0tyU/tm5BRayCZ5H"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:mG/2oXnPFLosPvRxNBPfDm99uHk=
Content-Language: en-US
In-Reply-To: <f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net>
 by: olcott - Wed, 6 Dec 2023 21:37 UTC

On 12/6/2023 2:33 PM, Jim Burns wrote:
> On 12/6/2023 2:08 PM, olcott wrote:
>> On 12/6/2023 11:21 AM, Jim Burns wrote:
>
>>> [...]
>>
>> True(x) ≡ (⊢ x)
>> It includes everything known to be true on
>> the basis of its meaning and excludes
>> unknown truths
>
> Unknown truths are at least as capable of
> killing you as known truths.
>
> That is something our tiger-dodging ancestors
> would have been able to explain well to you,
> if they didn't give up and kick you out
> into the dark, to let you find out for yourself,
> for a short, adrenalized period of time.
>
>> As soon as humans accept
>> the correct measure of True(x)
>> then we can manually create
>> formal proofs of English statements.
>
> Consider the claim qnff =
> | Q is not-first-false in
> | ⟨… P∨Q ¬P Q …⟩
> |     t   f t
> |     t   t t
> |     t   f f
> |     f   t f
> |
> True(qnff) ?
> ¬True(qnff) ?
>
> Consider the claim finseq =
> | For finite sequence ⟨foo … bar⟩
> | if ⟨foo … bar⟩ holds a false claim,
> | then it holds a first false claim.
> |
> True(finseq) ?
> ¬True(finseq) ?
>
> _Abbreviate_
> | n ends ordered ⟨0,…,n⟩ such that,
> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
> | some i‖i+1 is last‖first in F‖H,  and
> | 0‖n is first‖last in ⟨0,…,n⟩
> | for
> | non-0 non-doppelgänger non-final i+1
> as
> | n is a natural number
>
> Consider the claim natnum =
> | n is a natural number
> | if and only if
> | n ends ordered ⟨0,…,n⟩ such that,
> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
> | some i‖i+1 is last‖first in F‖H,  and
> | 0‖n is first‖last in ⟨0,…,n⟩
> | for
> | non-0 non-doppelgänger non-final i+1
> |
> True(natnum) ?
> ¬True(natnum) ?
>
> Are you expecting these answers to change
> if, for example, a proof of the Goldbach
> conjecture is discovered?
>
> Please explain.
>
>

It seems that you ignored all of my important points.
Can you try again and ask to have anything that you
don't understand explained?

I understand that the philosophy of logic stuff might
be new to you.

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

Re: Gödel's 1931 incompleteness fails HOL

<0799a653-e040-4130-810b-e14a176f747b@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49888&group=comp.theory#49888

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 16:49:21 -0500
Organization: A noiseless patient Spider
Lines: 99
Message-ID: <0799a653-e040-4130-810b-e14a176f747b@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net> <ukqpi0$u330$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="0d741a6c128faa4a3bd094fa89ce188c";
logging-data="986285"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/0S2rTBoF04kCNSWTgheaCJW107XkJl30="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:yi17PHNrFlLa04w8Np6Sc75JnW0=
Content-Language: en-US
In-Reply-To: <ukqpi0$u330$1@dont-email.me>
 by: Jim Burns - Wed, 6 Dec 2023 21:49 UTC

On 12/6/2023 4:37 PM, olcott wrote:
> On 12/6/2023 2:33 PM, Jim Burns wrote:
>> On 12/6/2023 2:08 PM, olcott wrote:
>>> On 12/6/2023 11:21 AM, Jim Burns wrote:

>>>> [...]
>>>
>>> True(x) ≡ (⊢ x)
>>> It includes everything known to be true on
>>> the basis of its meaning and excludes
>>> unknown truths
>>
>> Unknown truths are at least as capable of
>> killing you as known truths.
>>
>> That is something our tiger-dodging ancestors
>> would have been able to explain well to you,
>> if they didn't give up and kick you out
>> into the dark, to let you find out for yourself,
>> for a short, adrenalized period of time.
>>
>>> As soon as humans accept
>>> the correct measure of True(x)
>>> then we can manually create
>>> formal proofs of English statements.
>>
>> Consider the claim qnff =
>> | Q is not-first-false in
>> | ⟨… P∨Q ¬P Q …⟩
>> |     t   f t
>> |     t   t t
>> |     t   f f
>> |     f   t f
>> |
>> True(qnff) ?
>> ¬True(qnff) ?
>>
>> Consider the claim finseq =
>> | For finite sequence ⟨foo … bar⟩
>> | if ⟨foo … bar⟩ holds a false claim,
>> | then it holds a first false claim.
>> |
>> True(finseq) ?
>> ¬True(finseq) ?
>>
>> _Abbreviate_
>> | n ends ordered ⟨0,…,n⟩ such that,
>> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
>> | some i‖i+1 is last‖first in F‖H,  and
>> | 0‖n is first‖last in ⟨0,…,n⟩
>> | for
>> | non-0 non-doppelgänger non-final i+1
>> as
>> | n is a natural number
>>
>> Consider the claim natnum =
>> | n is a natural number
>> | if and only if
>> | n ends ordered ⟨0,…,n⟩ such that,
>> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
>> | some i‖i+1 is last‖first in F‖H,  and
>> | 0‖n is first‖last in ⟨0,…,n⟩
>> | for
>> | non-0 non-doppelgänger non-final i+1
>> |
>> True(natnum) ?
>> ¬True(natnum) ?
>>
>> Are you expecting these answers to change
>> if, for example, a proof of the Goldbach
>> conjecture is discovered?
>>
>> Please explain.
>
> It seems that you ignored all of
> my important points.

>>> excludes unknown truths
is
your most important point.
YMMV.

Unknown truths are at least as capable of
killing you as known truths.

> Can you try again and ask to have
> anything that you don't understand
> explained?

True(qnff) ?
¬True(qnff) ?

True(finseq) ?
¬True(finseq) ?

True(natnum) ?
¬True(natnum) ?

Re: Gödel's 1931 incompleteness fails HOL

<ukqqkm$u6p9$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49889&group=comp.theory#49889

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 15:55:34 -0600
Organization: A noiseless patient Spider
Lines: 113
Message-ID: <ukqqkm$u6p9$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net> <ukqpi0$u330$1@dont-email.me>
<0799a653-e040-4130-810b-e14a176f747b@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 6 Dec 2023 21:55:34 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="ca648a567184d0d58952e4f61d968677";
logging-data="989993"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+kx9gtaMDkdcJpjMM5vq8o"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:PkjGGtQnKK4JyhID8cnQ544SnSY=
In-Reply-To: <0799a653-e040-4130-810b-e14a176f747b@att.net>
Content-Language: en-US
 by: olcott - Wed, 6 Dec 2023 21:55 UTC

On 12/6/2023 3:49 PM, Jim Burns wrote:
> On 12/6/2023 4:37 PM, olcott wrote:
>> On 12/6/2023 2:33 PM, Jim Burns wrote:
>>> On 12/6/2023 2:08 PM, olcott wrote:
>>>> On 12/6/2023 11:21 AM, Jim Burns wrote:
>
>>>>> [...]
>>>>
>>>> True(x) ≡ (⊢ x)
>>>> It includes everything known to be true on
>>>> the basis of its meaning and excludes
>>>> unknown truths
>>>
>>> Unknown truths are at least as capable of
>>> killing you as known truths.
>>>
>>> That is something our tiger-dodging ancestors
>>> would have been able to explain well to you,
>>> if they didn't give up and kick you out
>>> into the dark, to let you find out for yourself,
>>> for a short, adrenalized period of time.
>>>
>>>> As soon as humans accept
>>>> the correct measure of True(x)
>>>> then we can manually create
>>>> formal proofs of English statements.
>>>
>>> Consider the claim qnff =
>>> | Q is not-first-false in
>>> | ⟨… P∨Q ¬P Q …⟩
>>> |     t   f t
>>> |     t   t t
>>> |     t   f f
>>> |     f   t f
>>> |
>>> True(qnff) ?
>>> ¬True(qnff) ?
>>>
>>> Consider the claim finseq =
>>> | For finite sequence ⟨foo … bar⟩
>>> | if ⟨foo … bar⟩ holds a false claim,
>>> | then it holds a first false claim.
>>> |
>>> True(finseq) ?
>>> ¬True(finseq) ?
>>>
>>> _Abbreviate_
>>> | n ends ordered ⟨0,…,n⟩ such that,
>>> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
>>> | some i‖i+1 is last‖first in F‖H,  and
>>> | 0‖n is first‖last in ⟨0,…,n⟩
>>> | for
>>> | non-0 non-doppelgänger non-final i+1
>>> as
>>> | n is a natural number
>>>
>>> Consider the claim natnum =
>>> | n is a natural number
>>> | if and only if
>>> | n ends ordered ⟨0,…,n⟩ such that,
>>> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
>>> | some i‖i+1 is last‖first in F‖H,  and
>>> | 0‖n is first‖last in ⟨0,…,n⟩
>>> | for
>>> | non-0 non-doppelgänger non-final i+1
>>> |
>>> True(natnum) ?
>>> ¬True(natnum) ?
>>>
>>> Are you expecting these answers to change
>>> if, for example, a proof of the Goldbach
>>> conjecture is discovered?
>>>
>>> Please explain.
>>
>> It seems that you ignored all of
>> my important points.
>
>>>> excludes unknown truths
> is
> your most important point.
> YMMV.
>
> Unknown truths are at least as capable of
> killing you as known truths.
>

Philosophically I am only referring to the analytic side
of the analytic / synthetic distinction. That excludes
physical reality where things can kill you.

>> Can you try again and ask to have
>> anything that you don't understand
>> explained?
>
> True(qnff) ?
> ¬True(qnff) ?
>
> True(finseq) ?
> ¬True(finseq) ?
>
> True(natnum) ?
> ¬True(natnum) ?
>

That all seems to be gibberish to me.
Do you understand what this steps of the Tarski proof says:
(3) x ∉ Provable if and only if x ∈ True.

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

Re: Gödel's 1931 incompleteness fails HOL

<db0b32eb-5c6f-42cb-82ea-aa77cf747e5e@att.net>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49890&group=comp.theory#49890

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!news.hispagatos.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: james.g....@att.net (Jim Burns)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 17:35:03 -0500
Organization: A noiseless patient Spider
Lines: 118
Message-ID: <db0b32eb-5c6f-42cb-82ea-aa77cf747e5e@att.net>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net> <ukqpi0$u330$1@dont-email.me>
<0799a653-e040-4130-810b-e14a176f747b@att.net> <ukqqkm$u6p9$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="0d741a6c128faa4a3bd094fa89ce188c";
logging-data="1003483"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+Od8F8tCHJn4AC54jm6+7pEWz7W/oYlG8="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:uhaAo4Mj2stnIiMfv5hDtrFbf9E=
Content-Language: en-US
In-Reply-To: <ukqqkm$u6p9$1@dont-email.me>
 by: Jim Burns - Wed, 6 Dec 2023 22:35 UTC

On 12/6/2023 4:55 PM, olcott wrote:
> On 12/6/2023 3:49 PM, Jim Burns wrote:
>> On 12/6/2023 4:37 PM, olcott wrote:

>>> It seems that you ignored all of
>>> my important points.
>>
>>>>> excludes unknown truths
>> is
>> your most important point.
>> YMMV.
>>
>> Unknown truths are at least as capable of
>> killing you as known truths.
>
> Philosophically I am only referring to
> the analytic side of
> the analytic / synthetic distinction.
> That excludes physical reality where
> things can kill you.

Fascinating.
Would you like me to tell you about
global warming?

>>> Can you try again and ask to have
>>> anything that you don't understand
>>> explained?
>>
>> True(qnff) ?
>> ¬True(qnff) ?
>>
>> True(finseq) ?
>> ¬True(finseq) ?
>>
>> True(natnum) ?
>> ¬True(natnum) ?
>
> That all seems to be gibberish to me.

Consider reading the post to which you respond.

qnff =
| Q is not-first false

finseq =
| If this finite sequence of claims
| holds a false claim,
| then it holds a first false claim.

Abbreviate
a definition of "n is a natural number"
as "n is a natrual number.

natnum =
| n is a natural number
| if and only if
| n satisfies the definition of natural number

----
Consider the claim qnff =
| Q is not-first-false in
| ⟨… P∨Q ¬P Q …⟩
|     t   f t
|     t   t t
|     t   f f
|     f   t f
| True(qnff) ?
¬True(qnff) ?

Consider the claim finseq =
| For finite sequence ⟨foo … bar⟩
| if ⟨foo … bar⟩ holds a false claim,
| then it holds a first false claim.
| True(finseq) ?
¬True(finseq) ?

_Abbreviate_
| n ends ordered ⟨0,…,n⟩ such that,
| for each split Fᣔ<ᣔH of ⟨0,…,n⟩
| some i‖i+1 is last‖first in F‖H, and
| 0‖n is first‖last in ⟨0,…,n⟩
| for
| non-0 non-doppelgänger non-final i+1
as
| n is a natural number

Consider the claim natnum =
| n is a natural number
| if and only if
| n ends ordered ⟨0,…,n⟩ such that,
| for each split Fᣔ<ᣔH of ⟨0,…,n⟩
| some i‖i+1 is last‖first in F‖H, and
| 0‖n is first‖last in ⟨0,…,n⟩
| for
| non-0 non-doppelgänger non-final i+1
| True(natnum) ?
¬True(natnum) ?

Are you expecting these answers to change
if, for example, a proof of the Goldbach
conjecture is discovered?

Please explain.

> Do you understand what this steps of
> the Tarski proof says:
> (3) x ∉ Provable if and only if x ∈ True.

Here's the problem:

You:
> That all seems to be gibberish to me.

Re: Gödel's 1931 incompleteness fails HOL

<ukquta$uu7f$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49891&group=comp.theory#49891

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 17:08:25 -0600
Organization: A noiseless patient Spider
Lines: 143
Message-ID: <ukquta$uu7f$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net> <ukqpi0$u330$1@dont-email.me>
<0799a653-e040-4130-810b-e14a176f747b@att.net> <ukqqkm$u6p9$1@dont-email.me>
<db0b32eb-5c6f-42cb-82ea-aa77cf747e5e@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 6 Dec 2023 23:08:26 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="6fbae9edfbc5958dddb13ea5d3686772";
logging-data="1013999"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19CQlfDDmkT9zh1+8l3HMKG"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:YodNFKlu3XMK7FxsUQoKH5b0SLU=
In-Reply-To: <db0b32eb-5c6f-42cb-82ea-aa77cf747e5e@att.net>
Content-Language: en-US
 by: olcott - Wed, 6 Dec 2023 23:08 UTC

On 12/6/2023 4:35 PM, Jim Burns wrote:
> On 12/6/2023 4:55 PM, olcott wrote:
>> On 12/6/2023 3:49 PM, Jim Burns wrote:
>>> On 12/6/2023 4:37 PM, olcott wrote:
>
>>>> It seems that you ignored all of
>>>> my important points.
>>>
>>>>>> excludes unknown truths
>>> is
>>> your most important point.
>>> YMMV.
>>>
>>> Unknown truths are at least as capable of
>>> killing you as known truths.
>>
>> Philosophically I am only referring to
>> the analytic side of
>> the analytic / synthetic distinction.
>> That excludes physical reality where
>> things can kill you.
>
> Fascinating.
> Would you like me to tell you about
> global warming?
>
>>>> Can you try again and ask to have
>>>> anything that you don't understand
>>>> explained?
>>>
>>> True(qnff) ?
>>> ¬True(qnff) ?
>>>
>>> True(finseq) ?
>>> ¬True(finseq) ?
>>>
>>> True(natnum) ?
>>> ¬True(natnum) ?
>>
>> That all seems to be gibberish to me.
>
> Consider reading the post to which you respond.
>
> qnff =
> | Q is not-first false
>
> finseq =
> | If this finite sequence of claims
> | holds a false claim,
> | then it holds a first false claim.
>
> Abbreviate
> a definition of "n is a natural number"
> as "n is a natrual number.
>
> natnum =
> | n is a natural number
> | if and only if
> | n satisfies the definition of natural number
>
> ----
> Consider the claim qnff =
> | Q is not-first-false in
> | ⟨… P∨Q ¬P Q …⟩
> |     t   f t
> |     t   t t
> |     t   f f
> |     f   t f
> |
> True(qnff) ?
> ¬True(qnff) ?
>
> Consider the claim finseq =
> | For finite sequence ⟨foo … bar⟩
> | if ⟨foo … bar⟩ holds a false claim,
> | then it holds a first false claim.
> |
> True(finseq) ?
> ¬True(finseq) ?
>
> _Abbreviate_
> | n ends ordered ⟨0,…,n⟩ such that,
> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
> | some i‖i+1 is last‖first in F‖H,  and
> | 0‖n is first‖last in ⟨0,…,n⟩
> | for
> | non-0 non-doppelgänger non-final i+1
> as
> | n is a natural number
>
> Consider the claim natnum =
> | n is a natural number
> | if and only if
> | n ends ordered ⟨0,…,n⟩ such that,
> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
> | some i‖i+1 is last‖first in F‖H,  and
> | 0‖n is first‖last in ⟨0,…,n⟩
> | for
> | non-0 non-doppelgänger non-final i+1
> |
> True(natnum) ?
> ¬True(natnum) ?
>
> Are you expecting these answers to change
> if, for example, a proof of the Goldbach
> conjecture is discovered?
>
> Please explain.
>
>> Do you understand what this steps of
>> the Tarski proof says:
>> (3) x ∉ Provable if and only if x ∈ True.
>
> Here's the problem:
>
> You:
>> That all seems to be gibberish to me.
>
>

You are merely changing the subject away from the point.
My whole point pertains to True(L,x) and everything else
is off topic.

Everything about this must be able to be translated
into a clear, correct English sentence.

When G only has a meaning based on 85 instances of
indirect reference specified by 85 different math
formulas this *is not* specified clearly enough.

It must be as clear as this:
∃G ∈ WFF(F) (G ↔ (F ⊬ G))

To say that a Natural number is true or false is
nonsense and you know it.

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

Re: Gödel's 1931 incompleteness fails HOL

<ukr24c$31ue7$1@i2pn2.org>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49892&group=comp.theory#49892

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!.POSTED!not-for-mail
From: rich...@damon-family.org (Richard Damon)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 19:03:24 -0500
Organization: i2pn2 (i2pn.org)
Message-ID: <ukr24c$31ue7$1@i2pn2.org>
References: <ukghnk$2i6q1$2@dont-email.me> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net> <ukqpi0$u330$1@dont-email.me>
<0799a653-e040-4130-810b-e14a176f747b@att.net> <ukqqkm$u6p9$1@dont-email.me>
<db0b32eb-5c6f-42cb-82ea-aa77cf747e5e@att.net> <ukquta$uu7f$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 7 Dec 2023 00:03:24 -0000 (UTC)
Injection-Info: i2pn2.org;
logging-data="3209671"; mail-complaints-to="usenet@i2pn2.org";
posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <ukquta$uu7f$1@dont-email.me>
 by: Richard Damon - Thu, 7 Dec 2023 00:03 UTC

On 12/6/23 6:08 PM, olcott wrote:
> On 12/6/2023 4:35 PM, Jim Burns wrote:
>> On 12/6/2023 4:55 PM, olcott wrote:
>>> On 12/6/2023 3:49 PM, Jim Burns wrote:
>>>> On 12/6/2023 4:37 PM, olcott wrote:
>>
>>>>> It seems that you ignored all of
>>>>> my important points.
>>>>
>>>>>>> excludes unknown truths
>>>> is
>>>> your most important point.
>>>> YMMV.
>>>>
>>>> Unknown truths are at least as capable of
>>>> killing you as known truths.
>>>
>>> Philosophically I am only referring to
>>> the analytic side of
>>> the analytic / synthetic distinction.
>>> That excludes physical reality where
>>> things can kill you.
>>
>> Fascinating.
>> Would you like me to tell you about
>> global warming?
>>
>>>>> Can you try again and ask to have
>>>>> anything that you don't understand
>>>>> explained?
>>>>
>>>> True(qnff) ?
>>>> ¬True(qnff) ?
>>>>
>>>> True(finseq) ?
>>>> ¬True(finseq) ?
>>>>
>>>> True(natnum) ?
>>>> ¬True(natnum) ?
>>>
>>> That all seems to be gibberish to me.
>>
>> Consider reading the post to which you respond.
>>
>> qnff =
>> | Q is not-first false
>>
>> finseq =
>> | If this finite sequence of claims
>> | holds a false claim,
>> | then it holds a first false claim.
>>
>> Abbreviate
>> a definition of "n is a natural number"
>> as "n is a natrual number.
>>
>> natnum =
>> | n is a natural number
>> | if and only if
>> | n satisfies the definition of natural number
>>
>> ----
>> Consider the claim qnff =
>> | Q is not-first-false in
>> | ⟨… P∨Q ¬P Q …⟩
>> |     t   f t
>> |     t   t t
>> |     t   f f
>> |     f   t f
>> |
>> True(qnff) ?
>> ¬True(qnff) ?
>>
>> Consider the claim finseq =
>> | For finite sequence ⟨foo … bar⟩
>> | if ⟨foo … bar⟩ holds a false claim,
>> | then it holds a first false claim.
>> |
>> True(finseq) ?
>> ¬True(finseq) ?
>>
>> _Abbreviate_
>> | n ends ordered ⟨0,…,n⟩ such that,
>> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
>> | some i‖i+1 is last‖first in F‖H,  and
>> | 0‖n is first‖last in ⟨0,…,n⟩
>> | for
>> | non-0 non-doppelgänger non-final i+1
>> as
>> | n is a natural number
>>
>> Consider the claim natnum =
>> | n is a natural number
>> | if and only if
>> | n ends ordered ⟨0,…,n⟩ such that,
>> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
>> | some i‖i+1 is last‖first in F‖H,  and
>> | 0‖n is first‖last in ⟨0,…,n⟩
>> | for
>> | non-0 non-doppelgänger non-final i+1
>> |
>> True(natnum) ?
>> ¬True(natnum) ?
>>
>> Are you expecting these answers to change
>> if, for example, a proof of the Goldbach
>> conjecture is discovered?
>>
>> Please explain.
>>
>>> Do you understand what this steps of
>>> the Tarski proof says:
>>> (3) x ∉ Provable if and only if x ∈ True.
>>
>> Here's the problem:
>>
>> You:
>>> That all seems to be gibberish to me.
>>
>>
>
> You are merely changing the subject away from the point.
> My whole point pertains to True(L,x) and everything else
> is off topic.

And you are showing yourself to be so dumb that you don't understand the
connection to your claim.

>
> Everything about this must be able to be translated
> into a clear, correct English sentence.
>
> When G only has a meaning based on 85 instances of
> indirect reference specified by 85 different math
> formulas this *is not* specified clearly enough.

Nope. Of course, since you don't understand the basis of logic, it all
seems gibberish to you.

>
> It must be as clear as this:
> ∃G ∈ WFF(F) (G ↔ (F ⊬ G))

Except that isn't what Godel was saying.

>
> To say that a Natural number is true or false is
> nonsense and you know it.
>

Who said the number was true or false.

It is the EXISTANCE of the number that will be either true of false.

Or, do you think some definite things either both exist and not exist,
or neither exist and not exist?

Re: Gödel's 1931 incompleteness fails HOL

<ukrfq3$14naa$1@dont-email.me>

  copy mid

https://www.novabbs.com/devel/article-flat.php?id=49893&group=comp.theory#49893

  copy link   Newsgroups: sci.logic sci.math comp.theory comp.ai.philosophy
Path: i2pn2.org!i2pn.org!news.hispagatos.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: sci.logic,sci.math,comp.theory,comp.ai.philosophy
Subject: Re:_Gödel's_1931_incompleteness_fails_HOL
Date: Wed, 6 Dec 2023 21:56:50 -0600
Organization: A noiseless patient Spider
Lines: 143
Message-ID: <ukrfq3$14naa$1@dont-email.me>
References: <ukghnk$2i6q1$2@dont-email.me>
<96598a25-c10e-42d5-9c45-ad740f7aea38@att.net> <uki7o8$2t8ae$1@dont-email.me>
<14d28a7c-0e73-4edc-b5a5-2df480f1afb3@att.net> <ukie4a$2uf4c$2@dont-email.me>
<a46f4c70-de84-40a9-88a7-42ba40c5927e@att.net> <ukikki$2vs7i$1@dont-email.me>
<4d7b4cdf-7d45-4822-bd23-9d29bdce4468@att.net> <ukj0sv$32a8d$2@dont-email.me>
<cd5a612f-9a3f-41f5-a78c-1a41220f80f9@att.net> <ukjmem$39hg0$1@dont-email.me>
<cae06d77-3caa-43d6-9694-ffe962c199e7@att.net> <ukliag$3j59q$1@dont-email.me>
<a241f9fb-083a-4715-84c9-38ef5ca7ff32@att.net> <uklsms$3khan$1@dont-email.me>
<uklv9a$2trsp$4@i2pn2.org> <7c8b4a96-f84d-4c6a-bfdf-1baf82fd22e0@att.net>
<TZQbN.95066$%d2c.83651@fx08.iad>
<4ebc63b3-d3a6-49ac-b2af-cd7dfa3b9011@att.net> <ukqgs4$sp13$1@dont-email.me>
<f2f635d0-88d6-4d3e-9b72-4372cec594c8@att.net> <ukqpi0$u330$1@dont-email.me>
<0799a653-e040-4130-810b-e14a176f747b@att.net> <ukqqkm$u6p9$1@dont-email.me>
<db0b32eb-5c6f-42cb-82ea-aa77cf747e5e@att.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 7 Dec 2023 03:56:52 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="6fbae9edfbc5958dddb13ea5d3686772";
logging-data="1203530"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/qyBzkxFP/Bv+45pr8ATLT"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:x6uKeNd7LEpl1cHqk4OU0D/vldQ=
Content-Language: en-US
In-Reply-To: <db0b32eb-5c6f-42cb-82ea-aa77cf747e5e@att.net>
 by: olcott - Thu, 7 Dec 2023 03:56 UTC

On 12/6/2023 4:35 PM, Jim Burns wrote:
> On 12/6/2023 4:55 PM, olcott wrote:
>> On 12/6/2023 3:49 PM, Jim Burns wrote:
>>> On 12/6/2023 4:37 PM, olcott wrote:
>
>>>> It seems that you ignored all of
>>>> my important points.
>>>
>>>>>> excludes unknown truths
>>> is
>>> your most important point.
>>> YMMV.
>>>
>>> Unknown truths are at least as capable of
>>> killing you as known truths.
>>
>> Philosophically I am only referring to
>> the analytic side of
>> the analytic / synthetic distinction.
>> That excludes physical reality where
>> things can kill you.
>
> Fascinating.
> Would you like me to tell you about
> global warming?
>
>>>> Can you try again and ask to have
>>>> anything that you don't understand
>>>> explained?
>>>
>>> True(qnff) ?
>>> ¬True(qnff) ?
>>>
>>> True(finseq) ?
>>> ¬True(finseq) ?
>>>
>>> True(natnum) ?
>>> ¬True(natnum) ?
>>
>> That all seems to be gibberish to me.
>
> Consider reading the post to which you respond.
>
> qnff =
> | Q is not-first false
>
> finseq =
> | If this finite sequence of claims
> | holds a false claim,
> | then it holds a first false claim.
>
> Abbreviate
> a definition of "n is a natural number"
> as "n is a natrual number.
>
> natnum =
> | n is a natural number
> | if and only if
> | n satisfies the definition of natural number
>
> ----
> Consider the claim qnff =
> | Q is not-first-false in
> | ⟨… P∨Q ¬P Q …⟩
> |     t   f t
> |     t   t t
> |     t   f f
> |     f   t f
> |
> True(qnff) ?
> ¬True(qnff) ?
>
> Consider the claim finseq =
> | For finite sequence ⟨foo … bar⟩
> | if ⟨foo … bar⟩ holds a false claim,
> | then it holds a first false claim.
> |
> True(finseq) ?
> ¬True(finseq) ?
>
> _Abbreviate_
> | n ends ordered ⟨0,…,n⟩ such that,
> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
> | some i‖i+1 is last‖first in F‖H,  and
> | 0‖n is first‖last in ⟨0,…,n⟩
> | for
> | non-0 non-doppelgänger non-final i+1
> as
> | n is a natural number
>
> Consider the claim natnum =
> | n is a natural number
> | if and only if
> | n ends ordered ⟨0,…,n⟩ such that,
> | for each split Fᣔ<ᣔH of ⟨0,…,n⟩
> | some i‖i+1 is last‖first in F‖H,  and
> | 0‖n is first‖last in ⟨0,…,n⟩
> | for
> | non-0 non-doppelgänger non-final i+1
> |
> True(natnum) ?
> ¬True(natnum) ?
>
> Are you expecting these answers to change
> if, for example, a proof of the Goldbach
> conjecture is discovered?
>
> Please explain.
>
>> Do you understand what this steps of
>> the Tarski proof says:
>> (3) x ∉ Provable if and only if x ∈ True.
>
> Here's the problem:
>
> You:
>> That all seems to be gibberish to me.

For you to understand what I am saying you must learn a little
philosophy.

The Sapir–Whorf hypothesis shows that there may be some
concepts that cannot be expressed within the scope of the
terms of logic.
https://en.wikipedia.org/wiki/Linguistic_relativity

Everything that is true on the basis of its meaning:
https://en.wikipedia.org/wiki/Analytic%E2%80%93synthetic_distinction

AKA the analytic side of the analytic / synthetic distinction
necessarily must have a connection from an expression
to this meaning as its truthmaker or it cannot possibly be true.

Although within the conventional terms of logic there
may be some truths that cannot be proven there cannot
be analytic expressions of language that are true without
something making them true.

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


devel / comp.theory / Re: Gödel's 1931 incompleteness fails HOL

Pages:123
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor