Talk:Gödel's incompleteness theorems/Archive 6

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 Wikipedia 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." ([1], 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 [2]

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 $\Pi _{2}^{1}$ comprehension, but not for $\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 $\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 0 and halts. If it finds b) it returns 1 and halts

The axiom system now cannot consistently prove either ROSSER returns 1, or the negation ROSSER does not return 1. 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)

A question about the "modern proof"

Hi.

Likebox has turned my attention to the discussion about the "modern proof". Though I was the original author or the "proof sketch" article 3 years ago, I am no expert in this field and was only happy that experts took over; I also didn't follow what happened with the related articles for quite a long time. However, it seems that Likebox's suggestion has a great pedagogical value, as long as its limitations are explained. I saw tha Carl (= CBM) promised to write something about it, after a written source has been found by CeilingCrash, but I see no such thing.

I don't believe in giving unsourced material here, but I do think that sourced material can and should be explained in a simple way, when such a way is found. Even if the terminology is non-standard, it can be used as long as it is understood that this is only an intuitive "lay-man perspective". For example, if you want to explain what a topological interior of a closed set is, you may say something like "one may think of the relation between a closed set to its interior as similar to the relation between an apple to the apple without its peel". Well, maybe that's a bad example, but I hope you understand my meaning.

Dan Gluck (talk) 12:45, 30 January 2010 (UTC)

On the one hand, Wikipedia articles are not primarily intended to be pedagogical; things that we could put into class notes are not always appropriate.

There are many published proofs of Godel's incompleteness theorem using computability. Several of them (5 in fact) are referenced in the article already, in the section Relationship with computability. A key difficulty with incorporating Likebox's proof sketches has been that Likebox has disagreed with efforts to rewrite them into the standard language of the field, which would be a requirement if they were incorporated into the article.

It's also important to note, in order to understand the difficulties with Likebox's proof sketches, that the sketches omit the longest and most important part of the proof, which is the arithmetization of syntax. Godel's theorem is not just that some formal system is incomplete: it's that many formal systems in the signature $\langle 0,1,+,\cdot ,=\rangle$ are incomplete. Likebox's proof sketches implicitly rely on Kleene's T predicate being available in the formal system at hand, and so to make the the sketches into full proofs would include proving the correctness of the T predicate. In the article we do not include full proofs, but we would still need to link to the T predicate article.

Similarly, Likebox's sketches do not include any verification that the construction is correct, as in our "Proof of independence" section. It is unlikely that an untrained reader will see, with no prompting, what is going on in any proof of Goedel's theorem.

Thus a generous interpretation of Likebox's proposal is that we could replace the section "Diagonalization" in our proof sketch, which is the section of the proof sketch where the Goedel sentence is actually constructed. The previous section "Arithmetization of syntax" and the following section "Proof of independence" would still be necessary. Switching the construction in this way would not actually make the article shorter, unless we substantially lower the level of detail in which we discuss the proof, which is what is done in the sketches Likebox has posted above on this page.

But the particular construction of the Godel sentence that is presented in the "Diagonalization" is the one we should include here. It's the construction that corresponds directly to the Liar paradox, and which leads to the interpretation that the Godel sentence says "I am unprovable".

It is also arguable whether Likebox's proofs are actually easier for a general reader to understand. There's no reason to think that a general reader will be familiar with computability theory, the halting problem, and self-printing programs. Moreover, by the time we expand the proof sketches to a level fit for the article, we will have to mention Kleene's recursion theorem for the construction and Kleene's T predicate for the arithmetization of computability. For the construction already in the article we have to mention the Diagonal lemma for the construction as well as results on the arithmetization of syntax. There's no gain in simplicity there.

For readers who are familiar with computability, we already give numerous pointers to texts that explain the computability aspects better than we can, because those texts have more space to do it. — Carl (CBM · talk) 13:41, 30 January 2010 (UTC)

Also, note that the proof via Matiyasevich's theorem, discussed in the article, is very clean because it can avoid arithmetization entirely, only requiring that the theory can handle the integers as a definitional extension. The downside is that Matiyasevich's theorem itself is not simple to prove. But for readers who want a short proof of Goedel's theorem and are willing to accept computability results, this proof method is ideal. — Carl (CBM · talk) 13:50, 30 January 2010 (UTC)

This has been a long comment, but I will respond very briefly:

First: What is the "T-predicate"? it is the description of the operation of a computer as a statement of arithmetic. This is what allows statements of the form "This program halts" to be turned into a statement "forall N, the function F iterated N times on the integer K will not have this-and-such binary digit equal to zero".

Constructing the Kleene T-predicate is considered "difficult" by some, but this is one of those things that modern readers can just take for granted. The function F is the function that takes the computer one processor step forward in time. The integer K is the memory state of the computer at time 0, and the condition that this-and-such binary digit is equal to zero is the condition that programs halt. The resulting statement is easily seen to be a statement of formal arithmetic, at least if enough functions are included to make a function "F" that can act as a computer, and anyone who knows modern computers can see this immediately, without recourse to Kleene's construction.

I consider this too obvious to prove today. On the other hand, if someone wishes to prove this, I don't care.

Second: The text does not need to be modified for the untrained reader to see what is going on. Just ask any high school student, they can see what is going on. I presented this proof to people in many walks of life, and I have never had anyone who didn't pause, think for a few minutes, and say "ok, I see".

Third: I don't want the proof sketch to incorporate this discussion, because the diagonalization constructs things the way Godel did originally, which is a separate discussion. This thing assumes a whole bunch of modern stuff is understood--- like computers, the notion of "printing your code", etc. There is no need to mix and match.

Fourth: Matiyaseyvich's theorem uses undecidability of the halting problem within it, and is as unsuitable for this page or this discussion as string theory is for an article on special relativity. It can be intimidating to newcomers to bring up such an advanced result for no reason.

Finally, the text I presented above is short, and can be added as is. I worked hard to make it clean. These points have all been made before, so I will stop here. For further detail, I will refer the reader to the archives.Likebox (talk) 07:45, 31 January 2010 (UTC)

The points have been (mostly) made before, and also refuted before. Whether you disagree with the refutation doesn't mean either your arguments or the refutation is correct; but there is a Wikipedia consensus that your arguments are either not correct or not relevant. (And that you consider the arithmetization of the T-predicate obvious doesn't mean that it is.) — Arthur Rubin (talk) 08:34, 31 January 2010 (UTC)

That's right--- there was a consensus before, and there is always a chance that the new consensus will shift. I will be patient, and so should you. I consider the T-predicate obvious because it is obvious--- anyone can see that a statement about a computation is a statement about arithmetic, and if they can't, they should go learn about computers.Likebox (talk) 08:42, 31 January 2010 (UTC)

Carl's arguments are quite convincing. Additionally, after some thought and reading again the "proof sketch", I think it's more understandable to the wide audience as it is than the "modern" proof, and also emphasizes important points. The modern proof is arguably easier for people with some background in computing sciences and programming, but these people can just follow the proof already given there and jump over parts which are obvious to them. Dan Gluck (talk) 20:45, 3 February 2010 (UTC)

(deindent) I agree that Carl's argument is superficially convincing. But I disagree with the points he is making very strongly. Carl's preferred text is too vague, it doesn't make the construction clear. It shares this property with the most popular treatments of Godel's theorem, but this vagueness causes serious problems.

The construction in the proof should be made clear. Every proof constructs something or other, and the proof of Godel's theorem is no different. What is Godel's proof constructing? Most people say its a complicated sentence. That's true. But it's a complicated sentence of the form "This computer program does not halt". Most of the difficulty is constructing the program, not the sentence.

Giving the construction explcitly not only makes it easier to present this proof, but it clarifies related proofs as well. For example, the construction in the previous sentence works for the Godel-Rosser theorem. If you look through the archives, there's also the Godel proof length theorem, which is considered an advanced result (although only the simplest versions are presented).Likebox (talk) 00:10, 4 February 2010 (UTC)

The construction in the article is perfectly explicit: "We obtain p by letting F be the negation of Bew(x); thus p roughly states that its own Gödel number is the Gödel number of an unprovable formula." It's not obvious how the construction could be more explicit than "apply the diagonal lemma to the negation of Bew". — Carl (CBM · talk) 02:16, 4 February 2010 (UTC)

But "Bew" is the worst kind of jargon, outdated 1930s German jargon. If you replace "Bew" with the English synonym "provable in S", the sentence becomes:

we obtain p by letting F be the negation of x is provable in S

Or,

F says "x is not provable in S"

Of course, this proves nothing by itself. You need to say what "x" is, and how F talks about provability. The way you do this is to say:

F says the program that deduces all consequences of S will not find x"

And then you make sure that x ends up refering to the whole sentence in the tricky Godelian way which is very unilluminating, and completely equivalent to the construction I gave above. I want to point out that this is only a very small part of the construction: the main problems--- showing that "provable" is a statement of arithmetic, and showing that the self-reference can be achieved, are not part of this gloss. The wording I gave explicitly shows you how both points work.Likebox (talk) 02:26, 4 February 2010 (UTC)

Bew(x) is not a synonym for "x is provable". The former is a formalized statement that can be true or false relative to a particular model. The latter is a meta-level statement that is either true or false, period. If you prefer to call "Bew" by the name "Pvbl", that makes little difference in the proof. (Also, if current books use the term "Bew" then by definition it is not outdated.)

Similarly, the thing being searched for in your program is not "R does not halt", which is a meta-level statement. Your program is searching for proof of $\lnot \exists nT(R,0,n)$. This is not, in general, the same as "R does not halt". Your text does not explain how T is obtained. — Carl (CBM · talk) 03:13, 4 February 2010 (UTC)

This distinction is so tiny, I fail to see how anyone could get confused.Likebox (talk) 03:17, 4 February 2010 (UTC)

I would like to repeat your comment in English, so that people see how nitpicky it really is: "Bew x" says that "x is provable" as a statement in a theory. That does not mean that "x is provable", rather it is a statement in a formal theory that says "x is provable". So what? There is no chance for any confusion, and it is pointless to make distinctions that don't clarify anything.

The thing being searched for is not "R does not halt", but the formal statement "R does not halt" translated to the language of S. Yes that's true, but it's also obvious, and there is no chance of confusion. Again, these nitpicky pseudodistinctions don't do anyone any good.Likebox (talk) 02:41, 5 February 2010 (UTC)

"Bew(x)" is not a statement about provability, it is a statement about the existence of two numbers which satisfy certain properties. This distinction is crucial, because without it it would be possible to construct the sentence "I am not provable", which is impossible. The distinction between statements and numbers is very important and very confusing, because the numbers represent statement in Goedel numbering. In your proof, the code is just a number, and it represents a statement only in the programing language, and this distinction is, again, crucial. Dan Gluck (talk) 07:55, 5 February 2010 (UTC)

This distinction should be obvious, not confusing. You misidentified where it appears in the computational proof: it appears when you translate "R does not halt" to be a statement language of S, it does not appear in anything related to "code" or "programming language".

One of the superior aspects of presenting the proof using computer programs is that you cannot get confused on this point. Computer programs are just like integers, they are absolute notions, you don't need a specific axiom system to know what they mean, you just run them. The issue of language is unimportant--- any language is equivalent to any other by a simple process of translation.

On the other hand, some axiom systems will prove certain theorems, while other axiom systems will prove other theorems. So for axiom systems, you have to make the distiction between the theorem "T" as a statement about computations and the theorem "T" as a statement of S. S can prove T or disprove T, and T can be true or false as a statement about computations, and the two notions are different.

But this is where the proof I presented really makes things clear: the only place where you deal with an axiom system is when you are searching for a proof within S. You don't deal with the axiom system anywhere else, because everything is formulated in terms of computer programs. This is where a great deal of the clarity of the proof comes from.

