Path: ...!weretis.net!feeder9.news.weretis.net!news.nk.ca!rocksolid2!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: comp.theory
Subject: =?UTF-8?Q?Re=3A_G=C3=B6del=27s_actual_proof_and_deriving_all_of_the?=
 =?UTF-8?Q?_digits_of_the_actual_G=C3=B6del_numbers?=
Date: Thu, 31 Oct 2024 19:08:59 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <a2e87ee770e7e42c3f86dd96c416da205f139660@i2pn2.org>
References: <ves6p1$2uoln$1@dont-email.me> <vf5430$sjvj$1@dont-email.me>
 <vf5mat$v6n5$4@dont-email.me> <vf7jbl$1cr7h$1@dont-email.me>
 <vf8b8p$1gkf5$3@dont-email.me> <vfa8iu$1ulea$1@dont-email.me>
 <vfassk$21k64$4@dont-email.me> <vfdjc7$2lcba$1@dont-email.me>
 <vfdlij$2ll17$1@dont-email.me> <vffj9k$33eod$1@dont-email.me>
 <vfg6j4$36im7$1@dont-email.me>
 <dcc4d67737371dbac58b18d718b2d3b6613f1b24@i2pn2.org>
 <vfh3vp$3bkkv$1@dont-email.me>
 <040cd8511c02a898516db227faa75dbc5f74a097@i2pn2.org>
 <vfh8ad$3cdsr$1@dont-email.me>
 <17cad36a46956f00484737183121e8a2c9e742ef@i2pn2.org>
 <vfish6$3ner2$8@dont-email.me> <vfkvk2$8h64$1@dont-email.me>
 <vflio2$fj8s$3@dont-email.me> <vfnicm$to2h$1@dont-email.me>
 <vfo5l8$10s4m$1@dont-email.me> <vfq3dq$1fj4d$1@dont-email.me>
 <vfqnoe$1iaob$3@dont-email.me> <vfsvv1$23p4t$1@dont-email.me>
 <vft7tn$25aio$1@dont-email.me> <vfvjjm$2l1fl$1@dont-email.me>
 <vfvsdf$2mcse$2@dont-email.me>
 <711447717fc61d5f9c95747fe17174ad37e6e996@i2pn2.org>
 <vg03la$2nbaf$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 31 Oct 2024 23:08:59 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="366200"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <vg03la$2nbaf$2@dont-email.me>
X-Spam-Checker-Version: SpamAssassin 4.0.0
Bytes: 3974
Lines: 47

On 10/31/24 10:19 AM, olcott wrote:
> On 10/31/2024 9:00 AM, joes wrote:
>> Am Thu, 31 Oct 2024 07:15:42 -0500 schrieb olcott:
>>> On 10/31/2024 4:45 AM, Mikko wrote:
>>>> On 2024-10-30 12:13:43 +0000, olcott said:
>>>>> On 10/30/2024 4:57 AM, Mikko wrote:
>>>>>> On 2024-10-29 13:25:34 +0000, olcott said:
>>>>>>> On 10/29/2024 2:38 AM, Mikko wrote:
>>>>>>>> On 2024-10-28 14:04:24 +0000, olcott said:
>>>>>>>>> On 10/28/2024 3:35 AM, Mikko wrote:
>>>>>>>>>> On 2024-10-27 14:29:22 +0000, olcott said:
>>>>>>>>>>> On 10/27/2024 4:02 AM, Mikko wrote:
>>
>>>>>>>>> https://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdf
>>>>>>>> That page is not relevant to our immediate context. Note that it
>>>>>>>> uses symbols that are already defined earlier in the opus.
>>>>>>> I think that the assumption that it is anchored in arithmetic is
>>>>>>> incorrect until I see the details of it anchored in actual
>>>>>>> arithmetic.
>>>>>> Depends on what you mean by "it" and "anchored".
>>>>> Exactly what additional basic operations are require besides this to
>>>>> actual algorithmically perform every step of his whole proof? char*
>>>>> sum(x, char* y)
>>>>> char* product(x, char* y)
>>>>> char* exponent(x, char* y)
>>>> In those operations x should have a type. More specifically, the same
>>>> type as y and the function.
>>> Yet arithmetic does not have types and the proof is supposed to be about
>>> numbers.
>> Code has types.
>>
> 
> Not with TMs.

TMs don't have subroutines that you can call.

TMs DO have definitions of how things are to be represented for them.

> 
>>>> In addition to these operations you need comparisons:
>>>> bool equal(char* x, char* y)
>>>> bool greater(char* x, char* y)
>>>> Formulas and in particular the undecidable formulas contain universal
>>>> and existential quantifiers. THere is no way to iimplement those in C.
>>>> But Gödel numbers can be computed and proofs checked without them.
> 
>