Misplaced Pages

Revision as of 10:16, 23 January 2010

This article has not yet been rated on Misplaced Pages's content assessment scale. It is of interest to the following WikiProjects:

Mathematics Top‑priority This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Misplaced Pages. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics Top This article has been rated as Top-priority on the project's priority scale. Please add the quality rating to the {{WikiProject banner shell}} template instead of this project banner. See WP:PIQA for details. Philosophy: Epistemology / Logic Mid‑importance This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to philosophy on Misplaced Pages. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Misplaced Pages.PhilosophyWikipedia:WikiProject PhilosophyTemplate:WikiProject PhilosophyPhilosophy Mid This article has been rated as Mid-importance on the project's importance scale. Associated task forces: /  Epistemology Logic

Gödel's incompleteness theorems was a good article, but it was removed from the list as it no longer met the good article criteria at the time. There are suggestions below for improving the article. If you can improve it, please do; it may then be renominated. Review: May 8, 2006.

Archives

Arguments (Nov 2005–Jan 2007) Archive 1 (Oct 2001–July 2005) Archive 2 (Nov 2005–Nov 2006) Archive 3 (Nov 2006–Nov 2007) Archive 4 (Dec 2007–Aug 2008) Archive 5 (Aug 2008–Oct 2009)

The introductory sentence

The introductory sentence should say what the basic result of Goedel's theorems are. This is the information that 90% of users are looking for and it should be the first thing they find in the article. The fact that the theorems are inherent limitations on any formal system is a secondary consideration. Consider the following examples

Example 1: Pizza is a thin bread covered and baked with flavorful toppings, usually including mozzarella cheese and tomato sauce. There are many variations of pizza, including New York thin crust, Chicago deep dish, and classic Sicilian. Pizza is the most widely consumed take out food in the United States.

Example 2: There are many variations of pizza, including New York thin crust, Chicago deep dish, and classic Sicilian. Pizza is the most widely consumed take out food in the United States. Pizza is a thin bread covered and baked with flavorful toppings, usually including mozzarella cheese and tomato sauce.

Starting this article with the fact that the theorems state an inherent limitation on formal systems without stating what that limitation is is like starting a pizza article with example 2. It's not good encyclopedic writing. —Preceding unsigned comment added by Philosofool (talk • contribs) 17:12, 6 November 2009 (UTC)

Actually, the version you reverted strikes me as being more parallel to

Pizza is a culinary dish tracing its origin to Italy. <Here follows the more precise description>

Think of it this way: start all the wikipedia articles that could be started that way that way.

Pizza is a culinary dish tracing its origin to Italy. <Here follows the more precise description>

Spaghetti is a culinary dish tracing its origin to Italy. <Here follows the more precise description>

Risotto is a culinary dish tracing its origin to Italy. <Here follows the more precise description>

This imaginary Misplaced Pages is placing an awful lot of emphasis on national origin of italian food, don't you think? I don't think this is a better way to start articles about italian food. philosofool (talk) 15:15, 8 November 2009 (UTC)

When you have a complicated theorem with lots of hypotheses, and where the conclusion itself, even given the hypotheses, is somewhat difficult to follow, I think it makes more sense to start with a higher-level description, a "why should I care?" type sentence. I'm very much against getting the higher-level description by leaving out stipulations or stating the conclusion imprecisely — especially in the case of the Goedel theorems we know where that goes. But I see no problem with starting with a general description of what the theorems do, in a form that no one can mistake for a precise statement of the theorems themselves. --Trovatore (talk) 20:10, 6 November 2009 (UTC)

For people who already understand the theorem and understand what these limitations mean, it might be good to start by saying This theorem applies only to cases that satisfy x, y and z. It stays that, for those case, A but for someone who doesn't know what an x, y or z is, it's not at all helpful to start talking about x, y, and z. Much better is to say This theorem says A. Part of the problem with science and especially math related articles in wikipedia is that they're written with an eye to precision that can only really be appreciated by a specialist not at a level that is helpful to a smart but less educated reader.

The best way to choose between two introductory sentences is to ask "if the article were only one sentence, which one would I want it to be?" Clearly, the fact that Goedel's theorems state limitations is important, but it's not as important as what the limitations are. philosofool (talk) 15:15, 8 November 2009 (UTC)

I strongly disagree with you. The actual content of the theorems is far too complicated for the first sentence. I'm going to put it back. --Trovatore (talk) 21:30, 8 November 2009 (UTC)

I also thought the reversed order by Þjóðólfr was slightly better. — Carl (CBM · talk) 12:33, 7 November 2009 (UTC)

nofootnotes tag

This page uses parenthetical references for inline citations along with footnotes for explanatory notes. As WP:FOOTNOTE says, "It is often desirable for an article to list sources separately from explanatory notes.", and this is what is done here. So I have removed the "inline citations" tag. I don't know what the purpose of the "cleanup" tag was, but I will wait a few days before removing it. — Carl (CBM · talk) 19:05, 27 November 2009 (UTC)

Hilbert's program