To restate the distinction you and CBM are making: There is a difference between the statement "S says that program P halts", and the statement "program P halts". Yes, there is. This is why you say "GODEL looks for a proof in S of R does not halt". The fact that GODEL finds this proof in S does not make it true (and in fact, GODEL makes sure that if it finds it, it is false), it is just a statement in the language of S.

To summarize: if you stop thinking of the proof in the Godel style presentation, and think in terms of the computer program, you will never ever get confused on this point again.Likebox (talk) 10:05, 5 February 2010 (UTC)

The issue is mostly unrelated to provability in S. The issue is that "G halts" is not the same as "∃ n T(G,0,n)". The former is either true or false; the latter can be true in some models of S and false in other models of S. So there can be models of "∃ n T(G,0,n)" even if G does not halt. It's key to present this distinction relatively clearly for the concept of ω consistency to make sense. — Carl (CBM · talk) 12:26, 5 February 2010 (UTC)

You are not saying anything different than what I was saying above, except you are making it sound more mysterious. What you are saying is that "G halts" is different than "S proves that G halts" or that "S has a model where G halts" (i.e. S doesn't prove G doesn't halt). S can prove that G halts without G halting. S can not prove that G doesn't halt without G halting. This is abundantly clear if you use computational language, because the computational language is absolute. Only S and its model changes.

What a reader must keep in mind is that a consistent S can prove "G halts" when this is false, but it can't prove "G doesn't halt" when this is true. I put a section on this, and I agree that it is important for omega-consistency. But without computational language, I don't believe you can make the distinction clear.Likebox (talk) 13:31, 5 February 2010 (UTC)

The problem is that "S has a model where G halts" is mixing a meta-level concept ("halts") with object-level statements in models of S. Experts do mix these sometimes in papers when they know there will be no confusion, but in an elementary article such as this we should be slightly more careful. What can actually happen is that

S has a model in which ∃ n T(G,0,n)

even though G does not, in fact, halt. In that model, the set of standard numbers P for which ∃ n T(P,0,n) is not the same as the set of programs that actually halt. This is exactly the same as the difference between Bew(x) and "x is provable", and neither one is easier to explain than the other. — Carl (CBM · talk) 13:39, 5 February 2010 (UTC)

You might be right on this point. But I wanted to make sure that less experienced readers would see that they are equivalent statements.

The statement "S proves that G halts" doesn't mean S proves that G actually halts of course, it means S proves that in the representation of computation, there exists an integer number of steps such that G halts after those steps, just as you say above. This does not mean that G halts.

The way I like to say this with (I think) minimal confusion is as follows:

1. S can prove G halts even if its not true
2. S cannot (consistently) prove G doesn't halt if G halts.

I think this phrasing is better, but perhaps you can say "what G halts means in S is There exists an n such that T^n(blah blah)=0". I don't care.Likebox (talk) 13:51, 5 February 2010 (UTC)

I don't see how your "modern proof", if ammended with all the "blah blah" as it should be, is less confusing. And yet again, "R does not halt" should not appear anywhere. What you do have is R (which is the code of S) plus some characters, and this means only under some interpretation that S does not halt. This interpretation depends on the program language as well as other things. Instead of clarifying the distinction, your proof as it is written now only mixes both things and therefore makes the potential confusing worse. And if your proof is not confusing, hence I am mistaken in my claim here, this means that I have some confusion about this matter, which means that your proof is confusing. Therefore, our assumption that your proof is not confusing was wrong; This proves that your proof is confusing.Dan Gluck (talk) 22:48, 5 February 2010 (UTC)

(deindent) you are not confused about the modern proof exactly, you are confused because you can't understand what is the exact reason why the "modern proof" is so simple and the old proof is so convoluted, when they are logically equivalent. So what you are doing is translating every confusion you have about the old proof into an equivalent confusion about modern proof. If you do this, the number of confusions is conserved, and there is no gain. In this case, I agree both presentations are equally confusing.

But I am suggesting that a reader has no reason to follow the original reasoning at all. The main reason for confusion is that the notion of computation is not separated out. The clarity that the modern proof brings is to place the notion of computation first, assume this is understood, and then to carry out the construction by making a computer program. This is easier conceptually, because you don't have to muck around with these annoying distinctions.

The proof is: construct GODEL to:

1. Print its code into R
2. Deduce all consequences of S looking for "R does not halt"
3. if you find this theorem, halt.

Now what does "R does not halt" mean within S? It can't mean anything other than (T^n blah blah). There can be no confusion. The construction separates out the absolute part of the theorem, the computer program, from the S-dependent part, which is the sentence.

If you learn this proof first, then you will have no confusions in learning the standard presentations. Not so the other way around, as you can see.Likebox (talk) 01:43, 6 February 2010 (UTC)

New section on Proof via Self-refutation

This was added recently

Revised: Proof via Self-refutation

Carl Hewitt [“Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency” Coordination, Organizations, Institutions, and Norms in Agent Systems III Springer-Verlag. 2008] developed an alternative very simple proof of the incompleteness theorym that uses self-refutation. From the fixed point theorem discussed above, Gödel⇔¬Prov(⌈Gödel⌉). Consequently, Gödel⇒¬Prov(⌈Gödel⌉ and therefore, by soundness, Prov(⌈Gödel⌉)⇒Prov(⌈¬Prov(⌈Gödel⌉)⌉), which is self-refuting. Consequently, we have ¬Prov(⌈Gödel⌉) by the principle of self-refutation. On the other hand, from fixed point theorem, ¬Gödel⇒Prov(⌈Gödel⌉) and therefore, by soundness, Prov(⌈¬Gödel⌉)⇒Prov(⌈Prov(⌈Gödel⌉)⌉), which is equivalent to Prov(⌈¬Gödel⌉)⇒Prov(⌈Gödel⌉) and self-refuting. Consequently, we have ¬Prov(⌈¬Gödel⌉) by the principle of self-refutation. Thus incompleteness is proved because both ¬Prov(⌈Gödel⌉) and ¬Prov(⌈¬Gödel⌉) have been proved. Note that in this proof, unlike the Gödel-Rosser version, a consistency assumption is not required. The self-refutation proof works even for logics that are tolerant of inconsistency, e.g., paraconsistent logics. 209.131.62.144 (talk) 02:37, 6 February 2010 (UTC)

Why this is no good

1. It already assumes the G implies "G is not provable". The whole difficulty is carrying out this construction. Once you have this, the theorem follows.
2. It assumes soundness, which is not necessary. You only need soundness for calculating the answer of halting computations, and for omega-consistency in the non-Rosser version.

Otherwise it is a convoluted restatement of Godel's original proof. It piggy-backs on the same construction, and it does not clarify the reasoning, in my opinion. So I think it should be left out.Likebox (talk) 01:43, 6 February 2010 (UTC)

Why this is good

1. Gödel⇔¬Prov(⌈Gödel⌉) comes directly from the fixed point theorem
2. Soundness is an essential part of the self-refutation proof.

The self-refutation proof is quite different from Gödel's original proof.209.131.62.144 (talk) 02:57, 6 February 2010 (UTC)

How is it different? It's the exact same construction, and it glosses over this construction by saying "fixed point theorem". Well yes, it is the fixed point theorem, but that's all the interesting bit. The remaining parts are trivial logical deductions, which have been written here in an overly formal style. I'll let others comment, but it is wrong to claim that two proofs with the exact same construction are different proofs. This is why I disagree with those who have claimed that the proof using computer programs that I prefer is different from Godel's proof.Likebox (talk) 03:55, 6 February 2010 (UTC)

One important difference is that no consistency assumption is used in the self-refutation proof. Note that the self-refutation proof makes no appeal to the concept of "truth."

An important deficiency of the current article is that it does not clearly state Gödel⇔¬Prov(⌈Gödel⌉) from the fixed point theorem. I am sorry that you have trouble with the formal notation of mathematics, e.g., using ⇔.209.131.62.144 (talk) 04:32, 6 February 2010 (UTC)

I don't have trouble understanding your notation, I just find this type of over-formalism ridiculous. You aren't saying anything useful with your notation. The article already says that G iff G is not provable, it even repeats this in German.Likebox (talk) 04:50, 6 February 2010 (UTC)

Your claim that consistency is not assumed is also silly--- you are finding a self-refutation, which is the same as an inconsistency. You are assuming soundness, which is ten billion times stronger than consistency. Is it April 1?Likebox (talk) 04:52, 6 February 2010 (UTC)

Expressing Gödel⇔¬Prov(⌈Gödel⌉) formally has the advantage that it can be checked mechnaically.

Self-refutation is not the same as inconsistency. Also consistency is weaker than soundmess in proof theory, which is that if P⇒Q, then Prov(⌈P⌉)⇒Prov(⌈Q⌉).63.249.99.129 (talk) 21:42, 7 February 2010 (UTC)

I removed the section. 66.127.55.192 (talk) 05:33, 6 February 2010 (UTC)

I restored the section. 63.249.99.129 (talk) 21:42, 7 February 2010 (UTC)

I removed it again. The difference from the current proof is Hewitt weirdness, and it's not clear that the incompleteness theorem is actually correct in Hewitt's redefinition of logic. — Arthur Rubin (talk) 21:47, 7 February 2010 (UTC)

Out of curiosity, does anyone here actually get what Hewitt is talking about? I've looked at his talk-page arguments before (oh, I can't prove it was he, but it seemed pretty obvious) and I could never make sense of it. But I also couldn't definitively refute it, given that he has a very idiosyncratic use of terminology which he doesn't much explain, so I couldn't get a good enough handle on what he meant to be sure it was wrong. Now, in most cases, you just label that "not even wrong" and move on, but with someone of Hewitt's stature one is reluctant to do that lightly. --Trovatore (talk) 23:18, 7 February 2010 (UTC)

I remember looking at one of the references briefly ([3], which is listed in the article right now). It made enough sense to me after spending a little time with it. But it would require an enormous amount of space to explain in detail, which is why I think it's better to just link to it from our article. — Carl (CBM · talk) 23:35, 7 February 2010 (UTC)

I looked at the article and don't see any problem. What do you see as the problem with its statement of incompleteness?99.29.247.230 (talk) 22:12, 7 February 2010 (UTC)

CBM's formulation seems reasonable. However, it's not a form of "Gödel's incompleteness theorem", because Hewitt has redefined the logical terms. It may be a modification (not extension, without further effort, because Hewitt uses non-standard definitions of "proof" even in consistent logic), adn probably deserves a few words. — Arthur Rubin (talk) 23:05, 7 February 2010 (UTC)

Comments by CBM

Re 209.131.62.144: the current article does explicitly point out the diagonal lemma, in the section "Diagonalization".

In general: while it's interesting to think about what might happen in paraconsistent logics, it goes somewhat beyond the scope of this article to do more than just give a reference. Such a reference was in this article, and I don't know why it was removed. I have restored the reference and brief summary, which I think is reasonable to include. I do not think it is reasonable to include the "self-refutation" argument as it was earlier today. — Carl (CBM · talk) 22:45, 7 February 2010 (UTC)

While I agree with you about the content, I believe this gives an opportunity for clarifying when somebody has a new proof and when it's a rehash of an old proof.

To prove that zeta-3 is irrational, one gives a series of rational approximations which converge quickly to the value. If two different proofs give the same sequence of rationals, then it is in some sense correct to consider the two proofs equivalent. They construct equivalent objects.

On the other hand, Euler's proof of the infinitude of primes and Euclid's proof are very different, in that they imply different constructions for new primes not on any finite list, and they provide different upper bounds on the density.

