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.
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?
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:Incompleteness is easier to define if you also add the power
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:You may try with an informal foundation but you need to >>>>>>>>>>>>>> make sure
On 2024-10-20 15:32:45 +0000, olcott said:Not at all. The only theory needed are the operations >>>>>>>>>>>>>>> that can be performed on finite strings:
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. >>>>>>>>>>>>>>>
concatenation, substring, relational operator ... >>>>>>>>>>>>>>
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. >>>>>>>>
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.
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:Incompleteness is easier to define if you also add the power >>>>>>>>>> operator
On 2024-10-23 13:15:00 +0000, olcott said:
On 10/23/2024 2:28 AM, Mikko wrote:No, it does not. Incompleteness theorem does not apply to >>>>>>>>>>>> artihmetic
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:You may try with an informal foundation but you need to >>>>>>>>>>>>>>>> make sure
On 2024-10-20 15:32:45 +0000, olcott said: >>>>>>>>>>>>>>>>>>Not at all. The only theory needed are the operations >>>>>>>>>>>>>>>>> that can be performed on finite strings:
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. >>>>>>>>>>>>>>>>>
concatenation, substring, relational operator ... >>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>
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. >>>>>>>>>>
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 is unprovable in F"
is the following set of arithmetic operations on ASCII digit strings.
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:Incompleteness is easier to define if you also add the power >>>>>>>>>>>> operator
On 2024-10-23 13:15:00 +0000, olcott said:
On 10/23/2024 2:28 AM, Mikko wrote:No, it does not. Incompleteness theorem does not apply to >>>>>>>>>>>>>> artihmetic
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:You may try with an informal foundation but you need >>>>>>>>>>>>>>>>>> to make sure
On 2024-10-20 15:32:45 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>Not at all. The only theory needed are the operations >>>>>>>>>>>>>>>>>>> that can be performed on finite strings: >>>>>>>>>>>>>>>>>>> concatenation, substring, relational operator ... >>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>
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. >>>>>>>>>>>>
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. https://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdf
On 10/28/2024 6:56 PM, Richard Damon wrote:
Which isn't enough to encode it into a Godel number, as you need to go
back an assign every axioms, and the definition of every term of that
statement back to those axioms.
I knew that yet his full paper is no longer available online.
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:No, it does not. Incompleteness theorem does not apply >>>>>>>>>>>>>>>> to artihmetic
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: >>>>>>>>>>>>>>>>>>>>>>You may try with an informal foundation but you need >>>>>>>>>>>>>>>>>>>> to make sure
Not at all. The only theory needed are the operations >>>>>>>>>>>>>>>>>>>>> that can be performed on finite strings: >>>>>>>>>>>>>>>>>>>>> concatenation, substring, relational operator ... >>>>>>>>>>>>>>>>>>>>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. >>>>>>>>>>>>>>>>>>>>>
that it is sufficicently well defined and that is >>>>>>>>>>>>>>>>>>>> easier with a
formal theory.
The minimal complete theory that I can think of >>>>>>>>>>>>>>>>>>>>> computesThat is easily extended to Peano arithmetic. >>>>>>>>>>>>>>>>>>>>
the sum of pairs of ASCII digit strings. >>>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>>
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.
https://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdf
Which isn't enough to encode it into a Godel number, as you need to go
back an assign every axioms, and the definition of every term of that
statement back to those axioms.
I knew that yet his full paper is no longer available online.
Go ahead, try it.
I am challenging the assumption that it is actually based
on arithmetic combined with the existential operator.
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:No, it does not. Incompleteness theorem does not apply >>>>>>>>>>>>>>>> to artihmetic
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: >>>>>>>>>>>>>>>>>>>>>>You may try with an informal foundation but you need >>>>>>>>>>>>>>>>>>>> to make sure
Not at all. The only theory needed are the operations >>>>>>>>>>>>>>>>>>>>> that can be performed on finite strings: >>>>>>>>>>>>>>>>>>>>> concatenation, substring, relational operator ... >>>>>>>>>>>>>>>>>>>>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. >>>>>>>>>>>>>>>>>>>>>
that it is sufficicently well defined and that is >>>>>>>>>>>>>>>>>>>> easier with a
formal theory.
The minimal complete theory that I can think of >>>>>>>>>>>>>>>>>>>>> computesThat is easily extended to Peano arithmetic. >>>>>>>>>>>>>>>>>>>>
the sum of pairs of ASCII digit strings. >>>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>>
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.
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:No, it does not. Incompleteness theorem does not apply >>>>>>>>>>>>>>>>>> to artihmetic
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: >>>>>>>>>>>>>>>>>>>>>>>>You may try with an informal foundation but you >>>>>>>>>>>>>>>>>>>>>> need to make sure
Not at all. The only theory needed are the >>>>>>>>>>>>>>>>>>>>>>> operationsThe 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. >>>>>>>>>>>>>>>>>>>>>>>
that can be performed on finite strings: >>>>>>>>>>>>>>>>>>>>>>> concatenation, substring, relational operator ... >>>>>>>>>>>>>>>>>>>>>>
that it is sufficicently well defined and that is >>>>>>>>>>>>>>>>>>>>>> easier with a
formal theory.
The minimal complete theory that I can think of >>>>>>>>>>>>>>>>>>>>>>> computesThat is easily extended to Peano arithmetic. >>>>>>>>>>>>>>>>>>>>>>
the sum of pairs of ASCII digit strings. >>>>>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>>>>
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)
On 10/31/2024 9:00 AM, joes wrote:
Am Thu, 31 Oct 2024 07:15:42 -0500 schrieb olcott:
On 10/31/2024 4:45 AM, Mikko wrote:Code has types.
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:
Yet arithmetic does not have types and the proof is supposed to be about >>> numbers.In those operations x should have a type. More specifically, the sameExactly what additional basic operations are require besides this to >>>>> actual algorithmically perform every step of his whole proof? char*Depends on what you mean by "it" and "anchored".I think that the assumption that it is anchored in arithmetic is >>>>>>> incorrect until I see the details of it anchored in actualhttps://www.liarparadox.org/G%C3%B6del_Sentence(1931).pdfThat page is not relevant to our immediate context. Note that it >>>>>>>> uses symbols that are already defined earlier in the opus.
arithmetic.
sum(x, char* y)
char* product(x, char* y)
char* exponent(x, char* y)
type as y and the function.
Not with TMs.
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.
On 11/1/2024 3:34 AM, Mikko wrote:
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:Are they less than one GB each? I want to see the c
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: >>>>>>>>>>>>>>>>>>>>>>>>>>Basically you define that the successor of X is >>>>>>>>>>>>>>>>>>>>>>>> X + 1. The only
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 computesThat is easily extended to Peano arithmetic. >>>>>>>>>>>>>>>>>>>>>>>>>>
the sum of pairs of ASCII digit strings. >>>>>>>>>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>
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.
Finite strings of ASCII digits are an easy way to encode
natural numbers.
Arithmetic does have types.However,in the most interesting case, all
terms have the same type: natural number.
OK the arithmetic of natural numbers does have one type.
Sysop: | Keyop |
---|---|
Location: | Huddersfield, West Yorkshire, UK |
Users: | 546 |
Nodes: | 16 (2 / 14) |
Uptime: | 05:28:00 |
Calls: | 10,386 |
Calls today: | 1 |
Files: | 14,058 |
Messages: | 6,416,631 |