While Godel's theorem was interpreted as killing Hilbert's program by most mathematicians in the 1930's-1980's, it was not interpreted in this way by Hilbert, and I believe it is not universally interpreted this way anymore. Gentzen's 1936 proof of the consistency of arithmetic was considered satisfactory as a finitary proof by Hilbert (but not by many others). The reason is that Gentzen did not need to use any uncountable sets in the proof, he only needed countable ordinals. Whether the properties of countable ordinals should be considered finitary has been a point of contention. Many people say no, I personally would say yes, and I believe Hilbert said yes.

Hilbert comments on this issue in the "Grudlagen der Mathematische", which I don't think has been translated to English, so I can't read it. Unfortunately, Hilbert died a little after, and his program was abandoned. If somebody reads German it would be good to know exactly what he says. All I know is that he didn't feel that Godel's theorem was a serious impediment to his own program, and neither did Gentzen.

The idea that "finitary" means "provable in Peano Arithmetic" is certainly not what Hilbert had in mind, especially after 1931. In fact, since the statement "PA is consistent" is about finite mathematical objects (it doesn't mention any real numbers, it's just a computational statement), the axiom system PA+consis(PA) is perfectly OK, and is equivalent to ordinal induction up to epsilon-naught. What Hilbert wanted to do was to justify set theory by showing that the axioms are consistent only by making statements about computable objects. So Hilbert would have been fine with axioms of the form "consis(PA)" or "consis(PA+consis(PA))" iterated up to any recursive countable ordinal. It is pretty clear today that this process should be capable of proving the consistency of ZFC, although the requisite ordinal would be mind-numbingly large.

The modern program of reverse mathematics associated with Harvey Friedman keeps Hilbert's program alive. Followers of this approach believe that it is good to find fragments of second order arithmetic which are equivalent to chunks of mathematics. The reason they focus on second order arithmetic (I believe) is because it does not require talking about the set of all real numbers, so that it does not have to mention uncountable ordinals, or any other set theory monsters.

I think that many modern people believe that countable constructible ordinals are perfectly fine as finitary objects, so that there is no barrier to Hilbert's program of proving the consistency of ZFC from Peano Arithmetic plus additional axioms about these ordinals. So Hilbert's program is not affected in any serious way by Godel's theorem, but the theorem was important in showing how to go forward.Likebox (talk) 01:43, 4 December 2009 (UTC)

I noticed a reference to reverse math in an edit summary. While reverse math does clarify which parts of separable mathematics can be done in weak systems of second order arithmetic, it doesn't fundamentally affect the impact of Gödel's theorems on Hilbert's program. As Steve Simpson writes,

"The essence of Hilbert’s Program was to justify all of set-theoretical mathematics by means of a reduction to finitism. It is now well known that this task cannot be carried out. Any such possibility is refuted by Gö̈del’s Theorem. Nevertheless, recent research has revealed the feasibility of a significant partial realization of Hilbert’s Program. Despite G̈ödel’s Theorem, one can give a finitistic reduction for a substantial portion of infinitistic mathematics including many of the best-known nonconstructive theorems." (, pp. 1–2, emphasis in the original)

There are some philosophers who think that Hilbert's program is alive and well, or similarly that logicism is alive and well. They are discussed with detailed sources at Hilbert's second problem#Modern viewpoints on the status of the problem. But the dominant viewpoint in mathematical logic is certainly that G̈ödel's theorem made Hilbert's program impossible to complete in the way Hilbert intended. — Carl (CBM · talk) 01:45, 4 December 2009 (UTC)

Also, the most common contemporary definition of "provable in a finitary manner" is "provable in PRA". — Carl (CBM · talk) 01:50, 4 December 2009 (UTC)

That can't be right--- PRA can't prove hardly anything. I think that you mean PRA+induction, which is just PA. But quibbles aside, there is a dispute, and I don't think that it reflects NPOV to say "is interpreted" when "was interpreted" is undiputably true.

I disagree that the program cannot be carried out--- it all depends on what you mean by "finitism". If you mean "provable in PA" or "provable in PRA", the of course it it false by Godel's theorem. But if you mean "provable in PA + recursive countable ordinal axioms" (which are fully finitary objects), then Hilbert's program is alive and well.Likebox (talk) 01:59, 4 December 2009 (UTC)

"Tait in his 1981 paper argued that Hilbert's finitism is formalized by PRA. This conclusion is widely accepted in the f.o.m. literature." Simpson

WP:NPOV does require us to cover all viewpoints, but in relation to the prominence of each. As a second example besides the quote from Simpson higher up, read the introduction to "The Incompleteness Theorems" by Smorynski in the Handbook of Mathematical Logic. This also presents, very clearly, the viewpoint that Gödel's theorem rendered Hilbert's program impossible. There are many more such sources, but the Handbook is probably a compelling place to look for the mainstream viewpoint on a subject.

Our article does point out, lower down, that not everyone accepts this. But those people are generally philosophers, not people working in reverse mathematics. — Carl (CBM · talk) 02:08, 4 December 2009 (UTC)