It is traditional in mathematics to identify proofs with the same construction as equivalent. So that a bona-fide different proof of Godel's theorem is the "quick proof using Berry's paradox", because the construction is actually different. On the other hand, using some different logical formalism, or reworking the language of the proof (as I did), does not constitute a new proof, because there is no new construction.

Since there is no new construction in the Hewittish version, I cannot see how we can say that it is a different proof.Likebox (talk) 01:06, 8 February 2010 (UTC)

Whether or not it's a "different" proof, it's a proof of a different, unrelated theorem. The fact that the theorem uses many of the same words as this one doesn't make it the same theorem. — Arthur Rubin (talk) 09:04, 8 February 2010 (UTC)

I looked at the proof by self-refutation (above) and it looks like a proof of the standard incompleteness theorem:

From the fixed point theorem discussed in the article, Gödel⇔¬Prov(⌈Gödel⌉). Consequently, Gödel⇒¬Prov(⌈Gödel⌉ and therefore, by soundness, Prov(⌈Gödel⌉)⇒Prov(⌈¬Prov(⌈Gödel⌉)⌉), which is self-refuting. Consequently, we have ¬Prov(⌈Gödel⌉) by the principle of self-refutation. On the other hand, from fixed point theorem, ¬Gödel⇒Prov(⌈Gödel⌉) and therefore, by soundness, Prov(⌈¬Gödel⌉)⇒Prov(⌈Prov(⌈Gödel⌉)⌉), which is equivalent to Prov(⌈¬Gödel⌉)⇒Prov(⌈Gödel⌉) and self-refuting. Consequently, we have ¬Prov(⌈¬Gödel⌉) by the principle of self-refutation. Thus incompleteness is proved because both ¬Prov(⌈Gödel⌉) and ¬Prov(⌈¬Gödel⌉) have been proved.

The only question that I see is whether or not to accept the principle of self-refutation.98.210.236.129 (talk) 14:33, 8 February 2010 (UTC)

The issue is that the "principle of self refutation" (which is some sort of deduction rule in Hewitt's deductive system) is not a topic of ordinary first order logic. That is: can you point out any standard logic textbook that discusses this deduction rule? Or, more generally, any work not by Hewitt? References like that would be very useful for establishing some context in the discussion here. — Carl (CBM · talk) 14:45, 8 February 2010 (UTC)

Very good question! One good place to look for answers would be on the literature of Provability Logic98.210.236.129 (talk) 15:17, 8 February 2010 (UTC)

If you want to make a case why this material should be included, you are going to need to make the case by looking into the references yourself. We cannot include material in the article that uses terminology such as "principle of self refutation" here when that terminology is both undefined in our article and never used in the standard literature on the subject.

Indeed, in ordinary logic with the standard provability predicate Bew, PA can prove "Bew(G)→Bew(~Bew(G))" but this does not mean that PA proves "~Bew(G)". So the argument above must have been written in some other formal system that is not PA. A proof of Goedel's theorem that does not apply to the specific case of PA is not really a proof of "Goedel's theorem". — Carl (CBM · talk) 16:17, 8 February 2010 (UTC)

Correct Proof of Incompleteness via Self-refutation

Unfortunately, the above translation of the proof in Common sense for concurrency and inconsistency tolerance using Direct Logic^TM is incorrect. From the fixed point theorem discussed in the article, Prov(⌈Gödel⇔¬Prov(⌈Gödel⌉)⌉). Consequently, Gödel⊢¬Prov(⌈Gödel⌉) by the 2-way Deduction Theorem for Direct Logic and therefore, by soundness, Prov(⌈Gödel⌉)⊢Prov(⌈¬Prov(⌈Gödel⌉)⌉), which is self-refuting. Consequently, we have Prov(⌈¬Prov(⌈Gödel⌉)⌉) by the principle of Self-refutation. On the other hand, from the 2-way Deduction Theorem, ¬Gödel⊢Prov(⌈Gödel⌉) and therefore, by soundness, Prov(⌈¬Gödel⌉)⊢Prov(⌈Prov(⌈Gödel⌉)⌉), which is equivalent to Prov(⌈¬Gödel⌉)⊢Prov(⌈Gödel⌉). Consequently, we have Prov(⌈¬Prov(⌈¬Gödel⌉)⌉) by the principle of self-refutation. Thus incompleteness is self-proved because both ¬Prov(⌈Gödel⌉) and ¬Prov(⌈¬Gödel⌉) have been self-proved. Note that in this proof, unlike the Gödel-Rosser version, a consistency assumption is not required.

Direct Logic is the minimal fix to classical mathematical logic and statistical probability (fuzzy) inference that meets the requirements of large-scale Internet applications (including sense making for natural language) by addressing the following issues: inconsistency tolerance, contrapositive inference bug, and direct argumentation. Consequently, Direct Logic is different from previous classical logics like Peano Arithmetic and Provability logic. Note that the above proof is not valid in Peano Arithmetic because of the use of the principle of Self-Refutation. Also the above proof is not valid in Provability Logic because the standard translation of p⊢q as Prov(⌈p⇒q⌉) is not valid in Direct Logic. Indeed in Direct Logic, Prov(⌈p⇒q⌉) is equivalent to (p⊢q and ¬q⊢¬p) by the 2-way Deduction Theorem. Furthermore, because of the requirement of inconsistency tolerance, theories in Direct Logic not strictly speaking extensions of Peano Arithmetic and Provability logic.

The interesting thing is that Gödel's incompleteness result survives the transition to the brave new world of the Internet. Then it turned out that the result could be extended to become logically necessary inconsistency (which would horrify Gödel if he were still alive).70.231.251.220 (talk) 01:37, 10 February 2010 (UTC)

Paragraph on Direct Logic

I have trimmed back the text in the article some. We're talking here about work which is sufficiently related to Goedel's theorem for use to include a brief pointer, but not related enough to expound on in depth. In particular, we don't have space to try to define the various theories that Hewitt studies, so I personally think it's better to just say "certain theories" and leave it at that. Trying to say say something only half vague is much harder than saying something that is clearly not meant to be detailed. The only point of the text in the article, I feel, is to have a place to put the literature reference, not to really explain what's going on. — Carl (CBM · talk) 16:20, 8 February 2010 (UTC)

Discussed below are some problems with the current paragraph on Direct Logic:

Carl Hewitt (2008, 2009) has shown that Gödel's argument can be adapted to prove similar results within certain sufficiently strong paraconsistent theories. Theories in these logics are able to prove their own Gödel sentences are both provable and not provable, and the theories are thus inconsistent (although still paraconsistent).

These problems include the following

• It was not Gödel's argument that was adapted. The new proof based on self-refutation is fundamentally different from Gödel's proof because it uses different assumptions and a different logic (Direct Logic). The main thing is common is the use of the fixed point theorem to construct the Gödelian sentence. Gödel's informal proof is not valid in Direct Logic and the Direct Logic formal proof is not valid in the Model Theory used by Gödel.
• Direct Logic proves Incompletness of its theories, not "similar results."
• The theories proved Incomplete do not have to be "sufficiently strong." Roundtripping and Self-refutation are sufficient to prove every theory (even the empty theory) incomplete. Consequently, incompleteness is logically necessary because it does not depend on axioms for arithmetic, etc.
• Direct Argumentation is a much stronger property than paraconsistency (which is rather weak). Incompleteness follows from Self-refutation, which is a special case of Direct Argumentation. Paraconsistency is a very weak form of inconsistency tolerance that follows as a consequence of Direct Argumentation.

Consequently, a revised version of what was reverted will be restored since it does not have the above problems.70.231.251.220 (talk) 02:09, 10 February 2010 (UTC)

Computation and modal/paraconsistent logics

I spent a little bit of time wading through Hewitt's paper. When examining his claims regarding his peculiar paraconsistent "direct logic(TM)", it is essential to separate out the part of Godel's theorem which is about logic, and the part which is about computation.

Whatever your logic, there are statements which are absolute, namely the statements "X halts with result R after N steps" for all halting computations X. These theorems are verifiable by running X, and they are just plain true. In Hewitt's system these are the halting programs in lambda-calculus.

In addition to these absolute statements, there are statements of the form "X does not halt", which can be considered modal relative to any one fixed axiomatic system. So in some possible models, "X does not halt" is true, while in other models "X does not halt" is false. There are also higher order statements of the form "X running with Turing oracle halts/does not halt", the higher levels of the arithmetic heirarchy, which can be considered modal too.

The Godel sentence is of the form "GODEL does not halt" for a specific computer program GODEL. This construction can be interpreted modally, so that "GODEL does not halt" is true in some possible models, and false in others. But the incompleteness theorem, when made most general, is equivalent to the statement that there is no algorithm which can separate out all halting from non-halting programs. So if you have a logic, paraconsistent or not, if it runs on a computer, it can't discriminate between the non-halting and halting programs. This result is a computational result, and so absolute.Likebox (talk) 11:56, 9 February 2010 (UTC)

Found that Hilbert quote

While going through Hewitt, I found this quote I asked for a while ago from the preface to the Grundlagen:

This situation of the results that have been achieved thus far in proof theory at the same time points the direction for the further research with the end goal to establish as consistent all our usual methods of mathematics.

With respect to this goal, I would like to emphasize the following: the view, which temporarily arose and which maintained that certain recent results of Gödel show that my proof theory can't be carried out, has been shown to be erroneous. In fact that result shows only that one must exploit the finitary standpoint in a sharper way for the farther reaching consistency proofs --- David Hilbert (Hilbert/Bernays 1934)

This is a very important quote, because it sets the stage for Gentzen's consistency proof. The "sharper finitary standpoint" is to admit ever more complex methods of finitary deduction, Gentzen identified this as ordinal induction, so as to prove the consistency of ordinary mathematics. This quote is important to include, because Godel's theorem is often misinterpreted as saying that it is impossible to prove the consistency of complex set theories using only reasonable axioms on discrete combinatorial objects.

The heirarchical process of producing more complex axiom systems is criticized by Hewitt, who would prefer to expand an axiom system of limited complexity by including inconsistent statements.Likebox (talk) 11:56, 9 February 2010 (UTC)

Yes, it would be valuable to include the Hilbert quote and to discuss Gentzen's consistency proof. Also mention should be made of work by Feferman, et. al. to extend the consistency proof to analysis.

However, the paper that you quote did not criticize Gentzen's consistency proof. Instead it criticized the Taskian framework of stratified metatheories.70.231.251.220 (talk) 02:32, 10 February 2010 (UTC)

I don't know that long quotes by Hilbert should be included; Hilbert was too close in time to the incompleteness theorems, and too committed to his program, to really appreciate them in his speeches and writing. So what he says has to be interpreted in the light of history. But it would be a good idea to have something about Hilbert's views sourced to something contemporary. Hilbert's program is mentioned twice, but there is not currently a "history" section in which we could mention Hilbert's views directly.

The section "implications for consistency proofs" does have a paragraph on Gentzen's proof. I don't think there is room in this article to go into great detail about Gentzen's result; our articles should only be so long, and it's enough to try to talk about one difficult theorem, much less two. — Carl (CBM · talk) 02:43, 10 February 2010 (UTC)

The problem is that it is stated umpteen times in the literature that Hilbert was too thick to understand Godel's theorem, and that his response was uncomprehending. But this quote shows that he understood Godel's theorem fully, and was able to see how to extend the program in the way that it was later extended by Gentzen and others. This is important to note. I discussed the ramifications of this earlier in the archives, but at the least, this is the birth of ordinal analysis.

Not to be too hard on Hewitt, but he also states that Hilbert was too close to his own program and didn't appreciate Godel's theorem. That's absolute nonsense. He understood the theorem better than nearly anyone else.Likebox (talk) 02:55, 10 February 2010 (UTC)

To the extent that Hilbert thought that "the view, which temporarily arose and which maintained that certain recent results of Gödel show that my proof theory can't be carried out, has been shown to be erroneous", he was incorrect. Certainly the view was not "shown to be erroneous" given that it is now the majority viewpoint in mathematical logic. If anything, ordinal analysis only strengthened the argument that no finitistic system can produce a consistency proof for PA, because the ordinal of a finitistic system will be less than the ordinal of PA.

It isn't clear to me if this error is because Hilbert misunderstood Goedel's theorem, because he was just being polemic, or because Hilbert's own ideas about the his program were so vague that it was virtually unfalsifiable. But rather than trying to make that decision myself I would be happy to rely on some published analysis of the historical record. — Carl (CBM · talk) 03:02, 10 February 2010 (UTC)

(Edit collison)L The issue (confusion, morass) surrounding what Goedel's results did to Hilbert's "program" derives from what Hilbert meant in his specification by the use of the word "finitary". Hilbert was "upset" by Goedel's results, and he resisted them, but his age and his retirement plus the decimation of the German mathematical community by the Nazis put an end to his further efforts after the mid 1930's. Gentzen's proof is considered by some to be an unsuccessuful solution to Hilbert's second problem because of the issue (of the meaning of finitary); see more at Hilbert's second problem. I don't think this article is the place to discuss the issue of Hilbert's failed program, except in passing along a link to Hilbert's second problem and Gentzen's proof. Bill Wvbailey (talk) 03:14, 10 February 2010 (UTC)

(deindent) The problem with what you and CBM are saying is that it is belied by Hilbert's own goals and statements. Remember--- his goal was to prove the consistency of set theory by using combinatorial reasoning. He never said that this reasoning had to be restricted to PRA or PA (that was his followers). He never said what "finitary" meant exactly, except that it should not involve uncountable infinite sets or analysis.

The fact that modern authors conflate "finitary" with "provable in PA" is a sign of the degree to which Hilbert is misunderstood. PA + "PA is consistent" is just as finitary as PA for Hilbert. Likewise, ordinal induction is finitary, as long as the ordinals are computable. So Gentzen's proof and all that follows are finitary proofs.

People have often said "Hilbert was old" and "Hilbert was dumb", but in fact Hilbert was right.Likebox (talk) 03:36, 10 February 2010 (UTC)

Actually people generally identify "finitary" with PRA, not PA. It's true that Hilbert never precisely defined "finitary", which has the benefit of making any claims he made unfalsifiable. But we need to stick with the opinions that appear in the actual literature here, rather than trying to divine what Hilbert meant by looking at a few isolated quotes. — Carl (CBM · talk) 03:41, 10 February 2010 (UTC)

There's a reason that Hilbert did not define "finitary" as PRA, or as PA, unlike his followers. It's probably because he had intuition that it was too weak. Hilbert was extremely familiar with the power of ordinals, he was one of the people who advertized how useful Cantor's set theory was for combinatorial results like the nullstallensatz. So it seems unlikely to me that Hilbert was suckered in by the claim that "finitary=PRA". He certainly never says that.

Hilbert defined "finitary" as dealing with combinatorial objects, no infinite sets, no real numbers. In modern terms, it would be axioms about computations. This includes PA, but it also includes PA+"consisPA", PA+"consisPA"+consis(PA+consisPA) and any computable ordinal tower like this.

You are not mentioning that Gentzen was closely affiliated with Hilbert, and that Gentzen was satisfied that his method was finitary. It was only Godel that said "whatever this is, it isn't finitary", leading mathematicians to redefine "finitary" to mean less than PA.

I think that the word "finitary" when used by Hilbert should mean what he meant--- using obviously true axioms about computable objects. The only reason that he did not say it precisely is because computation had yet to be defined.Likebox (talk) 03:49, 10 February 2010 (UTC)

It is also folklore (I don't remember where I read this) that Hilbert and his school essentially had a version of the constructible universe "L" constructed in the 1930s, but would not use it to prove things because they refused to assume infinite set theory without proving its consistency first. Godel, who had no such compunctions, was able to prove things first.Likebox (talk) 03:53, 10 February 2010 (UTC)

The point of Hilbert's program was to reduce the consistency of infinitary mathematics to the consistency of a finitary system. It's fine if you think PA is a finitary system, but apparently the mathematical logic community doesn't, and our article needs to stick with the published literature.

Usually, when people speak of "finitary" systems, such systems never support full arithmetical induction. For example $\Pi _{5}^{0}$ induction is not finitary, because a $\Pi _{5}^{0}$ statement is inherently an infinitary statement. Gentzen's proof uses transfinite induction, but with a quantifier-free matrix. — Carl (CBM · talk) 04:01, 10 February 2010 (UTC)

This is mixing up the modern notion of "finitary" with the historical notion of "finitary". If someone provided a proof in PA that set theory was consistent, this would have been fantastic to Hilbert.

I agree that Gentzen does not need higher statements in the heirarchy, so this is a moot point to debate. The essential issue is not the quantifier number, but the largest ordinal you can prove is well founded. This was not clear in the old days, however, so the notion of "finitary" was left nebulous.Likebox (talk) 06:38, 10 February 2010 (UTC)

The statement of the theorem

It is not necessary to add "which are sufficiently powerful" to the lead, since the powerless systems are just as incapable of proving certain arithmetic theorems. The theorem was stated carefully so as to make the statement as short as possible, and still be correct.Likebox (talk) 12:24, 9 February 2010 (UTC)

It is perfectly possible for consistent, effective theories of arithmetic to prove their own Goedel sentences, if the theories do not prove enough other facts about the natural numbers. The phrase "certain truths" in the lede refers to the Goedel sentence of the theory. Therefore there is a need to assume the theory is strong enough. — Carl (CBM · talk) 13:50, 9 February 2010 (UTC)

Really the lede was pretty bad even in the state I left it in; it needs to be clarified quite a bit. — Carl (CBM · talk) 14:57, 9 February 2010 (UTC)

I agree; Likebox's modification leaves nonsense. A "bad" theory may "prove" that it proves all statements. The theory isn't inconsistent, just the definition of "proof" is wrong. — Arthur Rubin (talk) 15:17, 9 February 2010 (UTC)

I didn't say that a theory cannot prove it's Godel sentence, what I said was that "a consistent effective theory cannot prove certain truths about arithmetic". The point is that a weak theory might be able to prove it's own Godel sentence, but then it does not prove other "certain truths", because it it too weak. I didn't say "The theory cannot prove its own Godel sentence", what I said was the shortest way of summarizing the result which is correct for all theories.

To Arthur Rubin: A bad theory may prove that it proves all statements, but it will always fail to prove certain truths about arithmetic.Likebox (talk) 02:51, 10 February 2010 (UTC)

The phrase "certain truths" in the lede refers to the Goedel sentence of the theory. The reason I agree not to say "Goedel sentence" there is so that we don't have to define it in the lede. But the point of the theorems is not that there are some random things that are not provable, but that in particular the Goedel sentence is not provable. This is certainly the way that someone half-knowledgeable about the theorems will interpret the lede. The goal is not just brevity; the lede needs to be sufficiently clear, and clarity in general is more important than terseness. — Carl (CBM · talk) 02:52, 10 February 2010 (UTC)

I tried to clean it up. Please feel free to fix it some more if I broke something. 66.127.55.192 (talk) 02:49, 10 February 2010 (UTC)

Looks good. I removed the italics (they seem too patronizing) and rephrased one thing. I like to try to avoid using the word "arithmetic" to mean "natural numbers", at first, because this usage is not well known in the general readership and will probably cause confusion. I think the remaining use of "arithmetic" is clearer in context. I had thought about removing the first use earlier, but it's easier to do with the new phrasing. — Carl (CBM · talk) 02:56, 10 February 2010 (UTC)

I didn't notice you were also editing it, so I went and messed with it some more, and may have clobbered something you did. I'll stop for a while and leave it to you. 66.127.55.192 (talk) 03:05, 10 February 2010 (UTC)

I self-reverted back to your version. 66.127.55.192 (talk) 03:16, 10 February 2010 (UTC)

I thought the later version was OK, too. The deeper question is whether it's better to be vague in the lede (as the revision you reverted back to is), or better to state the theorem precisely, without really explaining it. Each of these has some advantage, and personally I am somewhat ambivalent. My main concern is for the lede to be very clear to readers of all levels (particularly for people who know just enough to be tempted to misread whatever is written, or confused if it seems to disagree with what they have read elsewhere). — Carl (CBM · talk) 03:23, 10 February 2010 (UTC)

I reverted back to your version because I thought the "precise" version was too technical. But the less precise version of the first incompleteness theorem has a significant shortcoming, which is that it allows for complete theories of arithmetic (like Presberger arithmetic), which while they cannot prove various facts about the natural numbers, they cannot state any of those facts. Similarly, it's uninteresting that Peano arithmetic can't prove (or state) various facts about natural numbers that use higher order quantifiers. We want to express that the incompleteness theorem establishes that the interesting arithmetic systems contain statements that they can state but cannot prove. Can you try to patch that? You can probably do it better than I can. 66.127.55.192 (talk) 03:32, 10 February 2010 (UTC)

(←) What about something like this:

Goedel's theorems apply to theories whose syntax is capable of expressing arithmetical statements about the natural numbers. The theories must also be effectively generated, which means in essence that there is a computer program that enumerates the theorems of the theory. The first incompleteness theorem states that for any such theory, there will be true statements about the natural numbers that can be expressed in the theory but which cannot be proven within the theory. The second incompleteness theorem shows that if such a theory is capable of proving certain basic facts about the natural numbers, then one particular arithmetic truth that the theory cannot prove is an expression of the consistency of the theory itself.

I am sure that can be improved, so I will just put it here for now. — Carl (CBM · talk) 03:53, 10 February 2010 (UTC)

I guess I'm not comfortable enough with logic terminology to tell whether the above statement is precisely correct. If a theory means a set of theorems per the theory (mathematical logic) article, then by definition every sentence that an effectively generated theory contains is provable. So I used the term "system" (above, not in the article) to include all the sentences in the language, but I don't know if that's standard terminology. I'm not sure what "syntax" is supposed to mean either (e.g. in Curry-style typed lambda calculus, the only syntactically valid terms are the ones corresponding to provable statements, so syntax-checking in those systems can be undecidable). I think it's ok to stay short and vague, so maybe the current lede is ok as-is. It's not actually wrong; it's just weaker than we'd like it to be. But there should be a way to strengthen it while keeping it short and understandable. 66.127.55.192 (talk) 04:24, 10 February 2010 (UTC)

I see what you mean. This is another symptom of trying to be terse. You're right that the theory itself is a set of sentences. Really the paragraph is saying that there's a formula in the same signature as the theory but which is not a logical consequence of the theory. I don't really like the word "system", though. If it's a synonym for "theory", then it's no improvement. If it isn't meant to be a synonym for "theory", I think many readers will still think that it is.

Is this better?

Goedel's theorems apply to theories written in formal languages that are capable of expressing arithmetical statements about the natural numbers. The theories must also be effectively generated, which means in essence that there is a computer program that enumerates the theorems of the theory. The first incompleteness theorem states that, for any such theory, there will be true statements about the natural numbers that can be expressed in the language of the theory but which cannot be proven within the theory. The second incompleteness theorem shows that if such a theory is capable of proving certain basic facts about the natural numbers, then one particular example of an arithmetic truth that the theory cannot prove is an expression of the consistency of the theory itself.

— Carl (CBM · talk) 11:21, 10 February 2010 (UTC)

I think that needs a little more tweaking, because 1) the first incompleteness theorem applies to all effectively generated theories (those theories that can't express arithmetic statements also can't prove them); 2) "expressing arithmetical statements" may have to be expanded a little, to rule out decidable fragments like Presburger arithmetic. I'm still trying to think of a way to fix the current description without expanding it too much. 66.127.55.192 (talk) 18:34, 10 February 2010 (UTC)

I don't like the idea of trying to include effectively generated theories that can't even express arithmetical statements (such as real closed fields). If you ask 10 logicians whether Goedel's incompleteness theorems apply to the theory of real closed fields, my guess is they would all say, "no, it can't, because that theory is complete" or "no, because you can't interpret arithmetic in that theory". We don't want to try to simplify the lede to the point where it starts to contradict the way that people usually think about the theorem. The ordinary viewpoint (e.g. Smorynski's article) is that the incompleteness theorem only applies to theories that can interpret some reasonable fragment of arithmetic (e.g. PRA, PA, ZF). — Carl (CBM · talk) 19:10, 10 February 2010 (UTC)

OK. Your judgement is better than mine about how much precision is needed. 66.127.55.192 (talk) 20:15, 10 February 2010 (UTC)

Paraconsistency

I shortened the paraconsistency stuff and moved it to the section about "other fields" (in this case, the other field is computer science). The incompleteness theorems are nonobvious and celebrated results about classical logic, and the article is about classical logic basically through and through, and it's reasonable to treat anything else as just marginally related. Incompleteness can hold in nonclassical logic (intuitionistic logic, say) without that fact being nearly as interesting as the classical case. Putting the paraconsistency stuff in the "extensions of Gödel's result" section made it way too prominent in my opinion. That section basically came across like "Gödel proved the incompleteness theorems in 1931, then Rosser removed the requirement of ω-consistency in 1936, then nothing happened until 2008 when Hewitt came along and introduced Direct Logic^TM (a logic based on XML, imagine that) so once again, there was progress in the field".

I defer to CBM on the issue of whether the paraconsistency stuff should be mentioned in this article at all, so I kept it in based on earlier discussion, even though it's already linked from the paraconsistency article which I think is more reasonable than having it here. My own approach would be to remove it from this article completely, since a Google Scholar search shows almost no non-self citations to it. I'd want to see some citations from standard logic literature before including it at all. Also I'd ask Prof. Hewitt to please stop editing the article on COI grounds and because of his ban. CBM or others can make any necessary changes regarding those papers. What I did isn't ideal and maybe some adjustment can be made, but it was just awful before. 66.127.55.192 (talk) 06:40, 10 February 2010 (UTC)

Incompletenesss in Logic for the Internet Age

Does Incompleteness hold in logical theories for the Internet Age?

A modern task was to develop logic for the Internet Age. (Note that this was a different task than the one that began with Euclid, et. al., to formalize mathematical truths beginning with geometrical truths.) Logic for the Internet Age absolutely demanded inconsistency tolerance. Also, it was extremely helpful to preserve as much of traditional logical reasoning as possible because humans are integral to the operation of the Internet.

Direct Logic was developed as a logic for the Internet Age. And in Direct Logic every theory is Incomplete (see proof above). So the news was that Incompleteness has survived the trasition to the Internet Age.171.66.107.218 (talk) 00:42, 11 February 2010 (UTC)

That's great, but it's not appropriate for this article. Even if "Logic for the Internet Age" was an appropriate topic for this article, which it isn't, the tone is completely inappropriate for a Wikipedia article. — Carl (CBM · talk) 00:38, 11 February 2010 (UTC)

Well, this is what happened to Incompleteness in logic for an important branch of Computer Science. So how should it be phrased and where should it go?171.66.107.218 (talk) 00:46, 11 February 2010 (UTC)

Is it mentioned in any works that are not by Carl Hewitt and/or his students? If the answer is "no", then there is no reason to think that it belongs on Wikipedia. It can be published in research journals, of course; Wikipedia is not the only forum for publishing logic research. — Carl (CBM · talk) 00:48, 11 February 2010 (UTC)

It is not clear how much published work follows on this published work. However, since it is published, should it not be reported in Wikipedia? The work is quite well known at Berkeley, CMU, Edinburgh, MIT, and Stanford. Also, there is commentary in academic blogs.171.66.107.218 (talk) 01:00, 11 February 2010 (UTC)

If you have not noticed, I have been speaking in favor of referencing Hewitt's work, but in a brief way that fits within the purposes of our article here. Please read my request immediately below. — Carl (CBM · talk) 01:06, 11 February 2010 (UTC)

Request to Dr. Hewitt and/or his students: in the Late Unpleasantness, there was an arbitration case that I would like us to move past. I think that it's worthwhile, in this particular instance, to include a very brief pointer to Hewitt's published work, because my subjective opinion is that this is sufficiently related to the topic of this article. I have defended the inclusion of this material before and even restored it when it was removed.

However, polemical edits such as [4] are clearly not written in a style appropriate for Wikipedia, nor even for the professional journals I publish in. In the spirit of cooperation, can we avoid that sort of thing and focus on content that has a chance of remaining in the article? I think I'm one of the more accommodating editors here, but edits like that make it harder for me to argue that the content should be included. — Carl (CBM · talk) 00:57, 11 February 2010 (UTC)

It looks like the policy of "reversion first, talk later" has resulted in unfortunate escalation. However, there is considerable force to the argument that began "Incompleteness in Logic for the Internet Age."171.66.107.218 (talk) 01:09, 11 February 2010 (UTC)

This diff [5] shows the text that I added on this topic in 2008. I'm not completely tied to that text, but it has about the level of terseness that I think is desirable and the tone is very neutral. We should be able to achieve those two things in rewrites. — Carl (CBM · talk) 01:23, 11 February 2010 (UTC)

The title of the article to which this talk-page is attached is ''Gōdel's'' incompleteness theorens. The key operative word is Gōdel. G. ō. d. e. l. Not Hewitt. Not Gentzen. Not anyone else. Just Gōdel. If someone wants to contribute to a new article entitled Contemporary incompleteness theorems that would be wonderful. I fail to see how the above blather is contributing to the development of this article. Bill Wvbailey (talk) 02:04, 11 February 2010 (UTC)

Someone took the hink and created the article.99.29.247.230 (talk) 23:09, 14 February 2010 (UTC)

Bill, don't stuff beans up your nose. ;-) FWIW, I'm fine with CBM's wording, though my version was also intended to be terse and neutral, and also briefly explain the motivation of Prof. Hewitt's work. 66.127.55.192 (talk) 02:23, 11 February 2010 (UTC)

Sigh. I have redirected Contemporary incompleteness theorems to this article and removed the xref that had been placed into this article. There is further crap going on at Actor model and its talk page. I will start pulling together diffs for an ANI or arb enforcement thread tomorrow. 66.127.55.192 (talk) 08:16, 15 February 2010 (UTC)

See suggestion by Bill Baley above.98.210.236.39 (talk) 12:18, 15 February 2010 (UTC)

With all respect to Bill, I don't think that splitting things off into another article is a good idea. I'm starting to wonder if it would be simpler to request that the articles be semiprotected, so that we can discuss things more calmly on the corresponding talk pages. — Carl (CBM · talk) 13:01, 15 February 2010 (UTC)

Relative to a split: (i) This article is running the risk of being like the work of a student who's got too big a topic. Carl as you mentioned above there's no history section, and that is probably necessary if this article is to improve to GA status. I've been mulling what such an addition might look like, but after consulting Martin Davis's excellent Engines of Logic I don't see any way to do it succinctly. (ii) As you noted above in dialog with Likebox, Goedel invoked the restricted induction axiom of PRA (and full mu-recursion not known at the time). Does this matter? Given the fact that by the 1960's Goedel twice disavowed the use of lambda-calculus and recursion (of any form) in favor of a mechanistic, Turing-like methodology (although he never presented one) . . . are there now such proofs? If so what are they like? For example, in his explanation (cf pages 118-120 in the paperback edition) Davis invokes undecidability first, then moves on to consistency, which is certainty different than what happened historically. (iii) Even Goedel modified his presentation in his Princeton lectures, and his worry about (what turned out to be primitive) recursion was justified; he presented his and Herbrand's possible "full" recursion in those same lectures. What has happened after 1938? I'm kind of excited to see someone working on an extension article; I'm going to find it valuable and interesting. Bill Wvbailey (talk) 16:07, 15 February 2010 (UTC)

I can work on a history section over time. I'm not sure exactly which proof you're asking about in "are there now such proofs?" but if you can expand the question I will let you know if I know a proof.

Re history: if you propose a skeleton/outline I could fill in some details. I've got a lot of the contemporary bios. One historical item I find fascinating is Finsler and his failed proof. A few years ago I found Dawson's volumes of Goedel's works and cc'd Goedel's response re Finsler . . ..

Re a fully mechanized version of a proof of incompleteness: I was thinking along the lines of a proof that invokes only a "system" consisting of a raw Turing machine and appropriate "programs"; "it" (just the machine + programs itself, I guess . . .) first proves that "itself" is an adequate foundation for PRA (and better yet all of arithmetic), and then demostrates that it and any unrestricted "extensions" of it is incomplete. In other words, there are "propositions" U and ~U neither one of which can be proven by "it", but we onlookers know that one or the other is "true" from external evidence. Can "it" itself even propose these sorts of undecidable propositions? Or does undecidability "lock out" the machinery from even proposing these propositions? I'm assuming "it" can create the symbol strings that represent U and/or ~U. But what happens next? As I recall, Turing's first proof caused his machinery to lock up in an endless regressive "circle" and thus never progress further; it had been creating a sequence of diagonal numbers to test but fails when it arrives at its own number. Are U and/or ~U always related to the machine's own "number?" Are Turing's original proofs sufficient to prove the incompleteness theorems? Am I hopelessly confused?

The issue with "contemporary extensions" is that the real extensions of the result are more about finding the most general hypotheses on a theory that cause it to be vulnerable to the incompleteness phenomenon, studying formalizations of the incompleteness theorem, and studying the relationship between the incompleteness theorem and computability (e.g. recursively inseparable sets). However, these things quickly go beyond the scope of this article, and probably beyond the scope of Wikipedia. They are covered in detail in references like Smorynski's paper in the Handbook of mathematical logic and Smullyan's books.

The extension to paraconsistent theories is interesting as a side note, but it isn't really a "contemporary extension" since it isn't really an "extension". It's just a similar theorem that can be proved in certain paraconsistent logics. Really I'm not surprised it can be proven in that context, because similar systems to the one Hewitt studies are already known to be inconsistent by the Kleene–Rosser paradox, and the proof by Hewitt is qualitatively similar. — Carl (CBM · talk) 16:40, 15 February 2010 (UTC)

It's the Gödelian proposition that leads to inconsistency not the Kleene-Rosser proposition. 69.110.144.119 (talk) 18:59, 15 February 2010 (UTC)

Yes, of course it is. The similarity is that the systems involved allow for a more direct sort of self-reference than can be achieved in first-order logic. In the case of the Kleene-Rosser paradox, it causes the system to be inconsistent, because it's possible to write a sentence that says "I am false". In the case of Hewitt's systems, a similar sort of thing seems to be achieved using reflection principles for the provability predicate. They aren't the same, but the Kleene-Rosser paradox shows that if one adds too many reflection principles, the system will certainly become inconsistent. — Carl (CBM · talk) 19:29, 15 February 2010 (UTC)

The Gödelian proposition just barely squeaks by to inconsistency. The others (Liar, Russell, Currty, Kleen-Rossser) are blocked in Direct Logic. So there is something special about the Gödelian proposition; it's not just self-reference in general.69.110.144.119 (talk) 19:48, 15 February 2010 (UTC)

On this I have to defer to your knowledge and experience. As regards an "extension article" to this one, maybe the one these folks have created needs a name change. Maybe it shouldn't be considered "an extension" to this article, but rather as a member of a "family" of loosely-related articles. BillWvbailey (talk) 18:42, 15 February 2010 (UTC)

Responding to your question above: the difficulty with using one system is that you have to separate the object theory from the metatheory. It's possible to use PRA as both the object theory and metatheory, in order to formalize the incompleteness theorems, but then one has to add a consistency assumption Con(PRA) in the metatheory but not in the object theory in order to show that the Goedel sentence is true but unprovable. With no metatheory, it doesn't really make sense to talk about unprovability of a Goedel sentence in an object theory. — Carl (CBM · talk) 19:33, 15 February 2010 (UTC)

ANI thread

I have opened an ANI thread:

Wikipedia:Administrators'_noticeboard/Incidents#Carl_Hewitt

66.127.55.192 (talk) 19:08, 15 February 2010 (UTC)

Article has been semiprotected

The article has been semiprotected (again) for 2 weeks, this time by User:Abecedare. This means that the article can only be edited by logged-in editors. The need for semiprotection is unfortunate, and I apologize to 69.228.170.24 because this locks him out as well. However, it's simply unsustainable to have numerous IP addresses adding content about Hewitt's work to the article and reverting it when it's removed. Apart from references by Hewitt, I know of no references that mention "direct logic" at all, much less references that connect it to the incompleteness theorems. — Carl (CBM · talk) 03:54, 30 April 2010 (UTC)

It's ok, the semi-protection is the right thing. If I have something to contribute I'll put it here on the talk page. 69.228.170.24 (talk) 04:17, 30 April 2010 (UTC)

Seems to be missing computer science POV. But references are needed and Hewitt leads the pack in pubishing. This brings out the Hewitt haters to delete the edits. Stuckness results.

archive request

Can someone create a new archive page? I want to archive all the paraconsistency stuff, so that material on this page legitimately related to article development isn't spread all over by the interspersed cruft. Thanks. 69.228.170.24 (talk) 21:17, 1 May 2010 (UTC)

Actually I propose a special talk page just for paraconsistency, sort of like we now have /Arguments. That is: Talk:Gödel's incompleteness theorems/Paraconsistency, since it's a recurring topic. If it is created, I will refactor this current page to move the paraconsistency stuff to the new one. 69.228.170.24 (talk) 21:21, 1 May 2010 (UTC)

I'm not thrilled about making a new page for this topic. That sounds like an encouragement to continue. Maybe move the paraconsistency stuff to the existing /Arguments page. --Trovatore (talk) 22:34, 1 May 2010 (UTC)

I will make a new archive page. But the main reason this page is so long is the "history" sections. I didn't archive those yet because I was hoping we could move forward on actually putting a short history section in the article soon. Actually, I should be able to work on that this evening. — Carl (CBM · talk) 00:04, 2 May 2010 (UTC)

The history notes should not be archived yet. I asked for a new archive page mainly to move the paraconsistency stuff away from cluttering up the history notes. 69.228.170.24 (talk) 02:26, 2 May 2010 (UTC)

Thanks for creating archive 8. I moved the paraconsistency stuff (and a few other no longer active discussions) there to get them out of the way on this page. 69.228.170.24 (talk) 02:33, 2 May 2010 (UTC)

SPI

Since the socks haven't gone away I have filed a sock report at Wikipedia:Sockpuppet_investigations/CarlHewitt. 69.228.170.24 (talk) 05:23, 3 May 2010 (UTC)

Are you just talking about the talk page? I'm not sure that's really worth the bother. Trying to block all the IP addresses is going to be a game of whack-a-mole that will just amuse the puppetmaster. No doubt a block is justified, as far as that goes, so if you're willing to put the effort in, I won't stand in your way. --Trovatore (talk) 06:11, 3 May 2010 (UTC)

Please look at the contrib history of the different IP's in the SPI report. They have been trying to insert Hewitt's POV into a bunch of different computer science articles, and some of them have been active for long enough that blocks would probably help. Maybe I should try to spell that out in the report tomorrow. I'm too sleepy right now to deal with it. 69.228.170.24 (talk) 07:42, 3 May 2010 (UTC)

Ah, sorry, I hadn't realized that. My watchlist doesn't have a large sample of CS articles. --Trovatore (talk) 20:45, 3 May 2010 (UTC)

I have added some diffs instead of sleeping. Bah. 69.228.170.24 (talk) 08:44, 3 May 2010 (UTC)

Folks at Stanford, Cal, Google, UCSC, etc.

Folks at Stanford must be laughing off their chairs. Also, why is the guy from Oakland so bitter?64.9.238.118 (talk) 01:59, 6 May 2010 (UTC)

The root cause is a long-running rivalry between Cal and Stanford. —Preceding unsigned comment added by 68.65.169.145 (talk) 01:44, 7 May 2010 (UTC)

I don't understand either of those comments. — Arthur Rubin (talk) 03:54, 7 May 2010 (UTC)

Cal is UC California Berkeley, a legendary rival of Stanford. This is the reason for the snide comments of anon in Oakland.63.112.0.74 (talk) 20:04, 8 May 2010 (UTC)

The students have been breath of fresh air in improving the articles. Maybe Wikipedia should figure out how to make peace with them ;-) 67.169.144.115 (talk) 00:47, 9 May 2010 (UTC)

When it's clear that something should be mentioned (as with the literature on paraconsistency), there's no problem in adding an appropriate amount of material about it to the article.

My advice to the students is to know your audience. Several editors involved on this talk page have professional degrees in mathematical logic and are completely familiar with the incompleteness theorems. So students should avoid using words like "roundtripping", which I doubt any logic publication has every used; that just makes student appear naive about the incompleteness theorems. Moreover, students should argue their points from the well-known literature on the incompleteness theorems whenever possible. If some topic cannot be found in that literature, it may be of interest as a side note in the article, but it's unlikely to warrant more than a brief mention. — Carl (CBM · talk) 01:12, 9 May 2010 (UTC)

I ask again of the anons: What does paraconsistency have to do with Gödel's incompleteness theorems? What do Cal and Stanford have to do with Hewitt and Wittgenstein vs. Gödel, mainstream mathematical logic, and Wikipedia? (Well, Wittgenstein had nothing to say about Wikipedia).

And the "students" have provided some interesting notes, but very few suitable for any Wikipedia articles other than those of Hewitt and his inventions. Perhaps we should use a filter to block all mainspace edits from those "students". I think a range block might be too severe. — Arthur Rubin (talk) 01:27, 9 May 2010 (UTC)

The relationship is not so much about Gödel's theorem in first-order logic; the relationship goes through the Gödel sentence, which can be written down equally well for a sufficiently strong effective paraconsistent theory of arithmetic. So it's natural to ask whether such theories are also unable to prove their Gödel sentences. This is of more interest to philosophy, particularly because there is a natural language (disquotational) aspect to the argument that the Gödel sentence of PA is true, and paraconsistency is one of the possible ways to handle the inconsistency of natural language. So they can look at the English sentence "This sentence is not provable", which is provable (by contradiction) in naive English reasoning. Of course this is not really relevant to mathematical logic, but it does appear as a theme in the published literature (for example, see the Stanford Encyclopedia article on paraconsistency). The key thing that has to be kept separate, which I think you are pointing out, is that this is not about the incompleteness theorem itself, which is not about paraconsistent logic. It's about research that is motivated by philosophical examination of the incompleteness theorems.

The Cal/Stanford thing was an in-joke. — Carl (CBM · talk) 01:58, 9 May 2010 (UTC)

Explanations and proofs at the seminar (from the paper Common sense for concurrency and inconsistency tolerance using Direct Logic(TM) and the Actor Model) seemed clear enough. Feferman participated. A video will be posted on the Web.

ANI

I opened an ANI thread, WP:Administrators'_noticeboard/Incidents#Proposed_community_ban_for_Carl_Hewitt.

69.228.170.24 (talk) 22:13, 8 May 2010 (UTC)

Conversation is now at Wikipedia:Administrators'_noticeboard#Proposed_community_ban_for_Carl_Hewitt — Carl (CBM · talk) 02:47, 10 May 2010 (UTC)

Trashing students may not be the best move. The number of contributors is dropping! 67.180.133.247 (talk) 21:44, 9 May 2010 (UTC) 67.180.133.247 (talk) 21:44, 9 May 2010 (UTC)

---

I don't want to let my silence be construed as assent: I'm with agent '69 on this, and I agree with Arthur Rubin above. BTW I know about the feral cats in the tunnels and the bats in UGLY, etc [in-joke: if you don't get it, ask around]. This talk page is about Goedel's incompleteness theorems. BillWvbailey (talk)

