Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers

Liste des GroupesRevenir à theory 
Sujet : Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers
De : mikko.levanto (at) *nospam* iki.fi (Mikko)
Groupes : comp.theory
Date : 28. Oct 2024, 09:30:35
Autres entêtes
Organisation : -
Message-ID : <vfni3b$tmp0$1@dont-email.me>
References : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
User-Agent : Unison/2.2
On 2024-10-27 10:02:38 +0000, joes said:

Am Sun, 27 Oct 2024 11:02:58 +0200 schrieb Mikko:
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 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.
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.
 Neat! How did you discover it?
Translation below (I can also translate it into German).
  A sentence describing itself
 I came up with the question if it is possible to find an arithmetic
expression, that when calculated and group the resulting digits in groups
of 3 (as is usual in writing large numbers) and assign each triple an
ASCII code, that you end up with the same sentence.
 The ASCII code gives numbers to 128 symbols. From those, 94 are printable,
like the english alphabet in upper- and lowercase, the digits and the
most common punctuation and some more. ASCII wasn't designed for
arithmetic sentences but for normal messages like orders or
congratulations.
The addition and subtraction symbols + and - are included, but the common
??? signs ... are missing. Instead, there is * which is used for
(where ??? and ... are the multiplication sights centered dot and cross)

 multiplication.
Fractions can't be written normally above and below a line, and   isn't
diwvision sign consisting of a dash with a dot above and another dot below

included. We use / instead. Powers can't be written either, thus we need
another symbol for it. The normal exponentiation symbol [up-arrow] was
included in the old ASCII code, but in the newer code its number is given
to the ^ sign, just like an arrowhead without the shaft. Therefore we use
this to denote raising to a power. Then the expression which would
normally be written [...] can be written in ASCII as 5*12^12. Not as nice,
5 times 10 <sup>12</sup> can be written as 5*10^12

but understandable.
[ymmÄrrettävissä]
 Since we need three digits for each symbol in the ASCII code [decimal?],
the ASCII encoding of the sentence (or whatever text) is much longer than
the sentence (or text) to be encoded. The result of addition is always
shorter than the sentence, as is multiplication. Therefore the sentence
which is supposed to present its own ASCII code requires raising powers.
For example, the previously mentioned 5*10^12 expresses a 13-digit number
with six symbols.
 The symbols and ASCII codes needed for writing the sentence:
symbol  code  meaning
          0   none, padding
         42   multiplication
         43   addition
         45   subtraction
         47   division
          ^   power
 I succeeded in finding a sentence of 21867 symbols in length. When
calculated, you get a number with 65600 digits, which you can divide into
21867 groups of three (the first group has only two digits, but one can
imagine an additional zero in front). Hence we have:
Nice translation. Thank you.
--
Mikko