You should find the context of this quote--- what does simpson mean by PRA? The thing that people call "PRA" today is a very,very limited system, which is much weaker than PA. If Simpson meant anything proven by arithmetic with primitive recursive function symbols and induction for all statements, then I would agree that this is what is meant by "finitary", since it might as well be PA.

But quibbles aside, I think you are wrong that mathematicians believe that this kills Hilbert's program in the sense described below. Although Trovatore is right that it does kill the second problem as originally stated.Likebox (talk) 02:23, 4 December 2009 (UTC)

Simpson means exactly what Tait meant, which is Primitive recursive arithmetic. Our article there also references Tait's 1981 paper. This is much weaker than PA, weaker even than RCA₀. On the other hand, I have no reason to think that when mathematicians say "Hilbert's program" they mean what you describe below. I expect they mean the original program to find finitistic consistency proofs for mathematics, as in Hilbert's second problem. — Carl (CBM · talk) 02:29, 4 December 2009 (UTC)

Fair enough--- they are all talking about the pre-1931 Hilbert program. So they probably were hoping to bootstrap from the weakest theory to stronger theories back then. But I know Hilbert had a more sophisticated view about what "finitary" means from some statements I ran across by him. The Grundlagen supposedly has a new Hilbert program as a response to Godel, following Gentzen, which I think is what I was calling "Hilbert's program" below. But I can't be sure, because I haven't read it.Likebox (talk) 02:42, 4 December 2009 (UTC)

LB, there is "no barrier to ... proving the consistency of ZFC from PA plus additional axioms" about the natural numbers, forget countable ordinals. For example, Con(ZFC) itself is a possible axiom about the natural numbers, and PA+Con(ZFC) easily proves that ZFC is consistent. But Hilbert's program was not to prove the consistency of ZFC; Hilbert didn't even know about ZFC. Hilbert wanted to reduce all arithmetical truth, or at least all Pi-0-1 truth, to a collection of axioms that was provably consistent by finitary means (whatever exactly that means). --Trovatore (talk) 02:03, 4 December 2009 (UTC)

I see. That's one thing I didn't consider. Yes, the original second problem asks for finite collection of axioms which can be used to prove itself consistent and which can in addition solve all arithmetic questions. That is certainly killed by Godel's theorem, and this must be stated clearly.

The Hilbert program that is alive is something that you could call "Hilbert's program prime", the modified Hilbert program in response to Godel's theorem. This no longer asks for a finitary proof of all of mathematics, but only for a finitary proof of the consistency of set theory and large cardinals from the consistency of arithmetic plus additional "finitary" assumptions which are natural.