Inconsistency tolerant logic

The following discussion on inconsistency tolerant logic comes from the the archives in the hope that by bringing it back into the foreground, the same arguments won't be repeated.63.249.108.250 (talk) 17:19, 3 June 2010 (UTC)

Correct Proof of Incompleteness via Self-refutation

Unfortunately, the above translation of the proof in Common sense for concurrency and inconsistency tolerance using Direct Logic^TM is incorrect. From the fixed point theorem discussed in the article, Prov(⌈Gödel⇔¬Prov(⌈Gödel⌉)⌉). Consequently, Gödel⊢¬Prov(⌈Gödel⌉) by the 2-way Deduction Theorem for Direct Logic and therefore, by soundness, Prov(⌈Gödel⌉)⊢Prov(⌈¬Prov(⌈Gödel⌉)⌉), which is self-refuting. Consequently, we have Prov(⌈¬Prov(⌈Gödel⌉)⌉) by the principle of Self-refutation. On the other hand, from the 2-way Deduction Theorem, ¬Gödel⊢Prov(⌈Gödel⌉) and therefore, by soundness, Prov(⌈¬Gödel⌉)⊢Prov(⌈Prov(⌈Gödel⌉)⌉), which is equivalent to Prov(⌈¬Gödel⌉)⊢Prov(⌈Gödel⌉). Consequently, we have Prov(⌈¬Prov(⌈¬Gödel⌉)⌉) by the principle of self-refutation. Thus incompleteness is self-proved because both ¬Prov(⌈Gödel⌉) and ¬Prov(⌈¬Gödel⌉) have been self-proved. Note that in this proof, unlike the Gödel-Rosser version, a consistency assumption is not required.

