On 10/25/2024 5:17 PM, Richard Damon wrote:No, how do you get that?
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:
Gödel seems to propose that his numbers are actual integers, are youThen try it and see.I am proposing actually doing Gödel's actual proof and deriving all ofThe power operator can be built from repeated operations of theLikely depends on how big of a system you are making F.
multiply operator. Will a terabyte be enough to store the Gödel
numbers?
the digits of the actual Gödel numbers.
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.
saying otherwise?
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 memory needs are easier to estimate if you use a different numbering system:Are they less than one GB each? I want to see the c code that computesNot at all, just that they may be very large numbers.Gödel seems to propose that his numbers are actual integers, are youThen try it and see.I am proposing actually doing Gödel's actual proof and deriving all >>>>>> of the digits of the actual Gödel numbers.Likely depends on how big of a system you are making F.The power operator can be built from repeated operations of the >>>>>>>> multiply operator. Will a terabyte be enough to store the Gödel >>>>>>>> numbers?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.So lets goes the next step and add multiplication to theNo, it does not. Incompleteness theorem does not apply to >>>>>>>>>>> artihmetic that only has addition but not multiplication. >>>>>>>>>>> The incompleteness theorem is about theories that haveFirst 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".Basically you define that the successor of X is X + 1. The >>>>>>>>>>>>> only primitive function of Peano arithmetic is theI 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.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 have no idea how the first grade arithmetic algorithm >>>>>>>>>>>>>> could be extended to PA.
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.
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.
quantifiers. A specific arithmetic expression (i.e, with no >>>>>>>>>>> variables of any kind)
always has a well defined value.
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
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.
saying otherwise?
them. I want to know how many bytes of ASCII digits strings they are.
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.
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 toDepends on what you mean by "it" and "anchored".I think that the assumption that it is anchored in arithmetic ishttps://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.
incorrect until I see the details of it anchored in actual
arithmetic.
actual algorithmically perform every step of his whole proof? char*
sum(x, char* y)
char* product(x, char* y)
char* exponent(x, char* y)
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.
Sysop: | Keyop |
---|---|
Location: | Huddersfield, West Yorkshire, UK |
Users: | 493 |
Nodes: | 16 (2 / 14) |
Uptime: | 191:12:52 |
Calls: | 9,707 |
Calls today: | 2 |
Files: | 13,740 |
Messages: | 6,180,052 |