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: Sun, 27 Oct 2024 13:49:00 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <vfluec$3nvp8$4@i2pn2.org>
References: <ves6p1$2uoln$1@dont-email.me>
 <eb38c4aff9c8bc250c49892461ac25bfccfe303f@i2pn2.org>
 <vf051u$3rr97$1@dont-email.me>
 <e3f28689429722f86224d0d736115e4d1895299b@i2pn2.org>
 <vf1hun$39e3$1@dont-email.me>
 <dedb2801cc230a4cf689802934c4b841ae1a29eb@i2pn2.org>
 <vf1stu$8h0v$1@dont-email.me>
 <592109c757262c48aaca517a829ea1867913316b@i2pn2.org>
 <vf37qt$fbb3$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 27 Oct 2024 17:49:00 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="3931944"; mail-complaints-to="usenet@i2pn2.org"
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <vflio2$fj8s$3@dont-email.me>
Bytes: 12652
Lines: 237

On 10/27/24 10:29 AM, olcott wrote:
> On 10/27/2024 4:02 AM, Mikko wrote:
>> On 2024-10-26 13:57:58 +0000, olcott said:
>>
>>> On 10/25/2024 11:07 PM, Richard Damon wrote:
>>>> On 10/25/24 7:06 PM, olcott wrote:
>>>>> On 10/25/2024 5:17 PM, Richard Damon wrote:
>>>>>> On 10/25/24 5:52 PM, olcott wrote:
>>>>>>> On 10/25/2024 10:52 AM, Richard Damon wrote:
>>>>>>>> On 10/25/24 9:31 AM, olcott wrote:
>>>>>>>>> On 10/25/2024 3:01 AM, Mikko wrote:
>>>>>>>>>> On 2024-10-24 14:28:35 +0000, olcott said:
>>>>>>>>>>
>>>>>>>>>>> On 10/24/2024 8:51 AM, Mikko wrote:
>>>>>>>>>>>> On 2024-10-23 13:15:00 +0000, olcott said:
>>>>>>>>>>>>
>>>>>>>>>>>>> On 10/23/2024 2:28 AM, Mikko wrote:
>>>>>>>>>>>>>> On 2024-10-22 14:02:01 +0000, olcott said:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> On 10/22/2024 2:13 AM, Mikko wrote:
>>>>>>>>>>>>>>>> On 2024-10-21 13:52:28 +0000, olcott said:
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> On 10/21/2024 3:41 AM, Mikko wrote:
>>>>>>>>>>>>>>>>>> On 2024-10-20 15:32:45 +0000, olcott said:
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> The actual barest essence for formal systems and 
>>>>>>>>>>>>>>>>>>> computations
>>>>>>>>>>>>>>>>>>> is finite string transformation rules applied to 
>>>>>>>>>>>>>>>>>>> finite strings.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Before you can start from that you need a formal 
>>>>>>>>>>>>>>>>>> theory that
>>>>>>>>>>>>>>>>>> can be interpreted as a theory of finite strings.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Not at all. The only theory needed are the operations
>>>>>>>>>>>>>>>>> that can be performed on finite strings:
>>>>>>>>>>>>>>>>> concatenation, substring, relational operator ...
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> You may try with an informal foundation but you need to 
>>>>>>>>>>>>>>>> make sure
>>>>>>>>>>>>>>>> that it is sufficicently well defined and that is easier 
>>>>>>>>>>>>>>>> with a
>>>>>>>>>>>>>>>> formal theory.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> The minimal complete theory that I can think of computes
>>>>>>>>>>>>>>>>> the sum of pairs of ASCII digit strings.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> That is easily extended to Peano arithmetic.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> As a bottom layer you need some sort of logic. There 
>>>>>>>>>>>>>>>> must be unambifuous
>>>>>>>>>>>>>>>> rules about syntax and inference.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I already wrote this in C a long time ago.
>>>>>>>>>>>>>>> It simply computes the sum the same way
>>>>>>>>>>>>>>> that a first grader would compute the sum.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I have no idea how the first grade arithmetic
>>>>>>>>>>>>>>> algorithm could be extended to PA.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Basically you define that the successor of X is X + 1. The 
>>>>>>>>>>>>>> only
>>>>>>>>>>>>>> primitive function of Peano arithmetic is the successor. 
>>>>>>>>>>>>>> Addition
>>>>>>>>>>>>>> and multiplication are recursively defined from the successor
>>>>>>>>>>>>>> function. Equality is often included in the underlying 
>>>>>>>>>>>>>> logic but
>>>>>>>>>>>>>> can be defined recursively from the successor function and 
>>>>>>>>>>>>>> the
>>>>>>>>>>>>>> order relation is defined similarly.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Anyway, the details are not important, only that it can be 
>>>>>>>>>>>>>> done.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> First grade arithmetic can define a successor function
>>>>>>>>>>>>> by merely applying first grade arithmetic to the pair
>>>>>>>>>>>>> of ASCII digits strings of [0-1]+ and "1".
>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Peano_axioms
>>>>>>>>>>>>>
>>>>>>>>>>>>> The first incompleteness theorem states that no consistent 
>>>>>>>>>>>>> system of axioms whose theorems can be listed by an 
>>>>>>>>>>>>> effective procedure (i.e. an algorithm) is capable of 
>>>>>>>>>>>>> proving all truths about the arithmetic of natural numbers. 
>>>>>>>>>>>>> For any such consistent formal system, there will always be 
>>>>>>>>>>>>> statements about natural numbers that are true, but that 
>>>>>>>>>>>>> are unprovable within the system.
>>>>>>>>>>>>> https://en.wikipedia.org/wiki/ 
>>>>>>>>>>>>> G%C3%B6del%27s_incompleteness_theorems
>>>>>>>>>>>>>
>>>>>>>>>>>>> When we boil this down to its first-grade arithmetic 
>>>>>>>>>>>>> foundation
>>>>>>>>>>>>> this would seem to mean that there are some cases where the
>>>>>>>>>>>>> sum of a pair of ASCII digit strings cannot be computed.
>>>>>>>>>>>>
>>>>>>>>>>>> No, it does not. Incompleteness theorem does not apply to 
>>>>>>>>>>>> artihmetic
>>>>>>>>>>>> that only has addition but not multiplication.
>>>>>>>>>>>>
>>>>>>>>>>>> The incompleteness theorem is about theories that have 
>>>>>>>>>>>> quantifiers.
>>>>>>>>>>>> A specific arithmetic expression (i.e, with no variables of 
>>>>>>>>>>>> any kind)
>>>>>>>>>>>> always has a well defined value.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> So lets goes the next step and add multiplication to the 
>>>>>>>>>>> algorithm:
>>>>>>>>>>> (just like first grade arithmetic we perform multiplication
>>>>>>>>>>> on arbitrary length ASCII digit strings just like someone would
>>>>>>>>>>> do with pencil and paper).
>>>>>>>>>>>
>>>>>>>>>>> Incompleteness cannot be defined. until we add variables and
>>>>>>>>>>> quantification: There exists an X such that X * 11 = 132.
>>>>>>>>>>> Every detail of every step until we get G is unprovable in F.
>>>>>>>>>>
>>>>>>>>>> Incompleteness is easier to define if you also add the power 
>>>>>>>>>> operator
>>>>>>>>>> to the arithmetic. Otherwise the expressions of provability and
>>>>>>>>>> incompleteness are more complicated. They become much simpler if
>>>>>>>>>> instead of arithmetic the fundamental theory is a theory of 
>>>>>>>>>> finite
>>>>>>>>>> strings. As you already observed, arithmetic is easy to do with
>>>>>>>>>> finite strings. The opposite is possible but much more 
>>>>>>>>>> complicated.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> The power operator can be built from repeated operations of
>>>>>>>>> the multiply operator. Will a terabyte be enough to store
>>>>>>>>> the Gödel numbers?
>>>>>>>>>
>>>>>>>>
>>>>>>>> Likely depends on how big of a system you are making F.
>>>>>>>>
>>>>>>>
>>>>>>> I am proposing actually doing Gödel's actual proof and
>>>>>>> deriving all of the digits of the actual Gödel numbers.
>>>>>>>
>>>>>>
>>>>>> Then try it and see.
>>>>>>
>>>>>> You do understand that the first step is to fully enumerate all 
>>>>>> the axioms of the system, and any proofs used to generate the 
>>>>>> needed properties of the mathematics that he uses.
>>>>>>
>>>>>
>>>>> Gödel seems to propose that his numbers are
>>>>> actual integers, are you saying otherwise?
>>>>>
>>>>
>>>> Not at all, just that they may be very large numbers.
>>>
>>> Are they less than one GB each? I want to see the c
>>> code that computes them. I want to know how many bytes
>>> of ASCII digits strings they are.
>>
>> The memory needs are easier to estimate if you use a different
>> numbering system:
========== REMAINDER OF ARTICLE TRUNCATED ==========