Direct Logic is the minimal fix to classical mathematical logic and statistical probability (fuzzy) inference that meets the requirements of large-scale Internet applications (including sense making for natural language) by addressing the following issues: inconsistency tolerance, contrapositive inference bug, and direct argumentation. Consequently, Direct Logic is different from previous classical logics like Peano Arithmetic and Provability logic. Note that the above proof is not valid in Peano Arithmetic because of the use of the principle of Self-Refutation. Also the above proof is not valid in Provability Logic because the standard translation of p⊢q as Prov(⌈p⇒q⌉) is not valid in Direct Logic. Indeed in Direct Logic, Prov(⌈p⇒q⌉) is equivalent to (p⊢q and ¬q⊢¬p) by the 2-way Deduction Theorem. Furthermore, because of the requirement of inconsistency tolerance, theories in Direct Logic not strictly speaking extensions of Peano Arithmetic and Provability logic.

The interesting thing is that Gödel's incompleteness result survives the transition to the brave new world of the Internet. Then it turned out that the result could be extended to become logically necessary inconsistency (which would horrify Gödel if he were still alive).70.231.251.220 (talk) 01:37, 10 February 2010 (UTC)

Paragraph on Direct Logic

I have trimmed back the text in the article some. We're talking here about work which is sufficiently related to Goedel's theorem for use to include a brief pointer, but not related enough to expound on in depth. In particular, we don't have space to try to define the various theories that Hewitt studies, so I personally think it's better to just say "certain theories" and leave it at that. Trying to say say something only half vague is much harder than saying something that is clearly not meant to be detailed. The only point of the text in the article, I feel, is to have a place to put the literature reference, not to really explain what's going on. — Carl (CBM · talk) 16:20, 8 February 2010 (UTC)