Of course, you could add "consis(ZFC)" as an axiom, but that axiom is unnatural, since nobody has any a-priori reason to believe that ZFC is consistent (that's the whole motivation). So you need a way of generating new axioms which are obviously true for completely finitary reasons, and which are strong enough that they are equivalent in strength to a theory like ZFC with uncountable ordinals. The source of these new axioms is provided by Godel's theorem. Starting with PA, you have the natural chain of theories: consis(PA) and consis(PA+consis(PA)) and so on up to any recursive ordinal. These theories which Godel provides go up in strength, and certainly somewhere along the chain they should prove consis(ZFC). This would be a satisfactory finitary proof, but it requires a description of large countable ordinals.

To give you an example of why this is needed, consider the question: is ZFC omega consistent? Suppose ZFC were consistent, but not omega-consistent. Then it would be possible to prove the existence within ZFC of solutions to some diophantine equation which does not have any solutions at all. How can you be sure this doesn't happen?Likebox (talk) 02:15, 4 December 2009 (UTC)

As far as I know, no one working in ordinal analysis has ever gotten even remotely close to a "natural" proof-theoretic argument for the consistency of ZFC, or even second-order PA. I agree that the Gödel theorems themselves do not rule out such an argument. But as far as I know, no one ever said they did, and I don't see how you could reasonably read the current text as saying they do. So basically I don't see the point as particularly relevant to this article. --Trovatore (talk) 02:20, 4 December 2009 (UTC)

There is an ordinal analysis for ${\displaystyle \Pi _{2}^{1}}$ comprehension, but not for ${\displaystyle \Pi _{3}^{1}}$ comprehension; full second-order arithmetic is far away. — Carl (CBM · talk) 02:24, 4 December 2009 (UTC)

To Trovatore: you are right, I misread the text. It is mostly about the second problem, not "Hilbert's program prime". The question of naturalness is actually somewhat subtle--- you can use systems of equivalent strength to ZFC to define proof-theoretic ordinals in a way that might be called artificial, but it's a question of taste.

The real question is whether you can describe the ZFC proof-theoretic ordinal in any natural combinatorial way. It is certainly very difficult, but I think that most logicians believe that it is surely possible.Likebox (talk) 02:28, 4 December 2009 (UTC)

(deindent) It would still be nice if some German speaker could reveal what Hilbert was saying in the Grundlagen.Likebox (talk) 02:37, 4 December 2009 (UTC)

Continuing to look at actual references, I opened Feferman's "What rests on what" from the bottom of Primitive recursive arithmetic. On p. 2, Feferman says,

"The driving aim of the original Hilbert program was to provide a finitary justification for the use of the `actual infinite` in mathematics. ... It is generally acknowledged that the Hilbert Program as originally conceived could not be carried through even for elementary number theory PA ..., in consequence of Gödel's 1931 incompleteness theorem."

This is exactly what our article says. Also, Feferman does not commit to Tait's argument that PRA exhausts finitism, but Feferman does say on p. 12 that there is no known finitistic justification of ${\displaystyle \Sigma _{2}^{0}}$ induction. — Carl (CBM · talk) 02:39, 4 December 2009 (UTC)

You don't need this reference--- you already convinced me that I was wrong. Everybody knows that this form of Hilbert's program was killed. But Hilbert has a response to Godel which is in the Grundlagen, and it would be nice if some German speaker could reveal what it was, because I strongly suspect it's what I wrote above.Likebox (talk) 02:45, 4 December 2009 (UTC)

Bad Example?

Regarding the example of the parallel postulate in Euclidean geometry under the section 2.1 Meaning of the first incompleteness theorem: Euclidean geometry is consistent with the parallel postulate or it's negation making this NOT an example of "Euclidean geometry minus PP"'s incompleteness.

The difference lies in the fact that PP is neither true nor false according to the other axioms of standard Euclidean geometry. It is only when a statement is true within your system and unprovable that makes your system incomplete. G is true within the system (because it cannot be false) but it also cannot be proven within the system (because that would be a contradiction).

Unfortunately, examples of true statements within mathematics that are unprovable exist, but it is impossible to know whether or not they are true because of the fact that they are unprovable. Therefore, I think a more suitable example illustrating incompleteness would be an instance where it is NOT KNOWN whether a statement can be true or false within the system, and is also provably unprovable.

E.G. The PP is provably unprovable from the rest of Euclidean Geometry, but it is known that it or it's negation together with EG is consistent if EG itself is consistent. The Continuum Hypothesis and it's negation are provably unprovable from ZFC, HOWEVER, although CH is known to be consistent with ZFC (which means that CH may be 1. true within the system xor 2. neither true nor false in the system) it is not currently known whether the negation of CH is consistent with ZFC (to the best of my knowledge. If it IS known, then consider my argument under the supposition that it i sn't, and come up with a different example satisfying the condition that it is not known whether the statement or its negation is consistent with whatever system.) This means that IT IS POSSIBLE that CH is actually true within the system, we could just never know it for fact (unless you are of the philosophical bent that rejects that sort of thing. But then, why would you be reading the discussion page on Godel's incompleteness theorem?). I.E. it is possible that CH illustrates the incompleteness of ZFC, where PP in no way illustrates the incompleteness of EG.

A simpler and more easily understood example would be the Goldbach conjecture. This would be nice because, although it is not known to be provable or unprovable, most people would agree that it is probably true, and the fact that it has not yet been proven means that there is a good chance that it is unprovable. And since we have to work within the realm of maybes anyway, it is possible that the Goldbach conjecture provides an illustration of the incompleteness of ZFC+whatever.

74.247.111.36 (talk) 17:21, 2 January 2010 (UTC)Scott Brown csbrown@gmx.com

I disagree that a statement which is not even known to be unprovable (Goldbach's conjecture) is a good example of an unprovable statement. On the other hand, the question whether the parallel postulate was provable from the remainder of Euclid's axioms was open for a long time, so it's a historically motivated example. Also, the parallel postulate is true in the intended model of Euclidean geometry (the plane), just as the Goedel sentence of Peano arithmetic is true in the intended model of PA. There are plenty of models of PA in which the Goedel sentence of PA is false, just as there are models of the remainder of Euclidean geometry in which the parallel postulate is false. — Carl (CBM · talk) 03:02, 4 January 2010 (UTC)

But there are essential differences between between the Godel sentence and the parallel postulate and between the Godel sentence and Goldbach's conjecture. The Godel sentence is true in the "intended model" of PA, when that model is defined computationally. It is a question of philosophy whether you put axiom systems first and consider them fundamental or whether you put computation first and take that as fundamental. There are schools of thought which treat computation as more fundamental than axioms, and this to my mind is the correct point of view.

If you take the computational perspective, the intended model of PA, the integers, can be given a definition in terms of computer programs, by providing specific algorithms for addition and multiplication. The precise axioms are not provided by this definition. But a computational definition is unambiguous, so the question of whether Goldbach's conjecture is true or false is a question about the halting of a certain computer program and is absolute. It is to my mind not reasonable to say that it can be neither true of false, because you can run the program. The point is that the computational definition of the integers is fully understood by our minds from the algorithmic definition, even though no finite computer program can list all its true properties.

The Godel sentence G for a theory T states that "T is consistent", which is also a statement about the non-halting of a computer program, so in the computational philosophy it is also absolute. That means that PA extended by "G is true" is a correct model for integer computation, while PA extended by "G is false" is an incorrect model for the integers. The point of Godel's theorem is that for any algorithmic method of producing true statements about the integers, one can pass to a stronger algorithm which adds "this algorithm proves no contradiction" as an axiom. Given any infinite increasing sequence of stronger and stronger algorithms which prove no contradiction, one can pass to a stronger algorithm which runs all of them in parallel to produce all their theorems jointly. These two processes are the same as "ordinal increment" and "ordinal limit", and explain why ordinal systems of set theory are good models for stronger systems of mathematics.

The main article of faith (and so far it seems to be a pure article of faith) is that Godelization repeated ordinally many times will eventually prove every absolute theorem. So that Goldbach's conjecture is either provable or refutable in a strong enough system. So Goldbach's conjecture is not a good example of a proposition like Godel's sentence which is an obvious candidate for a new axiom.

The parallel postulate is better analogy, but also not perfect. Like Godel's sentence, it is a postulate which you find to be true of your intended model and which you add as an axiom. But once you add the parallel postulate, you uniquely determine plane geometry.

Strictly speaking, this is only true in Hilbert's geometry. Euclid's system is incomplete, because the flat two-dimensional Minkowski space-time of special relativity satisfies all the axioms of Euclidean geomety including the parallel postulate, but is not the same as Euclid's two-dimensional plane. There are implicit assumptions in Euclid about which side of a line points occur on, and about distances always being comparable, and these assumptions are only explicitly axiomatized by Hilbert. Without axioms for sided-ness which are strong enough to decide whether a point is inside or outside of any closed polygon, Minkowksi space is just as good a model as Euclid's.

The parallel postulate completes Hilbert's sided version of Euclidean geometry because this geometry is not computationally complete--- it is incapable of describing an arbitrary computation. It is very similar to the axioms for a real closed field, with limited functions corresponding to circles and lines. The theory is completely decidable--- you can tell whether any statement is a theorem of Euclid's geometry or not. There are perfect computational models for Euclid's geometry with or without a parallel postulate.

So the parallel postulate has the property that either it or its negation is consistent and produces an interesting computable model. But taking the negation of the Godel sentence as an axiom produces a model which is not computationally defined. These models are defined only by the axiom system, not by specific algorithms for addition and multiplication. So unlike the parallel postulate, you are more or less forced to consider the Godel sentece true in a computational point of view.Likebox (talk) 13:59, 4 January 2010 (UTC)

I think that Likebox raises very interesting philosophical questions, but classically godel's theorems (godel being a platonist himself) are taken with regards to an axiomatic system and regarding the ability to prove statements within that axiomatic system (as opposed to a computationally defined system), regardless of the model that you are using. With this in mind I would like to preface the remainder of this discussion with "Suppose we have an axiomatic system". Now, to answer Carl. Since, Historically, whether the parallel postulate was provable from the remainder of Euclid's axioms was an open question means that it WAS, at some time in the past, in the same situation that Golbach's conjecture IS right now, which is the situation where it is not known whether it is consistent with the rest of the system (if the system is consistent), true, its negation is consistent with the rest of the system (if the system is consistent), or its negation is true. Admittedly Goldbach's conjecture is not in any way an ideal example, but the fact that we do not know certain things about it illustrates an important point.

It seems like the rating for an example of this situation should be handled so that an IDEAL example (as in the best that we could possibly do) would be thus (and I will explain the less obvious points): 1. it is simple and easily understood (which PP satisfies) 2. it is known to be unprovable (which PP satisfies) 3. it is known to be consistent with the rest of the system (which PP satisfies) 4. it is not known whether its negation is consistent with the rest of the system (PP does not satisfy this point) 5. it is almost certainly true, as evidenced inductively within the confines of the system, but its exact truth value status is unknown (which PP also does not satisfy) 6. It would also be nice if its negation were unprovable but this seems less important if our purposes are simply illustative. (which PP satisfies)

Regarding 5: Obviously if the example were known to be true or false within the axiomatic system then it would fail to be an example because it must necessarily have been proven to be true or false. If neither the example's truth nor falsehood is implied by the system then we find that, if 3 is satisfied, 4 must not have been. This is bad because if the example is known to be consistent with the rest of the system and its negation is known to be inconsistent with the rest of the system, then obviously the statement is provably true. (as long as your system of logic allows for RAA proofs, which is, I think, standard for most systems. However, in order to have a good, universally illustrative example, whether you believe in RAA or not it may still be a good idea to have an example for which the negation is not known to be inconsistent with the rest of the system).

Regarding 4: If its negation is known to be consistent with the rest of the system, then it falls under a totally different category of statements with respect to the system. Goldbach's conjecture does NOT satisfy all of the above requirements (failing 2, 3, and 6), however, I was suggesting Goldbach's conjecture to illustrate the fact that criterion 4 is very important to correctly illustrating Godel's theorem. Even moreso, I think, than criterion 3 (in the sense of it's consistency being KNOWN) because the whole reason for having an example is to prevent statements that are shown to exist by Godel's theorem (even if it is Godel's sentence G and only G) from being confused with statements that are neither true nor false within the system (i.e. it and its negation are consistent with the system if the system is consistent). Statements of THAT type were trivially known to exist before Godel's theorem. Godel's theorem shows that there are statements such that the axiomatic system implies their truth, but we are unable to prove it using our system. Really, I think that there must be a much better example than either Goldbach's conjecture or the Parallel Postulate that simply has not presented itself to me. My hope is that someone more knowledgable than I about such examples can find one that satisfies the above criterion as much as is possbile. Before such an example is found, I still feel that the parallel postulate is a really terrible example because it is exactly the sort of thing that we are attempting to contrast G against, and almost anything would better serve the need (even, as a terrible but slightly less terrible choice, Goldbach's conjecture).

