This theorem (or any of its alternatives/corollaries) are fine exercises of formal reasoning, but why draw such far-going epistemological conclusions?
I mean, we start with a specific formalization of logic (and arithmetics), then keep building on top of it using agreed-upon methods and procedures, and come to a result, that in terms of agreed-upon interpretation means any (sufficiently rich and consistent) theory (built according to this formalism) is incomplete. I have no problem with that, but how does this prove any limit to knowledge per se? I think it only proves limitations of the initially chosen formalism.
Not quite - it proves limitations to any chosen formalism. That’s why Godel’s theorem is so important, it isn’t only true within a particular formalism, it’s constructed so that it will be true in any (sufficiently powerful) formalism. Choose any axioms you like… so long as they are sufficiently powerful to perform basic arithmetic, Godel’s theorem applies.
Not quite - it proves limitations to any chosen formalism. That’s why Godel’s theorem is so important, it isn’t only true within a particular formalism, it’s constructed so that it will be true in any (sufficiently powerful) formalism. Choose any axioms you like… so long as they are sufficiently powerful to perform basic arithmetic, Godel’s theorem applies.
What about it? The article notes that Godel’s incompleteness theorem applies to the axioms of Peano arithmetic.
Clayton -
Um, you are right, I must have been thinking about something different at the moment. Nevermind this article.
My point is: Peano arithmetic is not a given, nor is Zermelo–Fraenkel set theory. Using them, and arriving at a problem raises a question of whether we are 100% sure we are using right foundations.
Note that I do not claim existence of any absolute theory or ability to (eventually) comprehend the universe fully. In fact, I strongly believe in the universe being incomprehensible by finite analysis. I just do not think Goedel’s theorem proves this.
That’s exactly the point - we cannot be 100% sure because there is always the possibility we have undiscovered inconsistencies. See, if we could prove that the system is consistent, Godel’s second theorem tells us that the system must therefore be inconsistent. Wiki says it pretty well, “For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, T includes a statement of its own consistency if and only if T is inconsistent.”
Well, true, Godel’s theorems don’t say anything about the universe one way or the other. However, they do say something about not just Peano arithmetic or ZFC but any formal system you may choose which is powerful enough to express ordinary arithmetic… which is basically any formal system that is interesting (the formal systems to which Godel’s theorems do not apply are so restricted as to be uninteresting). Godel’s theorems spell out the limits of what we can know about formal systems.
The theorem is basically saying no matter what you start with [initial assumptions and rules of deduction], there exists a proposition you cannot prove, even though it’s true. He also tells you what said proposition is.
So that even though it only proves the limitation of a chosen formalism, since that formalism was arbitrary, it proves it for all formalisms.
As an example of what is going on, if you prove something about a group G [with nothing else given about it but that it is a group], it is true of all groups, even though you only proved it for G.
I think I saw Chaitin mentioned here as proving something stronger, that you will not be able to prove most of the true statements, even though they are true.
I hoped my point was clear - as the theorem is expressed in specific metatheory, we cannot possibly say that it holds true in any imaginable metatheory. E.g., what if we use co-induction instead of induction as our main tool to define theories? What is we use constructive logic instead of classical one? I do not say that it is feasible (economically) to start the math from scratch to try and find a better foundation - I am not even sure it is possible - I just say the theorem does not automatically holds for every possible approach to formalisation of human knowledge. Let me reformulate my point in terms of a difference between being true and being provable - despite the conclusion of the Goedel’s theorem possibly being true for all formalisms, it is not proved (for all of them).
Andris, I recommend you read up on “effective methods”, there was a huge amount of discussion and debate about it at the turn of the 20th century. Godel’s theorems are specifically connected to answer open questions (at the time) about the extents of what can be known through the means of effective methods, aka formal systems. The term “effective method” is so broad as to include anything that is math/logic-ish, it’s basically any system or rules which are intelligible to a human brain and which are consistently followed at every point (in other words, you don’t change rules half way through or randomly violate rules). Godel’s theorems apply to any interesting logic/math-ish system that you can dream up, however exotic. Non-standard logics such as modal logic or quantum logic do not escape Godel’s theorem. Even hypercomputers (computers which can “solve” the halting problem) are subject to their own hyper-halting problem which means that Chaitin’s halting probability (and, hence, Godel’s theorems) apply to them as well. Non-deterministic machines are as subject to the halting problem as are deterministic machines. Godel proved that, for any effective method or formal system of sufficient power to express ordinary arithmetic, there exists true but unprovable statements (first theorem) and such systems are consistent if and only if they cannot prove their own consistency (second theorem). Chaitin extended this by showing that almost all true mathematical statements are unprovable in any given formal system, in other words, Godel’s theorems are not merely a philosophical curiosity but an all-pervasive attribute of formal systems.
“Goedel’s theorem [is] possibly … true for all formalisms, it is not proved (for all of them)”
False. Godel’s theorem is proved for all formal systems of sufficient power to express basic arithmetic. You’re confusing the “Godel sentence” which is the device that Godel used to prove his theorems with the theorems themselves. The Godel sentence is the thing that is true, but not provable, in any given formal system. To prove his theorem, Godel proved that such a sentence can be constructed in any formal system of sufficient power to express basic arithmetic. So no formal systems escape. Maybe “systems” which are not formal (systems that do not follow regular rules) are not subject to Godel’s theorems but how could studying such a system be interesting? Its behavior is not well defined so we would never really know what we’re talking about from one moment to the next.
You’re confusing the “Godel sentence” which is the device that Godel used to prove his theorems with the theorems themselves.
Not really, I meant the theorem itself (and chose the metacircular argument in spirit of Goedel on purpose). You might be right, I need to brush up on my theory of computation and formal logics, it’s been years since I last used them…
BTW, all kinds of computational impossibility arguments can be good to convert academics from statism to anarchism
Andris said that the theorem only proves there are limitations to the initially chosen formalism, and you replied by implying that you need certain axioms to perform basic arithmetic. This is the common response, but it always seemed totally bizarre to me. Do we really need to establish axioms to know that if I have 1 brother and 2 sisters I have 3 siblings?
There are formal systems that do not “express basic arithmetic”, or more accurately, do not define or develop basic properties of the natural numbers, and therefore do not meet the requirements of Godel’s hypothesis. Euclidean geometry is a perfect example.
I don’t know the status of Euler’s axioms w.r.t. Godel’s theorems but it may very well be that a sufficiently restricted set of geometric axioms would not meet the critieria for incompleteness under Godel’s theorems. But there are geometric axioms powerful enough to model arithmetic operations and these axiom sets are constrained by incompleteness.
I think you’re dealing with two unrelated issues. First, we do not need to choose any particular axioms in order to be able to do arithmetic, there are an infinite number of axiom sets which will permit basic arithmetic operations to be performed. The restriction that the axioms must permit basic arithmetic is the result of the fact that Godel’s construction explicitly uses basic arithmetic operations to encode the “Godel sentence” which says “This statement is unprovable” in the given formal system. So, as long as arithmetic is possible in the formal system under discussion - some formal systems, such as first-order logic, are too restricted to even be able to define the basic arithmetic operations - then Godel’s theorem applies since you could construct a Godel sentence in the system, a sentence which by its very construction is either unprovable in the system or the system is inconsistent.
You don’t need to “establish axioms” to know that 1 brother and 2 sisters is 3 siblings because you have a brain. Your brain contains all the circuitry needed to perform basic arithmetic or, at least, it contains all the circuitry needed to learn how to perform basic arithmetic.
No, you don’t need axioms for 1+2=3. But arithmetic has much more complicated results than that, e.g. Fermat’s Last Theorem. Peano hoped he would be able to get a list of axioms from which all results will follow, and gave a list of what are nowadays the generally accepted axioms of arithmetic.
Godel showed you can’t get all results from that list, or any other list.
Actually, Principia Mathematica doesn’t get around to proving 1+1=2 until 350 pages in … So, yes, you do need axioms and addition is actually a non-trivial operation if you have to define it from first principles. Look at the logic circuits for an adder in a computer to get an idea of why this is the case. They’re not super-complicated but, then, they’re not trivial, either. Addition just feels trivial because our brains are pretty good at small sums.
I thought this discussion died… Ok, let me try to clarify myself the last time.
Let’s take a computational rather than mathematical perspective, as this may be more natural at least to programmers. One can see (if squinting enough, a part of) the (first) Goedel’s theorem as a program, which accepts a definition of your formal system as an input, and provides a sententce in the language of this formal system that says that in this system this sentence cannot be proven.
Then the metatheory (meaning we are already reasoning out of scope of this formal system) kicks in - we say, either this sentence is true, and then the formal system contains some true but unprovable sentences, or this sentence is false, and then the formal system contains some false but provable sentences.
My gripe is exactly with this last step - for example, why do we think there are exactly two alternatives? Because our metatheory says so. This part of the reasoning is independent of the formal system we used as input, it is in a way hard-coded, so it is incorrect to say that it we can fully parameterize the theorem by any formal system we choose.
Anyway, there are so many simple impossibility results in computability and logic, that splitting hairs is not too useful (except as an exercise). For example, the number of all imaginable predicates on natural numbers (and this is almost the simplest functions that can be imagined) is uncountable, so only a tiny fraction of them can be expressed as a program of finite size (no matter how big).
So, yes, you do need axioms and addition is actually a non-trivial operation if you have to define it from first principles.
BTW, has anyone on this thread ever counted more than a few hundreds of real objects? How do you KNOW that axioms of arithmetics correspond to reality? How do you know that if you put one million grains in a pit, and then another million, that there are exactly two million grains in a pit? Just because your intuition says so? But it is trained on small counts. Because “laws” of arithmetics say so? But they were written to reflect our intuition.
