• =?utf-8?Q?Re:_G=C3=B6del's_actual_proof_and_deriving_all_of_the_digits_

    From Mikko@21:1/5 to olcott on Sun Oct 27 11:02:58 2024
    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.

    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.

    --
    Mikko

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mikko@21:1/5 to joes on Mon Oct 28 10:30:35 2024
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mikko@21:1/5 to olcott on Mon Oct 28 10:35:34 2024
    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
    found in textbooks of logic.

    --
    Mikko

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mikko@21:1/5 to olcott on Tue Oct 29 09:38:34 2024
    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
    found in textbooks of logic.

    In other words this is too difficult for you.

    "In other words" is too difficult for you. You should not use those
    words.

    https://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdf

    That page is not relevant to our immediate context. Note that it
    uses symbols that are already defined earlier in the opus.

    --
    Mikko

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mikko@21:1/5 to olcott on Wed Oct 30 11:57:53 2024
    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
    found in textbooks of logic.

    In other words this is too difficult for you.

    "In other words" is too difficult for you. You should not use those
    words.

    https://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdf

    That page is not relevant to our immediate context. Note that it
    uses symbols that are already defined earlier in the opus.


    I think that the assumption that it is anchored in
    arithmetic is incorrect until I see the details of
    it anchored in actual arithmetic.

    Depends on what you mean by "it" and "anchored".

    --
    Mikko

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mikko@21:1/5 to olcott on Thu Oct 31 11:45:26 2024
    On 2024-10-30 12:13:43 +0000, olcott said:

    On 10/30/2024 4:57 AM, Mikko wrote:
    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
    found in textbooks of logic.

    In other words this is too difficult for you.

    "In other words" is too difficult for you. You should not use those
    words.

    https://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdf

    That page is not relevant to our immediate context. Note that it
    uses symbols that are already defined earlier in the opus.


    I think that the assumption that it is anchored in
    arithmetic is incorrect until I see the details of
    it anchored in actual arithmetic.

    Depends on what you mean by "it" and "anchored".


    Exactly what additional basic operations are require besides this
    to actual algorithmically perform every step of his whole proof?
    char* sum(x, char* y)
    char* product(x, char* y)
    char* exponent(x, char* y)

    In those operations x should have a type. More specifically, the same
    type as y and the function.

    In addition to these operations you need comparisons:
    bool equal(char* x, char* y)
    bool greater(char* x, char* y)

    Formulas and in particular the undecidable formulas contain universal
    and existential quantifiers. THere is no way to iimplement those in C.
    But Gödel numbers can be computed and proofs checked without them.

    --
    Mikko

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mikko@21:1/5 to olcott on Fri Nov 1 10:34:45 2024
    On 2024-10-31 12:15:42 +0000, olcott said:

    On 10/31/2024 4:45 AM, Mikko wrote:
    On 2024-10-30 12:13:43 +0000, olcott said:

    On 10/30/2024 4:57 AM, Mikko wrote:
    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 >>>>>>>> found in textbooks of logic.

    In other words this is too difficult for you.

    "In other words" is too difficult for you. You should not use those >>>>>> words.

    https://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdf

    That page is not relevant to our immediate context. Note that it
    uses symbols that are already defined earlier in the opus.


    I think that the assumption that it is anchored in
    arithmetic is incorrect until I see the details of
    it anchored in actual arithmetic.

    Depends on what you mean by "it" and "anchored".


    Exactly what additional basic operations are require besides this
    to actual algorithmically perform every step of his whole proof?
    char* sum(x, char* y)
    char* product(x, char* y)
    char* exponent(x, char* y)

    In those operations x should have a type. More specifically, the same
    type as y and the function.

    Yet arithmetic does not have types and the proof
    is supposed to be about numbers.

    Your proposed functions are not untyped and not of numbers.

    Arithmetic does have types.However,in the most interesting case, all
    terms have the same type: natural number.

    --
    Mikko

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)