Discussed below are some problems with the current paragraph on Direct Logic:

Carl Hewitt (2008, 2009) has shown that Gödel's argument can be adapted to prove similar results within certain sufficiently strong paraconsistent theories. Theories in these logics are able to prove their own Gödel sentences are both provable and not provable, and the theories are thus inconsistent (although still paraconsistent).

These problems include the following

• It was not Gödel's argument that was adapted. The new proof based on self-refutation is fundamentally different from Gödel's proof because it uses different assumptions and a different logic (Direct Logic). The main thing is common is the use of the fixed point theorem to construct the Gödelian sentence. Gödel's informal proof is not valid in Direct Logic and the Direct Logic formal proof is not valid in the Model Theory used by Gödel.
• Direct Logic proves Incompletness of its theories, not "similar results."
• The theories proved Incomplete do not have to be "sufficiently strong." Roundtripping and Self-refutation are sufficient to prove every theory (even the empty theory) incomplete. Consequently, incompleteness is logically necessary because it does not depend on axioms for arithmetic, etc.
• Direct Argumentation is a much stronger property than paraconsistency (which is rather weak). Incompleteness follows from Self-refutation, which is a special case of Direct Argumentation. Paraconsistency is a very weak form of inconsistency tolerance that follows as a consequence of Direct Argumentation.

