Path: ...!eternal-september.org!feeder2.eternal-september.org!i2pn.org!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: Sat, 26 Oct 2024 11:35:43 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <vfj28f$3j3qf$3@i2pn2.org>
References: <ves6p1$2uoln$1@dont-email.me> <vev8gg$3me0u$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 26 Oct 2024 15:35:43 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="3772239"; mail-complaints-to="usenet@i2pn2.org"
User-Agent: Mozilla Thunderbird
Content-Language: en-US
In-Reply-To: <vfish6$3ner2$8@dont-email.me>
Bytes: 9369
Lines: 172

On 10/26/24 9:57 AM, olcott wrote:
> 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.
> 

Maybe not. Godel, having written his proof before the modern computer 
doesn't deal with such minor details.

Some will be. but some might not, and the size of them doesn't matter 
for the proof, since mathematics isn't limited by the number of bytes 
needed to represent the numbers.

To give you an idea of the numbers, his encoding is based on the use of 
prime numbers and building powers and products of them.

========== REMAINDER OF ARTICLE TRUNCATED ==========