Path: ...!eternal-september.org!feeder2.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: =?utf-8?Q?Re:_G=C3=B6del's_actual_proof_and_deriving_all_of_the_digits_of_the_actual_G=C3=B6del_numbers?=
Date: Wed, 30 Oct 2024 11:57:53 +0200
Organization: -
Lines: 203
Message-ID: <vfsvv1$23p4t$1@dont-email.me>
References: <ves6p1$2uoln$1@dont-email.me> <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> <vfnicm$to2h$1@dont-email.me> <vfo5l8$10s4m$1@dont-email.me> <vfq3dq$1fj4d$1@dont-email.me> <vfqnoe$1iaob$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 30 Oct 2024 10:57:54 +0100 (CET)
Injection-Info: dont-email.me; posting-host="0011499cc82b83165b64a4733e06e655";
	logging-data="2221213"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19t4Subt1/pyJXcDcZjO4Fx"
User-Agent: Unison/2.2
Cancel-Lock: sha1:laO7+xnhAA6Qfkf2JO3BzMzhts0=
Bytes: 11863

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:
>>>>>> 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:
>>>>>> 
>>>>>> 1. Encode all formulas with the 94 visible ASCII characters.
>>>>>> 2. Encode the 94 ASCII characters with two decimal digits.
>>>>>> 
>>>>> 
>>>>> Just encode them as actual ASCII and you have a 94-ary number
>>>>> system in half the space.
>>>>> 
>>>>>> In addition to the 94 ASCII characters you may use 6 other characters.
>>>>>> To encode a proof you need one character (e.g. semicolon or one of
>>>>>> the 6 non-ASCII characters) for separator. Some uses of this encodeing
>>>>>> are much simpler if the code 00 is used as a separator and a filler
>>>>>> that is not a part of a formula. That way you can use formulas that are
>>>>>> shorter than the space for them. For example, proofs are easier to handle
>>>>>> if every sentence of the proof is padded to the same length. Leading
>>>>>> zeros should be meaningless anyway.
>>>>>> 
>>>>>> At the end of the page http://iki.fi/mikko.levanto/lauseke.html
>>>>>> I have an arithmetic expression that evaluates to a 65600 digits
>>>>>> number. With one leading zero the number can be split in to 21867
>>>>>> groups of three digits. Each group encodes one character of the
>>>>>> expression.
>>>>>> 
>>>>>> Gödel numbers of proofs are larger, possibly much arger, than Gödel
>>>>>> numbers of formulas.
>>>>>> 
>>>>> 
>>>>> Lets at least see the exact sequence of steps as applied
>>>>> to ASCII digits. He says he is basing this on arithmetic
>>>>> lets see this actual arithmetic even is applied to variables.
>>>>> What are the 100% completely specified steps with zero details
>>>>> left out where elements of the set of arithmetic operations
>>>>> applied to ASCII digits can possibly say things totally outside
>>>>> of the scope of arithmetic operations?
>>>> 
>>>> Gödel did not use ASCII digits. The rules of his numbering can
========== REMAINDER OF ARTICLE TRUNCATED ==========