Browncs (talk) 16:58, 15 January 2010 (UTC)

(deindent) You misunderstood my main point. You are saying "Goldbach's conjecture is not known to be provable from the rest of the system". But what do you mean by "the rest of the system"? Do you mean the Peano Axioms? ZFC? Peano Axioms extended by the statement "PA is consistent"? Large cardinal theories?

Each of these axiomatizations can be used to describe the integers, and each of them prove more and more theorems. So it might be the case that Goldbach is independent of PA, but provable in ZFC + large cardinals.

That's the point that I was making: there is no one unique axiom system which we use to define "the integers". We define them by describing their computational properties, and then we show that many of the properties can be proven by induction, and others can be proven using set theory (analysis, measures and large ordinals).

Since mathematicians consider practically of these axiomatic systems as a good system for proving theorems about the integers, it makes no sense to say "Goldbach could be independent". Independent of ZFC? So what--- just go to large cardinals. Independent of these large cardinals? Just add the axiom "there is a model for this large cardinal theory". There is no limit to the sophistication of axiomatic systems, and it is an article of faith (which you should believe) that if Goldbach's conjecture is true, it has a proof somewhere along this indescribable chain of theories.

The statement "Godel was a Platonist" is neither here nor there. Most mathematicians are as much Platonists regarding the integers as Godel was. The issues of "Platonism" vs. "Formalism" mostly come up when intepreting the real numbers or huge infinite sets.Likebox (talk) 23:22, 15 January 2010 (UTC)