Consequently, a revised version of what was reverted will be restored since it does not have the above problems.70.231.251.220 (talk) 02:09, 10 February 2010 (UTC)

Computation and modal/paraconsistent logics

I spent a little bit of time wading through Hewitt's paper. When examining his claims regarding his peculiar paraconsistent "direct logic(TM)", it is essential to separate out the part of Godel's theorem which is about logic, and the part which is about computation.

Whatever your logic, there are statements which are absolute, namely the statements "X halts with result R after N steps" for all halting computations X. These theorems are verifiable by running X, and they are just plain true. In Hewitt's system these are the halting programs in lambda-calculus.

In addition to these absolute statements, there are statements of the form "X does not halt", which can be considered modal relative to any one fixed axiomatic system. So in some possible models, "X does not halt" is true, while in other models "X does not halt" is false. There are also higher order statements of the form "X running with Turing oracle halts/does not halt", the higher levels of the arithmetic heirarchy, which can be considered modal too.

The Godel sentence is of the form "GODEL does not halt" for a specific computer program GODEL. This construction can be interpreted modally, so that "GODEL does not halt" is true in some possible models, and false in others. But the incompleteness theorem, when made most general, is equivalent to the statement that there is no algorithm which can separate out all halting from non-halting programs. So if you have a logic, paraconsistent or not, if it runs on a computer, it can't discriminate between the non-halting and halting programs. This result is a computational result, and so absolute.Likebox (talk) 11:56, 9 February 2010 (UTC)

Edit disappeared (article misunderstood computer science)

My edit fixing a misunderstanding in computer science disappeared. The sentence on Professor Hewitt should be something like the following:

Carl Hewitt (2008) has proved that theories developed for inconsistent software engineering systems can prove their own Gödel sentences and are therefore inconsistent. —Preceding unsigned comment added by 171.66.50.25 (talk) 21:13, 2 June 2010 (UTC)

Misunderstanding? — Arthur Rubin (talk) 00:09, 3 June 2010 (UTC)

Maybe. But the students do have a point: previous wording was definitely wrong. 17.244.68.54 (talk) 00:25, 3 June 2010 (UTC)

"The students". Do we really have to keep playing at this coy word-game? If the previous wording was wrong, fine; just remove it. It's not important anyway. --Trovatore (talk) 00:26, 3 June 2010 (UTC)

Word games? What does this have to do with the disucssion of Wittgenstein? —Preceding unsigned comment added by 64.9.242.94 (talk) 03:43, 3 June 2010 (UTC)

What does Hewitt have to do with a discussion of Wittgenstein? — Arthur Rubin (talk) 08:15, 3 June 2010 (UTC)

According to Common sense for concurrency and inconsistency tolerance using Direct Logic^TM and the Actor Model,

"The controversy between Wittgenstein and Gödel can be summarized as follows:

• Gödel

1. Mathematics is based on objective truth
2. A theory is not allowed to reason about itself.
3. Roundtripping proves incompleteness but (hopefully) not inconsistency
4. Theories should be proved consistent

• Wittgenstein

1. Mathematics is based on communities of practice
2. Reasoning about theories is like reasoning about everything else, e.g., chess.
3. Proof of incompleteness leads to inconsistency
4. Theories should use inconsistency tolerant reasoning"

99.29.247.230 (talk) 16:19, 3 June 2010 (UTC)

That's complete nonsense. Goedel never said a theory isn't allowed to reason about itself. It so happens that the kind of self-reference that Hewitt wants to do just can't be done in our theories. But this is not an imposition from above; it's just something that the theory is not strong enough to do.

Wittgenstein was utterly incompetent as a mathematician and his thoughts on the matter are not important. --Trovatore (talk) 18:27, 3 June 2010 (UTC)

It's not complete nonsense; merely a controversy between Gödel and Wittgenstein. As Wittgenstein noted, provability of the incompleteness of Principia Mathematica (PM) in PM leads immediately to inconsistency of PM. Since inconsistency was unacceptable to Gödel, he needed a work-around. The restriction that he imposed was that a theory is not be allowed to directly speak of its own provability relationship. Classical logicians (Chruch, Rosser, Kleene, etc.) went along with this restriction because:

1. They wanted the incompleteness theorem to be provable.
2. A single inconsistency destroys classical logic.

Gödel was rather vague on the issue as to exactly what theory proves the incompleteness theorem. However, Wittgenstein was not willing to go along with this double talk. And he was one of the first to see through to the inconsistency. Hence the controversy.17.244.68.54 (talk) 20:36, 3 June 2010 (UTC)

That's total crap; that's not what happened at all. Goedel did not invent first-order logic. He just applied it. As a matter of cold hard fact, you cannot do the kind of self-reference Hewitt wants to do, in PM using first-order logic. --Trovatore (talk) 20:51, 3 June 2010 (UTC)

What Trovatore (above) is objecting to is that the following kind of proposition is allowed in Direct Logic:

P, (P⊢Q) ⊢ Q

However, it is not clear why the above propostion (which expresses chaining) is so objectionable.171.66.105.147 (talk) 01:02, 4 June 2010 (UTC)

Wrong; that is not what I am objecting to. I am not "objecting" to anything in Direct Logic at all. I have no particular interest in Direct Logic, and for the most part I simply ignore it.

What I am objecting to, at the moment, is your blatantly false characterization of the historical record. --Trovatore (talk) 01:05, 4 June 2010 (UTC)

Gödel absolutely objected to propositions like the one below because, as Wittgenstening noted, they mean that proving incompleteness immediately leads to inconsistency:

P, (P⊢Q) ⊢ Q —Preceding unsigned comment added by 171.66.105.147 (talk) 01:33, 4 June 2010 (UTC)

I am not sure just what sorts of things P and Q are supposed to range over (e.g. sentences or entire theories?) but in any case, whatever rule you have in mind that allows your conclusion, Goedel did not impose any "restriction" that excludes it. It was not part of the logic he was studying. The rule was not excluded; it was just never there in the first place. --Trovatore (talk) 01:39, 4 June 2010 (UTC)

P and Q are obviously propositions and chaining [P, (P⊢Q) ⊢ Q] is also a proposition. The whole point of meta-theories was to outlaw propositions like chaining.171.66.105.147 (talk) 01:52, 4 June 2010 (UTC)