Date Sujet#  Auteur
18 Oct 24 * A state transition diagram proves ...142olcott
18 Oct 24 `* Re: A state transition diagram proves ...141Richard Damon
18 Oct 24  `* Re: A state transition diagram proves ...140olcott
18 Oct 24   `* Re: A state transition diagram proves ...139Richard Damon
18 Oct 24    `* Re: A state transition diagram proves ...138olcott
18 Oct 24     `* Re: A state transition diagram proves ...137Richard Damon
18 Oct 24      `* Re: A state transition diagram proves ... GOOD PROGRESS136olcott
18 Oct 24       +* Re: A state transition diagram proves ... GOOD PROGRESS24joes
18 Oct 24       i`* Re: A state transition diagram proves ... GOOD PROGRESS23olcott
18 Oct 24       i +- Re: A state transition diagram proves ... GOOD PROGRESS -- I only wanted to cross post this key break through once.1olcott
18 Oct 24       i +* Re: A state transition diagram proves ... GOOD PROGRESS14joes
18 Oct 24       i i`* Re: A state transition diagram proves ... GOOD PROGRESS13olcott
18 Oct 24       i i `* Re: A state transition diagram proves ... GOOD PROGRESS12joes
18 Oct 24       i i  `* Re: A state transition diagram proves ... GOOD PROGRESS11olcott
18 Oct 24       i i   `* Re: A state transition diagram proves ... GOOD PROGRESS10Alan Mackenzie
18 Oct 24       i i    `* Re: A state transition diagram proves ... GOOD PROGRESS9olcott
18 Oct 24       i i     `* Re: A state transition diagram proves ... GOOD PROGRESS8joes
18 Oct 24       i i      `* Re: A state transition diagram proves ... GOOD PROGRESS7olcott
18 Oct 24       i i       +- Re: A state transition diagram proves ... GOOD PROGRESS1olcott
19 Oct 24       i i       `* Re: A state transition diagram proves ... GOOD PROGRESS5joes
19 Oct 24       i i        `* Re: A state transition diagram proves ... GOOD PROGRESS4olcott
19 Oct 24       i i         `* Re: A state transition diagram proves ... GOOD PROGRESS3Richard Damon
19 Oct 24       i i          `* Re: A state transition diagram proves ... GOOD PROGRESS2olcott
19 Oct 24       i i           `- Re: A state transition diagram proves ... GOOD PROGRESS1Richard Damon
19 Oct 24       i `* Re: A state transition diagram proves ... GOOD PROGRESS7Richard Damon
19 Oct 24       i  `* Re: A state transition diagram proves ... GOOD PROGRESS6olcott
19 Oct 24       i   `* Re: A state transition diagram proves ... GOOD PROGRESS5Richard Damon
19 Oct 24       i    `* Re: A state transition diagram proves ... GOOD PROGRESS4olcott
19 Oct 24       i     `* Re: A state transition diagram proves ... GOOD PROGRESS3Richard Damon
19 Oct 24       i      `* Re: A state transition diagram proves ... GOOD PROGRESS2olcott
19 Oct 24       i       `- Re: A state transition diagram proves ... GOOD PROGRESS1Richard Damon
19 Oct 24       `* Re: A state transition diagram proves ... GOOD PROGRESS111Richard Damon
19 Oct 24        +- Re: A state transition diagram proves ... GOOD PROGRESS1olcott
19 Oct 24        `* THREE DIFFERENT QUESTIONS109olcott
19 Oct 24         `* Re: THREE DIFFERENT QUESTIONS108Richard Damon
19 Oct 24          `* Re: THREE DIFFERENT QUESTIONS107olcott
19 Oct 24           `* Re: THREE DIFFERENT QUESTIONS106Richard Damon
19 Oct 24            `* Re: THREE DIFFERENT QUESTIONS105olcott
19 Oct 24             `* Re: THREE DIFFERENT QUESTIONS104Richard Damon
20 Oct 24              `* Re: THREE DIFFERENT QUESTIONS103olcott
20 Oct 24               `* Re: THREE DIFFERENT QUESTIONS102Richard Damon
20 Oct 24                `* I have always been correct about emulating termination analyzers --- PROOF101olcott
20 Oct 24                 +* Re: I have always been correct about emulating termination analyzers --- PROOF99Richard Damon
20 Oct 24                 i`* Re: I have always been correct about emulating termination analyzers --- PROOF98olcott
20 Oct 24                 i +* Re: I have always been correct about emulating termination analyzers --- PROOF10Richard Damon
20 Oct 24                 i i+* Re: I have always been correct about emulating termination analyzers --- PROOF2olcott
20 Oct 24                 i ii`- Re: I have always been incorrect about emulating termination analyzers --- PROOF1Richard Damon
20 Oct 24                 i i+* Re: I have always been correct about emulating termination analyzers --- PROOF2olcott
20 Oct 24                 i ii`- Re: I have always been incorrect about emulating termination analyzers --- PROOF1Richard Damon
20 Oct 24                 i i`* Deriving X from the finite set of FooBar preserving operations --- membership algorithm for X in L5olcott
21 Oct 24                 i i +- Re: Deriving X from the finite set of FooBar preserving operations --- membership algorithm for X in L1Richard Damon
21 Oct 24                 i i `* Re: Deriving X from the finite set of FooBar preserving operations --- membership algorithm for X in L3Richard Damon
21 Oct 24                 i i  `* Re: Deriving X from the finite set of FooBar preserving operations --- membership algorithm for X in L2olcott
21 Oct 24                 i i   `- Re: Deriving X from the finite set of FooBar preserving operations --- membership algorithm for X in L1Richard Damon
21 Oct 24                 i `* Re: I have always been correct about emulating termination analyzers --- PROOF87Mikko
21 Oct 24                 i  `* Re: I have always been correct about emulating termination analyzers --- PROOF86olcott
22 Oct 24                 i   `* Re: I have always been correct about emulating termination analyzers --- PROOF85Mikko
22 Oct 24                 i    `* Re: I have always been correct about emulating termination analyzers --- PROOF84olcott
23 Oct 24                 i     `* Re: I have always been correct about emulating termination analyzers --- PROOF83Mikko
23 Oct 24                 i      `* Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs82olcott
24 Oct 24                 i       +- Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs1Richard Damon
24 Oct 24                 i       `* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs80Mikko
24 Oct 24                 i        `* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs79olcott
25 Oct 24                 i         +* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs5Richard Damon
25 Oct 24                 i         i`* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs4olcott
25 Oct 24                 i         i `* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs3Richard Damon
25 Oct 24                 i         i  `* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs2olcott
25 Oct 24                 i         i   `- Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs1Richard Damon
25 Oct 24                 i         `* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs73Mikko
25 Oct 24                 i          `* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs72olcott
25 Oct 24                 i           +* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs36Richard Damon
25 Oct 24                 i           i`* Gödel's actual proof and deriving all of the digits of the actual Gödel numbers35olcott
26 Oct 24                 i           i `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers34Richard Damon
26 Oct 24                 i           i  `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers33olcott
26 Oct 24                 i           i   +* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers30Richard Damon
26 Oct 24                 i           i   i`* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers29olcott
26 Oct 24                 i           i   i +- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Richard Damon
27 Oct 24                 i           i   i `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers27Mikko
27 Oct 24                 i           i   i  +* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers2joes
28 Oct 24                 i           i   i  i`- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Mikko
27 Oct 24                 i           i   i  `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers24olcott
27 Oct 24                 i           i   i   +- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Richard Damon
28 Oct 24                 i           i   i   `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers22Mikko
28 Oct 24                 i           i   i    `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers21olcott
29 Oct 24                 i           i   i     +* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers5Richard Damon
29 Oct 24                 i           i   i     i`* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers4olcott
29 Oct 24                 i           i   i     i +* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers2André G. Isaak
29 Oct 24                 i           i   i     i i`- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1olcott
29 Oct 24                 i           i   i     i `- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Richard Damon
29 Oct 24                 i           i   i     `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers15Mikko
29 Oct 24                 i           i   i      `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers14olcott
30 Oct 24                 i           i   i       +- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Richard Damon
30 Oct 24                 i           i   i       `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers12Mikko
30 Oct 24                 i           i   i        `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers11olcott
31 Oct 24                 i           i   i         +- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Richard Damon
31 Oct 24                 i           i   i         `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers9Mikko
31 Oct 24                 i           i   i          `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers8olcott
31 Oct 24                 i           i   i           +* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers3joes
31 Oct 24                 i           i   i           i`* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers2olcott
1 Nov 24                 i           i   i           i `- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Richard Damon
1 Nov 24                 i           i   i           +- Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers1Richard Damon
1 Nov 24                 i           i   i           `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers3Mikko
26 Oct 24                 i           i   `* Re: Gödel's actual proof and deriving all of the digits of the actual Gödel numbers2joes
26 Oct 24                 i           `* Re: Peano Axioms anchored in First Grade Arithmetic on ASCII Digit String pairs35Mikko
20 Oct 24                 `- Re: I have always been correct about emulating termination analyzers --- PROOF1Richard Damon

Haut de la page

Les messages affichés proviennent d'usenet.

NewsPortal