Well, the issue isn't that Goldbach may be provable within some axiomatic systems and not others, the issue is that within any fixed axiomatic system, Goldbach (or whatever, insert conjecture here) may be true within that system (i.e. it may, in fact, not be the case that there is an even integer which cannot be expressed as the sum of two primes) but is unprovable within that system. Agreed that you could just take ZFC+Goldbach as your new system, but the issue (especially with Goldbach) is that if you do that, how do you know that your system has not just become inconsistent? If you take ZFC+Goldbach, it may very well be that case that Grahams number + 1 is an even number that cannot be written as a sum of two primes, and this would mean that ZFC+Goldbach was an inconsistent system. So it is NOT the case that Goldbach (or something that implies Goldbach) can just be arbitrarily added to the system.

In fact, in my earlier post suggesting qualities of a good example, if we had an example that satisfied all of these properties, then that statement could indeed be added as an axiom without issue. However, its NEGATION may or may not be able to be added without issue. If the statement is an example illustrating Godel's theorem, then its negation CANNOT be added (though this will be unknown to us) no matter what model you are using, since (axioms)+(false statement) is necessarily an inconsistent system. If the statement is NOT such an example (like PP) then its negation can be added in its stead and everything is just fine. The issue, once again, is that PP is KNOWN not to be an example illustrating Godel's theorem, and, though we have no examples save G that we know to BE a bona fide example, we can at least use something that COULD BE an example and for which there is heuristic evidence that it is indeed such an example. Goldbach's Conjecture is such a case, though there are probably much better ones out there, namely propositions that are known to be unprovable (which would be much much nicer, as Carl has already stated) but that are not known to be independent of the system in question. 69.85.217.236 (talk) 16:27, 19 January 2010 (UTC)

You are confused about something when you say "Goldbach (or whatever, insert conjecture here) may be true within that system". A statement is not true or false within a theory, it is true or false within a model of the theory. When people say that the Godel sentence of a theory is true, they mean it is true in the standard model of arithmetic, ω. However, the negation of the Godel sentence of a consistent effective theory can be added to that theory, resulting in another consistent theory that happens to not be satisfied by the standard model of arithmetic. The only way that adding a sentence S to a theory can result in an inconsistent theory is if the theory already proves the negation of S. — Carl (CBM · talk) 16:36, 19 January 2010 (UTC)

Just to add--- I never said you could add Goldbach to your system--- you obviously can't. The only thing you can add to your system is stuff like Godel's sentence--- things that are obviously true. You can add "this theory is consistent" and "this theory plus the theory is consistent is consistent" etc, etc, up to any computable countable ordinal.

The chain of theories is not gotten by adding nontrivial statements, only by adding "trivially true" but unprovable statements. Somewhere along this chain of theories, you probably end up proving Goldbach's conjecture (or maybe it's false).

The point is that if you have an axiom system that does not prove or disprove Goldbach's conjecture, then this axiom system does not describe only the integers. It also describes the "integers-prime" which are integers including symbol that represents an infinite even number which cannot be written as the sum of two infinite primes. These alternate models, these alternate symbol systems, are just as good as the integers as far as the axioms go.