More nonsense history. First-order logic was well-characterized by Hilbert before Goedel got to work. It does not include the above claim as a proposition (though it's fine, of course, as a rule, in Gentzen-style sequent calculus). --Trovatore (talk) 02:05, 4 June 2010 (UTC)

Yes, this is exactly Wittgenstein's objection: According to Gödel, there are fundamental logical propositions (e.g. chaining) that must not be expressed because if they are allowed to be expressed then incompleteness leads to inconsistency.171.66.105.147 (talk) 02:23, 4 June 2010 (UTC)

The natural formulations of first-order logic do not include rules as propositions; the linguistic machinery isn't strong enough. To allow them to be propositions requires extra work. They are not excluded; they were simply never included.

At this point I have reached the end of this discussion. This is not the right forum for it anyway. You (if you are who I'm assuming you are) are banned from this article by ArbCom and it is clear that the community is not going to permit your edits. The purpose of the talk page is to discuss changes to the article. Therefore this discussion is outside that scope. --Trovatore (talk) 02:32, 4 June 2010 (UTC)

Interesting case. For a long time Wittgenstein's views were bad-mouthed. Then when it turned out that they had merit, the response is outright censorship. It's no wornder that Wikipedia gets no respect in academia.17.244.68.54 (talk) 18:52, 4 June 2010 (UTC)

As Wittgenstein noted, incompleteness does not have much to do with arithmetic and induction. Incompleteness comes from making up certain kinds of propositions (e.g., This proposition is not provable in Principia Mathematica.). Later on, in discussions of the incompleteness theorem, Gödel retreated from Principia Mathematica to arithmetic with induction. Of course, first-order Peano Arithmetic is thoroughly unsatisfactory for characterizing the integers (see Models of arithmetic).

What can and cannot be proved in Principia Mathematica (PM) is more than a little mysterious. Gödel thought that round-tripping was a valid part of PM even though it did not appear in the Russell and Whitehead books. Russell introduced the Axiom of reducibility to create first-order equivalents for omega-order propositons of PM. So far there are no relative consistency proofs of the full PM to standard set theory.17.244.68.54 (talk) 23:02, 3 June 2010 (UTC)

I concede that I am no expert on PM and can't claim utter confidence that it's consistent. That doesn't justify your fantasy-historical claim that Goedel "imposed a restriction" on the theories or their logic to make things work. That claim has no merit whatsoever; the theories and logic were what they were, Goedel only showed what they could and could not do. --Trovatore (talk) 00:57, 4 June 2010 (UTC)

In terms of the historical recoord, there is no question that Gödel adhered to the restriction that a theory is not allowed to directly express its own provablity relation. Also there is no question that Gödel thought that mathematics is based on objective truth. At the same time, he needed to plausibly claim tha the incompleteness theorem had been proved. The issue is the relationship among these historical facts. Since he was a first-rate logician, the most plausible hypothesis is that he devised the only possible way out given the constraints of his philosophical beliefs.171.66.105.147 (talk) 01:25, 4 June 2010 (UTC)

Your claims above are absolutely false. Goedel did not adhere to any such restriction. --Trovatore (talk) 01:28, 4 June 2010 (UTC)

To user 171.66.105.147: If Goedel did not "allow" for a theory to express its own provability relation, then please explain what it is, exactly, that is going on in functions 43 - 46 of his paper "On formally undecidable propositions of Principia Mathematica and related systems". You can find them on page 55 of the 1992 Dover republication. --Taekwandean (talk) 10:41, 18 June 2010 (UTC)

According to Historical development of Incompleteness and Inconsistency:

Since Russell's theory (Russell) aimed to be the foundation of all of mathematics, a theorem to the effect that Russell is incomplete should be provable in itself. And as Wittgenstein noted, self-provable incompleteness of Russell would mean that Russell is inconsistent.

Because of inconsistency, Gödel insisted on the restriction that the theory Russell was not allowed to speak of its its own inference relationship ⊢_Russell. Instead, the theory Russell must be restricted to using the predicate Inference_Russell intuitively defined for a sentence s by Inference_Russell(s)⇔⊢_Russell⌊s⌋. However, Gödel prohibited the intuitive definition of Inference_Russell from being expressed in the theory Russell insisting that use of ⊢_Russell must be restricted to another theory called the "meta-theory" of Russell. Gödel completely ignored Wittgenstein's previous rejection of the restriction:

"There can’t in any fundamental sense be such a thing as meta-mathematics. . . . Thus, it isn’t enough to say that p is provable, what we must say is: provable according to a particular system." [Wittgenstein 1964, p. 180]

99.29.247.230 (talk) 21:35, 18 June 2010 (UTC)

Hewitt, quoting Wittgenstein misinterpreting Gödel. AGAIN. — Arthur Rubin (talk) 21:47, 18 June 2010 (UTC)

The above cited article goes on to say:

Gödel wrote as follows:

"He [Wittgenstein] has to take a position when he has no business to do so. For example, 'you can’t derive everything from a contradiction.' He should try to develop a system of logic in which that is true." [5 April 1972 letter to Carl Menger quoted in Wang 1997]

Gödel knew that it would be technically difficult to develop a useful system of inconsistency-tolerant logic in which “you can’t derive everything from a contradiction” and evidently doubted that it could be done. (In fact, It took over 40 years to develop such a system!) So there was a great deal at stake: classical logicians held that incompleteness was provable, but if Wittgenstein is correct then classical logic is finished because it cannot tolerate a single inconsistency. Consequently, classical logicians tried to defeat Wittgenstein by whatever means available, fair or foul.

Perhaps the last comment also applies to Arthur Rubin's criticism :-)

67.169.144.115 (talk) 00:29, 19 June 2010 (UTC)

I respectfully submit that this discussion of whatever the heck it is that Wittgenstein thought was wrong with incompleteness (or classical logic or metalanguages) has little to do with what it is that Goedel did or did not do in his proof. So, again, I'll ask what it is that the "Bew" relation is supposed to be if it is not the provability relation? Honestly, I think that this business about trying to "defeat Wittgenstein by whatever means necessary" is a bit over the top as well, however, our opinions about the motivations of classical logicians are also beside the point of this article. The real issue is whether or not Goedel used the provability relation in his proofs. I have suggested several places where he does. Do you have some evidence that the relation that I am looking at is not provability? --Taekwandean (talk) 10:34, 19 June 2010 (UTC)

Dear Taekwandean,

You seem to have missed the point of the above discussion. The relationship Inference_Russell discussed above is Gödel's Bew intuitively defined for a sentence s (which Gödel encoded as an integer) as Bew(s)⇔⊢_Russell⌊s⌋. However, Gödel disallowed use of the intuitive definition in Russell because, as Wittgenstein pointed out, allowing the intuitive definition into Russell would lead to inconsistency by means of the incompleteness proof. 67.169.144.115 (talk) 17:01, 19 June 2010 (UTC)

That almost makes sense. You're saying that Wittgenstein claimed that Gödel disallowed use of the Russell's intuitive definition because it would lead to inconsistency. And this is bad (on Gödel's part), why? There weren't any methods of dealing with paraconsistent theories then. (I would argue that there still aren't, but that may be my bias.) Still, what does this have to do with Gödel's incompleteness theorems?

As you can see by clicking on the link, the Wikipedia topic Incompleteness theorem is this article. And Wittgenstein's thesis is clearly relevant to the topic of the incompleteness theorem.

In historical terms, it seems that in his writings Gödel misunderstood Wittgenstein (perhaps deliberately). This misunderstanding was promoted by Gödel's contempt for Wittgenstein who opposed Gödel's deeply held belief that mathematics is based on objective truth. In this regard Wittgenstein agreed with von Neumann according the above cited article:

"From the very beginning, von Neumann strongly disagree with Gödel’s interpretation of incompleteness and had immediately concluded '... there is no rigorous justification for classical mathematics.' [letter of von Neumann to Gödel, November 29, 1930]"

67.169.144.115 (talk) 17:53, 19 June 2010 (UTC)

It's possible that all mathematicians misunderstand Wittgenstein. There's no reason to single out Gödel. There is no credible (not to say, even marginally, reliable) source who believes that Wittgenstein's beliefs are at all similar to von Neumann's, and few sources who believe that Wittgenstein had any idea what he was talking about. Further, if I recall von Neumann's letter correctly, he did not "disagree with Gödel’s interpretation of incompleteness"; and I think you'd find that Gödel agreed (after his work on incompleteness) that "... there is no rigorous justification for classical mathematics." Gödel had shown there was no rigorous justification. — Arthur Rubin (talk) 18:07, 19 June 2010 (UTC)

With their backs to the wall, it was the classical logicians who trashed Wittgenstein. In recent publications, his reputation has come back. See [Rodych 2003], etc.99.29.247.230 (talk) 15:19, 20 June 2010 (UTC)

Moreover, just to point it out again: Goedel did not "change" any properties of any logical system in response to his theorems. He studied classical logic as it stood; this is why he referred to Principia Mathematica as an example of a pre-existing system to which his work applied. Goedel demonstrated that this sort of logic (classical first-order logic) has various properties; his results can be recast as results of elementary number theory. So it's historically inaccurate to say things such as "Because of inconsistency, Gödel insisted on the restriction that the theory Russell ...". Goedel did not insist on anything; the properties of the system Russell were already fixed when Goedel began to study it. — Carl (CBM · talk) 21:13, 19 June 2010 (UTC)

When Russell and Whitehead did their work, the distinction between sentences and propositons (see Propositions versus Sentences) had not yet been made explicit in mathematical logic. In order to avoid inconsistency because of incompleteness, Gödel insisted on the restriction that the theory Russell was not allowed to speak of its its own inference relationship ⊢_Russell. (Wittgenstein refused to accept Gödel's restriction.) Also, roundtripping (see Roundtripping Reification and Abstraction) was an extension to mathematical logic that Gödel introduced to prove incompleteness although he did not formalize it because the proof was carried out in an alleged "meta-theory" which he chose not to formalize or specify too carefully (probably because inconsistency lurked).67.169.144.115 (talk) 21:51, 19 June 2010 (UTC)

I believe you are simply wrong. The usual formalism known as "Hilbert-style deduction" does not have any provision for treating inference rules as propositions, and Hilbert stopped being active well before the thirties. So the timeline you seem to have in mind just doesn't make sense. If I'm wrong, prove it with references to standard sources. --Trovatore (talk) 22:07, 19 June 2010 (UTC)

Leaving aside the historical issues (of which there may be many), perhaps this is a terminological problem? What exactly is meant when you say that Goedel "disallowed" something? You have said repeatedly that he disallowed some kinds of sentences, or that he insisted on some kind of restriction. Can you cite a few examples of places where he did that? Perhaps if you could show me a place in one of his papers where he made an explicit statement of that kind I would be better able to understand what you are driving at.--Taekwandean (talk) 22:48, 19 June 2010 (UTC)

In his paper on the incompleteness theorems, Gödel explained that the proof is not in Russel's system (the foundation of all of mathematics). Instead, the proof is in a alleged (poorly specified) "meta-theory." 99.29.247.230 (talk) 17:15, 20 June 2010 (UTC)

Of course it quickly become known that Goedel's proof can be formalized in PRA, an extremely weak theory of arithmetic. This is referenced in footnote 1 of the article. — Carl (CBM · talk) 19:09, 20 June 2010 (UTC)

Professor Hewitt's work is mischaracterized in the article

The following charaterization of Professor Hewitt's work was removed from the article:

Carl Hewitt (2008) has proved that in inconsistency toleratint theories developed for pervasively inconsistent software systems, incompleteness infers inconsistency because theories can prove their own Gödel sentences and are therefore inconsistent.

by contrast the characterization in the aricle

Carl Hewitt (2008) has proposed that (inconsistent) paraconsistent logics that prove their own Gödel sentences may have applications in software engineering.

is deficient in the following ways:

1. It denigrates his work by alleging that it "may" have applications in software engineering.
2. It places his work under the limitations of "paraconsistent logic" that is a very limited form of inconsistency tolerant logic.
3. It misses the fundamental point that incompleteness infers inconsistency in the powerful logics required in software engineering.
4. It entirely misses his thesis that software systems must tolerate immense numbers of inconsistencies and therefore it is OK that incompleteness entails inconsistency about a self referential proposition that has no impact on software engineering (namely the propositon: This proposition is unprovable.)

63.249.99.129 (talk) 20:42, 19 June 2010 (UTC)

I would be perfectly happy to remove all mention of Hewitt's work. Then there would be no risk of mischaracterization. --Trovatore (talk) 20:52, 19 June 2010 (UTC)

Contrary to your second assertion, paraconsistent logic is not a limited form of "inconsistency-tolerant logic". First, the system Hewitt studies is a particular example of a paraconsistent logic. Second, there is no general definition of "inconsistency-tolerant logic" to which you can appeal; the term is only used by Hewitt. It might refer to Hewitt's system, or to paraconsistent logic in general, but in either case this goes against your claim.

Issues 3 and 4 seem to be primarily about Hewitt's proposed applications of these methods to software engineering. That is an extremely tangential issue for this article, since the incompleteness theorems are nearly exclusively studied in the context of classical logic.

I have not seen any evidence that Hewitt's proposed methods are widely employed in software engineering, nor do I believe they are taught in software engineering texts. This is why the article says "may" (issue 1): because the applications appear to hypothetical at this time. This is different than, say, the study of the boolean satisfiability problem, which I do believe is concretely related to software engineering. — Carl (CBM · talk) 21:03, 19 June 2010 (UTC)

In fact, the Boolean satisfiability problem is rather tangential to the fundamental problems of software engineering--it is only applicable to a few narrow applications that can be consistency axiomatized. Pervasive inconsistency is probably the most fundamental problem currently facing software engineering. Also, you are wrong about incompleteness being exclusive to classical logic; it is also fundamental to the literative of inconsistency tolerant logic that is now being applied to software engineering.67.169.144.115 (talk) 22:04, 19 June 2010 (UTC)

I suspect that reviewing Wikipedia:Sockpuppet investigations/CarlHewitt/Archive and WP:DENY is in order. —David Eppstein (talk) 22:30, 19 June 2010 (UTC)

I can see your point. However, if it's actually true that no one before Goedel had a formalism for propositions that did not include rules of inference, I would genuinely like to know that. It sounds like complete crap to me, but history is not really my best subject. --Trovatore (talk) 22:33, 19 June 2010 (UTC)

The issue was not whether to allow rules of inference. Rather it was a question of whether the inference relatinship ⊢_Russell would be allowed, i.e. Bew(s)⇔⊢_Russell⌊s⌋. Gödel disallowed the inference relationship because allowing it would mean that incompleteness immediately proved inconsistency 99.29.247.230 (talk) 15:31, 20 June 2010 (UTC)

That's complete nonsense. Goedel "disallowed" nothing at all. The formalism he was studying was what it was; he did not impose any "restrictions" on it. --Trovatore (talk) 19:02, 20 June 2010 (UTC)

It is paradoxical that the formalism that Gödel was studying (Principia Mathematica) was fuzzy analogous to the way that Frege's set theory was fuzzy when Russell formulated his famous pardoxical set (this set that all sets that are not members of themselves) and derived an inconsistency. Likewise Wittgenstein derived a contradiction from a paradoxical proposition (the proposistion that this proposition is not provable) and derived an inconsistenecy. In both cases the inconsistency turns on the language that is available for constructing new entities.67.169.144.115 (talk) 21:01, 20 June 2010 (UTC)

I do not believe you that the formalism was "fuzzy". Prove it, with standard references (not "knols" written by Hewitt). --Trovatore (talk) 21:03, 20 June 2010 (UTC)