| Deutsch English Français Italiano |
|
<vfpisj$3u885$3@i2pn2.org> View for Bookmarking (what is this?) Look up another Usenet article |
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: Mon, 28 Oct 2024 22:56:19 -0400 Organization: i2pn2 (i2pn.org) Message-ID: <vfpisj$3u885$3@i2pn2.org> References: <ves6p1$2uoln$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> <16660b4a608849fb60806904e37def1999b19789@i2pn2.org> <vfpav0$1837o$1@dont-email.me> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Tue, 29 Oct 2024 02:56:19 -0000 (UTC) Injection-Info: i2pn2.org; logging-data="4137221"; mail-complaints-to="usenet@i2pn2.org" User-Agent: Mozilla Thunderbird Content-Language: en-US In-Reply-To: <vfpav0$1837o$1@dont-email.me> Bytes: 12707 Lines: 246 On 10/28/24 8:41 PM, olcott wrote: > On 10/28/2024 6:56 PM, Richard Damon wrote: >> On 10/28/24 10:04 AM, olcott wrote: >>> 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. >>>>>>>>>> >>>>>>>>> ========== REMAINDER OF ARTICLE TRUNCATED ==========