The integers are defined a-priori as a computational model, not by axioms. The axioms we use to describe them are unlimited in their complexity. Instead of going up using Godel's theorem, by adding "the previous system is consistent" to the old theory, people go up using the "reflection principle", but that's just a set-theoretic way of saying the same thing.Likebox (talk) 02:23, 20 January 2010 (UTC)

Proofs

This article is lacking a clear proof of the theorem, because it follows the original work of Godel too closely, without paying too much attention to subsequent development, especially the development of computers. The proof of the theorem needs to be included, so that the theorem can be understood by everyone.

Halting problem

To understand how to prove the theorem, it is important to know how to prove closely related results in computer science, results which came after Godel, but whose proof was largely modelled on the proof of the incompleteness theorem, and which include this theorem as a special case. The earliest of these results is the statement that the Halting problem does not have a solution.

The Halting problem: there is no computer program "HALT(X)" which can take the variable X, which contains the code for a computer program, and tells you whether the code X halts (stops running) or doesn't halt (runs forever in an infinite loop).

The easiest way to present the proof of the halting problem is to use what is sometimes called the "fixed point theorem". The fixed point theorem says that it is always possible for a program to include a subroutine that prints its own code into a variable or region of memory.

This standard result can be proved by construction. Using "C", it is a straightforward exercise to write such a subroutine: Include a variable Q which is declared to contain the code of the program, except for the part which says "Q= blah blah blah". Replace this part of the code with "Q= XDQF#!@#". Then to print out the code of the program into memory, you print out Q, except taking care to replace the nonsense string with the contents of Q surrounded by quotes. In most recursion theory texts, the same result is called the recursion theorem or the Kleene fixed point theorem, and is proved in the same way with recursive function calls instead of sprintf.

The proof that the halting problem is undecidable is then completely straightforward, since all the subtlety is in the act of printing your own code:

Given HALT(X), write SPITE to do the following:

1. Print its own code into a variable R
2. Compute HALT(R)
3. If the answer is "Halts" go into an infinite loop, otherwise halt.

In other words, SPITE asks HALT "What do I do?" and then does the opposite. Obviously whatever HALT says about SPITE, it is wrong.

The same method of proof obviously works for any property of the output. For example, if HALT(X) claims to tell you whether the program X returns the value "1" or the value "0", it cannot work for the same reason. You can always write a program to spite the prediction.

Godel's original theorem

The proof of Godel's theorem, following Godel's original treatment, is exactly the same. Godel's theorem states that given an axiomatic system S which is computable (meaning where there is a computer program which can deduce all the consequences of S), and which can describe the integers well enough to describe computer programs (which are after all manipulations of memory, or large integers), then there is a true theorem which is not provable.

Consider the program GODEL which:

1. Prints its own code into a variable R
2. Deduces all theorems of S looking for "R does not halt"
3. if it finds this theorem, it halts

In other words, GODEL uses the axiom system S as a halting-predictor, and spites it. If GODEL halts, it is only because S has proved that it doesn't. The statement "GODEL does not halt" is the Godel sentence G for the theory S. It is true, but unprovable.

Logical form of the construction

Any such proof can be stated in two ways, in terms of formal logical statements, or in terms of explicit computer programs. Godel originally stated the result in the language of formal logic, because computation was not yet defined.

The tranlation is as follows: if GODEL halts, then S proves that GODEL does not halt, and vice-versa. So the statement G, "GODEL does not halt", is logically equivalent to "S does not prove GODEL does not halt". So the Godel sentence G is if and only if equivalent to "S does not prove G", meaning "S does not prove this statement".

The way Godel originally constructed such a statement is to explicitly define the logical process of step-by-step deduction within an axiom system as a simple type of computer program, a primitive recursive function. By iterating this primitive recursive function, he could find all the theorems. He then constructed a statement which asserts "I am unprovable" just as above, except he incorporated the proof of the fixed point theorem. The fixed point theorem was later isolated by Kleene, while the notion of computaiton and the halting problem were isolated by Turing.

A reasonable axiom system S that describes computations will be able to follow a computation that halts. So if a computer program X halts after a finite time, then S can follow all the steps, and see that X halts, figure out the return value, etc. This can be stated in two different looking ways, in terms of computation, or in terms of formal logic:

An axiomatic system S which is strong enough to describe computations has the following property:

1. If X halts, S proves that X halts
2. If S proves X then S proves that S proves X

Statement 1 implies statement 2, since the program which looks for a proof of X in S is a halting program if and only if X is provable.

The opposite statements don't necessarily hold:

1. X can run forever, but S can falsely prove that it halts.
2. S can claim that it proves a theorem A, when it actually doesn't.

If a program X runs forever, but an axiom system S proves falsely that it halts, then this axiom system is called omega inconsistent (actually a special kind of omega inconsistency, called sigma-one inconsistency).

Godel's second incompleteness theorem

Note that:

1. if S is consistent, then GODEL does not halt (ie consis(S) implies G).
2. if S is inconsistent, then it proves any theorem, so that in particular GODEL halts (not consis(S) implies not G).

This means that the Godel sentence G is if and only if equivalent to "S is consistent". So if an axiom system cannot prove G, that's the same as saying that an axiom system cannot prove its own consistency. This holds whenever the proof of Godel's theorem can be carried out within S.

Rosser-Godel theorem

The usual statement of the incompleteness theorem is that there are statements which can neither be proved or disproved. While S cannot prove GODEL does not halt, it could prove Godel halts without contradiction. Then GODEL would run forever, but S would falsely claim that it halts.

So G is not necessarily an example of a statement which cannot be disproved. To construct such a statement, consider the program ROSSER which:

1. Prints its own code into R
2. Deduces all theorems of S, looking for the theorem a) R returns 1 b) R does not return 1
3. if it finds a), it returns 1 and halts. If it finds b) it returns 0 and halts

The axiom system now cannot prove either that ROSSER returns 1, or the negation that ROSSER returns 0. The statement "ROSSER returns 1" is neither provable or disprovable.

To convert this to logical form, consider

1. "ROSSER returns 1" if S proves "ROSSER returns 0" first
2. "ROSSER returns 0" if S proves "ROSSER returns 1" first

So if you call statement G: "ROSSER returns 1", then G is equivalent to "If S proves G, then S proves the negation of G first". This is ROSSER's preferred language.

Lob's theorem

Consider the program LOB(X) which takes as input a statement X:

1. It prints its own code into R
2. It deduces all consequences of S, looking for the theorem "R halts implies X"
3. If it finds this theorem, it halts.

note the following:

1. LOB halts if S proves X (since then it proves anything implies X)
2. if LOB halts, S proves X (since it proves LOB halts implies X, and also that LOB halts)

Therefore LOB halts iff S proves X. If this can be formalized in S, then S proves "LOB halts iff X"

But LOB halts if and only if S proves "LOB halts implies X", or inserting the previous equivalence, if and only if S proves "(S proves X) implies X". So an axiom system proves "(S proves X) implies X" iff "S proves X".

Similarly LOB halts iff S proves "LOB halts implies X", or inserting the equivalence "(LOB halts implies X) implies X", or "((S proves X) implies X) implies X". So this double recursive construction is provable only if S proves X.

This material should be included here and on appropriate pages.Likebox (talk) 07:31, 22 January 2010 (UTC)

This has been discussed over and over. Inserting it into articles would violate your edit restriction. — Carl (CBM · talk) 12:38, 22 January 2010 (UTC)

And it will be discussed AGAIN and AGAIN. I am under no editing restrictions--- I am asked to keep to 1RR, and I have complied with this voluntarily. So do not be under the impression that I am somehow going to go away. This will never go away as long as I am around.

The reason I am bringing it up now is because the old material has been archived, and it is important that new editors, and interested readers have access to the proof somewhere immediately accessible. Since the issue is not going to go away, I will suggest that you explain why you think that this material is inappropriate, and I suggest that you don't archive the discussion, so that it will not have to repeat.Likebox (talk) 22:49, 22 January 2010 (UTC)

Actually, you are under an editing restriction; see Misplaced Pages:Editing restrictions. You contributed to the relevant discussion, so I'm sure you already realized that. — Carl (CBM · talk) 23:10, 22 January 2010 (UTC)

I am sorry--- but there is no editing restriction. You are mistaken. Anyway, as I said, I am not going away.Likebox (talk) 23:28, 22 January 2010 (UTC)

So long as you are aware. I am not planning to discuss the material with you again; you may find my previous comments in the archives. — Carl (CBM · talk) 23:31, 22 January 2010 (UTC)

That's good, because I am sick of talking about it. I only placed it here because the old discussion was archived. The point of this is to inform readers that there is a simple presentation of the proof. Eventually, when there is another editor willing to back me up, it will get inserted. Until then, it is good enough to keep the proof on the talk page.Likebox (talk) 23:35, 22 January 2010 (UTC)

I reread the discussions on editing restrictions, and all I saw was that I am on some sort of probation. There is no restriction on the editing, but I am asked to comply with 1RR, and keep everything civil. I intend to do that. All the rest of the proposed editing restrictions that you kept asking for were rejected, for good reason.Likebox (talk) 23:55, 22 January 2010 (UTC)

I think you did not look thoroughly at the link Misplaced Pages:Editing restrictions that I gave above. Under your name, it says,

If User:Likebox makes any edits deemed to be tendentious, point of view pushing, addition of original research, or disruptive by an uninvolved administrator, Likebox may be blocked. After three incidents the block length may increase to one year.

There is no mention 1RR there. This was discussed in the section Results in the ANI discussion I linked above. — Carl (CBM · talk) 23:59, 22 January 2010 (UTC)

• All unassessed articles
• Unassessed mathematics articles
• Top-priority mathematics articles
• B-Class Philosophy articles
• Mid-importance Philosophy articles
• B-Class epistemology articles
• Mid-importance epistemology articles
• Epistemology task force articles
• B-Class logic articles
• Mid-importance logic articles
• Logic task force articles
• Delisted good articles