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

Girard

I spent part of today reading through Girard's account of the incompleteness theorems, chapter 2 of his rather opinionated proof theory notes "The Blind Spot" ([1] specifically [2]). It's a bit weird to start with, made weirder by occasional roughness in the translation from French, but I found it pretty interesting and I learned some things. It's not really suitable for reference from the article, but others here might like it too. 66.127.55.192 (talk) 10:04, 18 February 2010 (UTC)

i like this quote--maybe we can use it: "From a certain viewpoint, the (immense) endeavour accomplished by Gödel is not that surprising. After all, those metamathematics, those finitistic meta-methods, there are quite part of mathematics. Let us be clear : if metamathematics could not have been translated in mathematics, this would have been an incompleteness much more dramatic than Gödel’s. In fact, Gödel’s work must be seen as the end of the process starting with Cantor, Dedekind,... of coding mathematics: the pioneers did encode reals by sets of rationals in turn encodable by integers, Gödel closed the cycle by treating language." —Preceding unsigned comment added by 75.62.109.146 (talk) 11:05, 26 February 2010 (UTC)

I think it would be better to say: Godel's work must be seen as the end of the process starting with Cantor, Dedekind,... of coding mathematics: ... Godel closed the cycle by treating computation. Godel encoded primitive recursive functions, later general recursive functions, and always encouraged using Turing's work on computers as the definition of a formal system.Likebox (talk) 16:24, 26 February 2010 (UTC)

Gödel was suspicious of abstraction because he was cautious and afraid of inconsistency. Consequently, his 1931 proof encoded logical sentences as character strings. Modern computer science has proceeded mainly from the lambda calculus rather than Turing machines. Also modern proofs of incompleteness make use of the lambda calculus to prove the logical fixed point theorem. And abstract principles such as roundtripping and provability theory have replaced using Gödel numbers to code character strings. So abstraction is winning out in computer science.98.210.236.39 (talk) 14:28, 27 February 2010 (UTC)

It's a quote from Girard's book, so if you want it to be written differently, you'll have to take it up with Girard ;). 75.62.109.146 (new address) (talk) 07:35, 27 February 2010 (UTC)

I know--- I just was adressing the other editors.Likebox (talk) 07:41, 27 February 2010 (UTC)

"Incompleteness Theorems" on Knol

There is an article on Incompleteness Theorems over on Google Knol that has additional material.98.210.236.39 (talk) 10:59, 27 February 2010 (UTC)

This material is crappy.Likebox (talk) 13:03, 27 February 2010 (UTC)

Do you have any *particular* objection? 98.210.236.39 (talk) 13:40, 27 February 2010 (UTC)

I find myself agreeing with Likebox. What do you consider relevant that could be added here. — Arthur Rubin (talk) 14:47, 27 February 2010 (UTC)

The article is already too long and disjointed. It should be divided into two articles: (1) on the mathematics of incompleteness theorems and (2) on a historical perspective of incompleteness theorems.98.210.236.39 (talk) 18:38, 27 February 2010 (UTC)

Of course everyone realizes that there's another article titled On Formally Undecidable Propositions of Principia Mathematica and Related Systems. Perhaps this companion could absorb the "history" (including the problem of "finitary" proofs) and "the aftermath" (the immediate aftermath, am unclear where the "contemporary" aftermath should go) etc while the article associated with this page could be tightened to present explications of the theorems only. Per my comment above I encourage those who are interested mainly in the mathematical end of things (as opposed to the historical) and can lay their hands on it read Kleene's "seven part" explication in Volume I of Kurt Godel Collected Works.

(On different note, the "Chinese remainder theorem" comes up in some (but not all) of the explications. I did a search of our article and found no mention of "chinese" or "remainder". But when I searched wikipedia I discovered an article Gödel numbering for sequences that contains a detailed discussion of this topic. And here I thought he was relying on the fundamental theorem of arithmetic . . .. What's going on? And, is it just me or is there little or no coordination between these various-but-associated articles?) Bill Wvbailey (talk) 23:16, 27 February 2010 (UTC)

Let's keep the On Formally Undecidable... article strictly about the publication, please. Historical context and aftermath both belong here — though not quite as detailed on the history as I expect you would prefer. --Trovatore (talk) 23:31, 27 February 2010 (UTC)

The article about Gödel numbering for sequences seems redundant with the article Gödel's_β_function. 75.62.109.146 (talk) 07:57, 28 February 2010 (UTC)

They are somewhat redundant in present form, but really Gödel numbering for sequences should discuss a more general concept (assigning Goedel numbers to finite sequences) while the article on the β function should discuss that particular method in more detail. There are many other ways to assign Goedel numberings to sequences, and also that article should explain the key step of going from an ordered pair to a single Goedel number; the β function only gets you down to a pair. Unfortunately the article Gödel numbering for sequences uses a different function from the three-argument β function often considered. — Carl (CBM · talk) 13:54, 28 February 2010 (UTC)

Unfortunately, the Knol article is a model of clarity and organization by comparison with the mess we have here. Let's get our act together! 63.249.108.250 (talk) 20:34, 27 February 2010 (UTC)

Well, ya know — we'd all love to see the plan. --Trovatore (talk) 22:01, 27 February 2010 (UTC)

I gave you a plan for writing this page and others a while ago, people here just attacked it.Likebox (talk) 16:41, 28 February 2010 (UTC)

Likebox, Your ability to selectively remember events is truly stunning. Almost as much as your passive-aggressive victim complex. But please, by all means, keep digging your own hole. 71.184.62.82 (talk) 22:00, 28 February 2010 (UTC)

I don't see in what way I am a victim: it's not me that suffers if my work is not incorporated. It's your loss.Likebox (talk) 22:52, 28 February 2010 (UTC)

The larger problem is how to report on modern published work on incompleteness theorems. The current article only addresses issues that predate modern computing.99.29.247.230 (talk) 17:19, 1 March 2010 (UTC)

There is indeed modern work on incompleteness, for example I can think of an interesting result due to Harvey Friedman that says that any effective theory of second-order arithmetic extending ACA₀ that has an ω-model must have an ω-model that does not itself contain a countable ω-model for the theory. However every countable ω-model of WKL₀ does contain a countable ω-model of WKL₀. I think that results like this are too technical to include in a general encyclopedia article on Goedel's theorems.

Another possible interpretation of "modern published work on incompleteness theorems" is reflection principles. I think that work should be covered on Wikipedia somewhere, but probably it is outside the scope of this article to cover in any depth.

There is also a lot more that could be said about generalizing and formalizing the incompleteness theorems, as in Smorynski's article in the Handbook of Mathematical Logic. I think that would also end up going out of the scope of an introductory article.

However, I think that what 99.xxx is talking about is not modern work on the incompleteness results. Rather, the IP is talking about Hewitt's work on certain paraconsistent logics. That is mentioned in the article already, at the end. I don't see any reason why it should be mentioned in more detail than that, given that it is only tangentially related to the actual incompleteness theorems. It's the type of thing that's worth including as a vague mention, but not worth going into in depth. — Carl (CBM · talk) 20:58, 1 March 2010 (UTC)

It's unclear to me how "contemporary" the modern work should be. Kleene's commentary before Goedel's 1931 in the 1986 Kurt Goedel Collected Works Volume I cites in order of their appearance: (1) Gentzen 1936 with Takeuti 1975 and Schutte 1977 "giv[ing} fairly substantial account of work in this direction" [all this having to do the problem of "finitary"], (2) Goedel himself in his 1958 and 1972 extending "a notion of computable functions of finite type (i.e. of computable functionals)" [this again having to do with the "finitary" problem], (3) Rosser's 1936 reducing the question from omega-consistency to simple consistency, (4) Paris and Harrington 1977 of which Kleene says "A new landmark in the expanding evolution of theory started by Goedel's 1931 is the discovery by Paris and Harrington in 1977 . . . this is a refinement of Ramsey's theorem wich is (i) a Π⁰₂ statement and (ii) equivalent to the Σ⁰₁ reflection principle for PA . . . hence independent of PA". He then brings in Kreisel 1980: "What is essentially involved is that the function determined by the Π⁰₂ Paris-Harrington statement majorizes all the provably recursive functions of PA (as shown in another way by Ketonen and Solovay in 1981)." (all quotes pages 139-141). Anyway, this is Kleene's take on the matter as of ca 1986. Bill Wvbailey (talk) 23:02, 1 March 2010 (UTC)

None the above work is relevant to modern computer science. However, the following published work on incompleteness theorems *is* relevant to modern computer science:

• Richard Routley. 1979. “Dialectical Logic, Semantics and Metamathematics” Erkenntnis 14
• Graham Priest, and Richard Routley. 1989. “The History of Paraconsistent Logic” in Paraconsistent Logic: Essays on the Inconsistent Philosophia Verlag.
• Carlo Cellucci. 1991. "Gödel's Incompleteness Theorem and the Philosophy of Open Systems" Kurt Gödel: Actes du Colloque, Neuchâtel 13–14 juin 1991, Travaux de logique N. 7, Centre de Recherches Sémiologiques, University de Neuchâtel.
• Per Martin-Löf. 1995. "Verificationism then and now" in "The Foundational Debate" Kluwer.
• Noson Yanofsky. 2003. "A universal approach to self-referential paradoxes, incomleteness anf fixed points" Bulletin of Symbolic Logic. 9 No. 3.
• Jean-Yves Girard. 2004. "The Blind Spot: Lectures on proof-theory" Roma Tre.
• Graham Priest and Koji Tanaka. 2004. “Paraconsistent Logic” The Stanford Encyclopedia of Philosophy.
• Solomon Feferman. 2006. "Are there absolutely unsolvable problems? Gödel's dichotomy" Philosophia Mathematica Series III vol. 14.
• Carl Hewitt. 2008. "Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency" Coordination, Organizations, Institutions, and Norms in Agent Systems III, Springer-Verlag.
• Carl Hewitt. 2009. "Common sense for concurrency and inconsistency tolerance using Direct Logic" ArXiv 0812.4852. —Preceding unsigned comment added by 98.210.236.39 (talk) 03:34, 2 March 2010 (UTC)

A few of those are relevant to the article. The ones on paraconsistent logic, not so much. This article is not fundamentally about things "relevant to modern computer science", however, and making it so is not a goal. The article is intended to be about Goedel's incompleteness theorem as it is usually studied in mathematical logic. — Carl (CBM · talk) 05:33, 2 March 2010 (UTC)

This article is currently focused on events that occurred more than a quarter century ago. It was an accident of history that incompleteness was first proved for Peano Arithmetic. Modern computer science is not so focused on Peano Arithmetic and ZF. With roundtripping, *every* theory is incomplete. Consequently, this article is not so relevant to modern computer science.98.210.236.39 (talk) 17:57, 2 March 2010 (UTC)

Right. Like I was saying, the article is intended to be relevant to Goedel's incompleteness theorems. If that means it is not relevant to modern computer science, there is no contradiction, because Goedel's theorems are not particularly about modern computer science. The incompleteness theorems are closely related to recursion theory, of course. (Also, regardless of "round-tripping", the set of sentences true in the standard model of arithmetic is by definition a complete theory.) — Carl (CBM · talk) 19:05, 2 March 2010 (UTC)

It's apparent that the Wikipedia has a rather large hole in its coverage of incompleteness theorems. Incompleteness theorems are highly relevant to modern computer science even though the work on incompleteness theorems has gone far beyond the work of Gödel that is the focus of this article.

Also, you do not have much of a theory by way of the set of sentences true in the standard model of arithmetic. About the only important thing known about this set is that by definition it contains the theorems of Peano Arithmetic as a proper subset. Incompleteness applies to real theories of interest to modern computer science.65.106.72.229 (talk) 20:57, 4 March 2010 (UTC)

It's apparent that what you see as a gap is not considered "of interest" in many reliable sources. Still, you're welcome to write an article on "incompleteness theorems", to the extent covered by reliable sources other than Hewitt. — Arthur Rubin (talk) 09:58, 5 March 2010 (UTC)

Please don't. There was an article contemporary incompleteness theorems for a while. It was a hodge-podge of topics: continuum hypothesis, paraconsistency, and absolutely unsolvable problems in intuitionistic logic. While all of these are of separate interest, they are not "Goedel's incompleteness theorem", as each of them differs in a significant way from Goedel's theorem. — Carl (CBM · talk) 12:24, 5 March 2010 (UTC)

Wikipedia doe not properly treat the topic of "incompleteness theorems" which redirects here. The current article is neither a proper article on the mathematics of incompleteness theorems nor is it a proper history of incompleteness theorems.99.29.247.230 (talk) 22:10, 5 March 2010 (UTC)

We're all doing what we can. — Carl (CBM · talk) 22:15, 5 March 2010 (UTC)

Check this outLikebox (talk) 23:38, 5 March 2010 (UTC)

Somehow the current version of the article has entirely missed the controversy with Wittgenstein. See Incompleteness Theorems.98.210.236.39 (talk) 15:24, 7 March 2010 (UTC)

Seems to be a controversy with Hewitt, rather than with Wittgenstein. — Arthur Rubin (talk) 16:04, 7 March 2010 (UTC)

The Knol article quotes Wittgenstein:

Let us suppose I prove the unprovability (in Russell’s system) of P [⊢_Russell ⊬_Russell P] [where P [Uninferable_Russell (see Knoll article)] is the Gödel sentence of the system]; then by this proof I have proved P [⊢_Russell P ]. Now if this proof were one in Russell’s system—I should in this case have proved at once that it belonged [⊢_Russell P ] and did not belong [⊢_Russell ¬P ] to Russell’s system.—That is what comes of making up such sentences. But there is a contradiction here!—Well, then there is a contradiction here [in Russell’s system]. Does it do any harm here? ...

Have said—with pride in a mathematical discovery: ‘Look, this is how we produce a contradiction.’

Also Gödel said that he disagreed with Wittgenstein.

So the controversy was between Wittgenstein and Gödel.98.210.236.39 (talk) 16:31, 7 March 2010 (UTC)

That, I can see, assuming Hewitt correctly "quoted" Wittgenstein, rather than translating Wittgenstein's statements into Hewitt's notation. I don't have a copy of the reference cited there as [Wittgenstein 1956], although not actually in the bibliography. If we can obtain a reliable source for Wittgenstein's statement, then it may deserve a note somewhere in Wikipedia. Probably not here, as it's not specifically related to "Gödel's incompleteness theorems", or even to incompleteness theorems in general. Perhaps under paraconsistent logic or a related article.

Wittgenstein was manifestly writing about Gödel's theorem. The material in itallics is a quotation of Wittgenstein. The non itallic material in square brackets is interpretation by the author of the Knol article.99.29.247.230 (talk) 19:22, 7 March 2010 (UTC)

(Misspelling "italics" doesn't lend verisimilitude to your comment.)

Actually, because < math > tags (and the Knol equivalent) put symbols in italics by default, I can't tell which expressions are attributed to Wittgenstein and which to Hewitt. Could you (Hewitt) quote the paragraph as Wittgenstein wrote it? You present a reasonable argument, even if "Russell's" system is the one quoted. — Arthur Rubin (talk) 20:58, 7 March 2010 (UTC)

The actual Wittgenstein quote is as follows:

Let us suppose I prove the unprovability (in Russell’s system) of P [where P s the Gödel sentence of the system]; then by this proof I have proved P. Now if this proof were one in Russell’s system—I should in this case have proved at once that it belonged and did not belong to Russell’s system.—That is what comes of making up such sentences. But there is a contradiction here!—Well, then there is a contradiction here [in Russell’s system]. Does it do any harm here? ...

Have said—with pride in a mathematical discovery: ‘Look, this is how we produce a contradiction.’

The above version just strips out the remarks not in italics.98.210.236.39 (talk) 23:12, 7 March 2010 (UTC)

How mainstream is the Hewitt material? (Likebox prefers "crappy")

In order to understand Godel's theorem, you need to have the proof in your head. In order to do that, you must formulate it in terms of computation, so that you can see what is going on.

Given an axiomatic system S which proves theorems about computer programs, 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.

S cannot consistently prove "GODEL does not halt". This formulation is superior to all others.

This statement and proof of the theorem explains Godel's construction completely, in particular, it makes it clear that there is no "stratified metatheory" (in other words, the theory of types of Principia Mathematica is not essential) and the only use of "consistency" is for formal reasons. The more general way to state the incompleteness theorem is that any computer program that prints out statements about the eventual behavior of other computer programs is going to get some statements wrong.

Wittgenstein was a philosophy twit, and had nothing important to say, otherwise he would have been a mathematician. The mathematicians in the crowd, Gentzen and Hilbert, formulated a proper response to Godel's theorem, which is "ordinal analysis". The correct accepted solution to incompleteness is to pass to stronger and stronger systems, not to pass to inconsistent theories. The idea of passing to inconsistent systems, which is Hewitt's response is the first idea you would think of, and it's probably the wrong idea.

Just for kicks, here's how you formulate the incompleteness theorems in Chaitin's preferred way (or Boolos):

Write the program CHAITIN which does the following:

1. Prints its own code into a variable R
2. Deduces all theorems of S looking for the theorem "Program P has a minimal length longer than R"
3. Runs program P.

By construction, CHAITIN has length equal to the length of R, but is equivalent to the first program P whose minimal length version is longer than R. But R is equivalent to P, and this contradicts the minimal length of P. So you conclude that axiom system S is incapable of proving that any program P is of minimal length when that minimal length is greater than R! That's a very profound incompleteness.Likebox (talk) 16:01, 7 March 2010 (UTC)

Although I agree that Hewitt's material is crappy non-mainstream, so is Likebox's. Perhaps they should have equal weight in another article (not this one). — Arthur Rubin (talk) 16:13, 7 March 2010 (UTC)

That is your silly opinion, born of old conflicts. The material I am presenting is just a rewording of Kleene's proof to be self-contained. The fact that you don't recognize it as such is not my problem, but it is a problem for Wikipedia.Likebox (talk) 16:42, 7 March 2010 (UTC)

Perhaps. My opinion, however, is shared by all mathematician-editors who have commented here, and even a few philosopher-editors. — Arthur Rubin (talk) 17:21, 7 March 2010 (UTC)

You realize you may be closer to Hewitt than you thought; your "print your own code" operator seems closer to the "reification/abstraction" operators in his logic than to traditional logic. — Arthur Rubin (talk) 17:24, 7 March 2010 (UTC)

Rubin has a very good point. Gödel did not give a formal proof of incompleteness in part because he did not axiomatize reification and abstraction. See Common sense for concurrency and inconsistency tolerance using Direct Logic for an axiomatization.99.29.247.230 (talk) 19:29, 7 March 2010 (UTC)

That is another reason I don't trust Hewitt's results. Gödel did (eventually) give a formal proof, although the proof that it's a formal proof is in the metatheory. For the first incompleteness theory (for ω-consistency), that ("P" is a proof of "S") implies S can only be done within the theory for specific P and S. — Arthur Rubin (talk) 21:09, 7 March 2010 (UTC)

Am confused. To the various biographers' knowledge, Goedel never offered a formal proof of the 2nd incompleteness theorem. Cf the timeline above: *1939 – a full proof of the second incompleteness theorem is published in Hilbert and Bernays 1939 (cf footnote 6 Dawson:70). But I haven't seen Volume II of his published papers so I cannot be "certain". Bill Wvbailey (talk) 23:07, 7 March 2010 (UTC)

Actually Gödel never gave a formal proof of even his 1^st incompleteness theorem. However, later authors have claimed to give formal proofs.98.210.236.39 (talk) 00:10, 8 March 2010 (UTC)

Hewitt does not have any "results", he just reexpresses the same thing in his own language, which is supposedly inconsistency tolerant. There is nothing new there, and I know, because I waded through it. The stuff I am presenting is also the same old thing, except I make no bones about saying so, and I don't try to claim it is new, just to put it on Wikipedia--- home of old results.

The fact that your "opinion" seems to be shared by "mathematician editors" is unfortunate, because it shows that there is a too-low level of contributors here. In their defense, Trovatore thinks the proof is correct and pedagogically useful, and CBM just opposes it because of his own personal political preferences. Nobody thinks it is either something new or something wrong'.

The "print your own code" operator is just the fixed point theorem, and has absolutely nothing to do with the reification/abstraction" operators in Hewitts crap.Likebox (talk) 22:20, 7 March 2010 (UTC)

Likebox's proof of incompleteness involves both the fixed point theorem and the roundtripping principle. See Common sense for concurrency and inconsistency tolerance using Direct Logic for details.98.210.236.39 (talk) 23:57, 7 March 2010 (UTC)

To User:Wvbailey; Defer. I thought Gödel offered a formal proof with ω-consistency in place of consistency. However, I'm not sure that's correct, either.

Still, Likebox and Hewitt agree that the other's work is crap WP:FRINGE, and the rest of us agree. — Arthur Rubin (talk) 00:08, 8 March 2010 (UTC)

I personally consider the first incompleteness theorem (as you've stated correctly above-- it is framed in omega-consistency, not simple consistency) to be "formal" (and so does anyone else who's actually read the proof). But it's the second proof of which he admits to providing only a "sketch". Here's what he writes about the "second" (actually XI) of his theorems, right at the very end of his 1931 paper:

"We have limited ourselves in this paper essentially to the system P and have only indicated the applications to other systems. The result will be expressed and proved in full generality in a sequel to appear shortly. Also in that paper, the proof of Theorem XI [the so-called "second incompleteness theorem"], which has only been sketched here, will be presented in detail." (cf Goedel 1931 in Davis 1965:38).

Goedel never bothered to follow up on his promise. Historians conclude that (i) he was by nature a point-man, and he'd done his work and was moving on and (ii) his work was so rapidly accepted (excepting by Zermelo) that he didn't see the need. Historical factors such as Nazis + escapes of comrades (e.g. von Neumann) to the US and his marriage and the death of Herbrand and etc etc also may have played a role in his general loss of interest (my conjectures). Why Bernays et. al. bothered to complete the "formal proof" of the 2nd theorem is anyone's guess. Bill Wvbailey (talk) 01:27, 8 March 2010 (UTC)

Gödel never formalized important properties like the Roundtripping principle. However, Shankar, O'Conner, and Sieg have published papers on formal proofs.98.210.236.39 (talk) 04:21, 8 March 2010 (UTC)

Yes, Gödel used the assumption of ω-consistency. Rosser's proof used the assumption of consistency. However, Gödel did not offer a formal proof. One important gap is that he never formalized roundtripping.98.210.236.39 (talk) 00:27, 8 March 2010 (UTC)

I don't think that it's necessary to put down Hewitt's work in order to explain why it shouldn't be in the article. The paper of Hewitt's that I read on the arxiv explained to me what Hewitt is doing, and it seemed reasonable enough if one wants to study that kind of paraconsistent logic. I agree with Likebox that, to some extent, the proof of incompleteness in that paper come down to reworkings of the usual proof. But sometimes being able to translate over an existing proof into a new system is useful to demonstrate that the new system is interesting. In any case it's not atypical; for example, if I create a new collection of axioms for set theory, I might help show their worth by showing how existing proofs can be formalized in my axioms. Given that this is just one part of a larger paper, I don't think it's a negative point in the paper overall.

My main concern about describing Hewitt's work in detail in this article is that his work is simply not very closely related to the incompleteness theorems as they are usually studied. Partially as a result of my background in mathematical logic, and partially because of editing this article, I have seen a reasonably large amount of literature on Goedel's theorem. No standard reference discusses paraconsistent logic, category theory, etc. There may well be interesting papers that discuss the incompleteness theorem in those contexts, but given the very low overall interest in such things in the literature on the incompleteness theorems, we should not go into depth here. I favor including a short pointer to Hewitt's paper, as it is an interesting piece for further reading. But I don't think that more than that can be justified from the broader literature. — Carl (CBM · talk) 01:32, 8 March 2010 (UTC)

The Knol article Incompleteness Theorems tied together two important themes that have received extensive treatment in the literature:

1. Wittgenstein's skepticism of metatheories and the resulting inconsistency
2. Providing completely formal proofs of incompleteness

Unfortunately, the current article does not treat the Wittgenstein theme at all and has only a single sentence about completely formal proofs.98.210.236.39 (talk) 20:05, 8 March 2010 (UTC)

I'm the one who put in the sentence about formalized proofs. I think it's worth having that sentence since WP is a reference work and it's appropriate to point people towards info about formalizations if they are seeking it. But, the formalizations are not terribly interesting from a mathematical point of view in relation to the theorems, so the one sentence is enough. And yes, Hewitt's stuff and Likebox's stuff are both crappy non-mainstream. 66.127.52.47 (talk) 05:33, 13 March 2010 (UTC)

You're talking about slightly different types of formalized proofs. You mean proofs formalized using software like Coq to actually generate formal proofs from the axioms of the original system. Hewitt is talking about using a paraconsistent logic in which Goedel's theorem can be expressed more naturally. I am not sure whether Hewitt would even count the following as a "formalization" in the sense he is talking about; it is certainly a formalization in another sense:

(*) If T is an effectively axiomatized system interpreting enough of the theory of the integers, and Con(T) is the "canonical" sentence in the language of PRA asserting the consistency of T, then there is a formula φ in the language of T such that PRA proves Con(T) → Con(T + φ) and PRA proves Con(T) → Con(T + ¬ φ).

Theorem (*) is different than a proof of Goedel's theorem in Coq because the proof of (*) does not use the axioms of T at all, only the axioms of PRA. — Carl (CBM · talk) 14:19, 13 March 2010 (UTC)

The proofs in Common sense for concurrency and inconsistency tolerance using Direct Logic are completely formal because they make all the axioms explicit including roundtripping. However the proofs would be difficult to formalize in Coq because they are not in 1^st order classical logic. Furthermore, it looks like PRA is something of a red herring for proving incompleteness theorems in general. For example the proofs of incompleteness in the Knol Incompleteness Theorems article do not rely on PRA.98.210.236.39 (talk) 13:17, 14 March 2010 (UTC)

Of course they don't, because they are in Hewitt's idiosyncratic paraconsistent system instead of in a standard first-order theory. PRA is relevant to the incompleteness theorems because PRA is commonly identified with finitism, and so the ability to prove formalized versions of the incompleteness theorems in PRA demonstrates that the theorems are finitisitcally provable. — Carl (CBM · talk) 14:59, 14 March 2010 (UTC)

From the point of view of Computer Science, the exclusive focus on finitism in this article is idiosyncratic. Hilbert introduced finitism to prove mathematics consistent by means that he thought secure. However, Gödel showed that Hilbert's program could not be carried out. Then Gentzen proved the consistency of PA by non-finitistic means. Wittgenstein noticed that rejection of the artificial Tarskian meta-theoretic framework means that the Gödelian proposition leads to inconsistency (but this does no harm to inconsistency tolerant logic). So why should anyone care about finitism?98.210.236.39 (talk) 15:43, 14 March 2010 (UTC)

The article here on wikipedia does not dwell on finitism; it only mentions PRA in one paragraph and a footnote. PRA is widely used in mathematical logic as a stand-in for a weak theory, for results where greater foundational importance is desired; see p. 859 of Smorynski's paper in the HML. — Carl (CBM · talk) 16:29, 14 March 2010 (UTC)

From the perspective of modern computer science, the current article is archaic and narrow-minded. It fails to mention either Wittgenstein or Martin-Löf and has only a single sentence about Gentzen. Also PA is just as much a red herring as PRA in terms of a modern understanding of incompleteness theorems.98.210.236.39 (talk) 17:39, 14 March 2010 (UTC)

Your arguments seem to be based on the assertion that Hewitt represents "modern computer science", and his arguments are hence notable in all articles (loosely) related to computer science. (And why is "modern computer science" not subject to finitism? Doesn't any computation have a finite number of steps?) — Arthur Rubin (talk) 18:15, 14 March 2010 (UTC)

Modern theories of computation are not finitistic. See the article on Denotational semantics.63.249.99.129 (talk) 22:39, 21 March 2010 (UTC)

IMHO Wittgenstein, Martin-Löf, and Gentzen are far more impoortant than Hewitt. It's PRA and PA that are not fundamental to computer science.63.249.116.52 (talk) 21:06, 14 March 2010 (UTC)

For better or worse, Wittgenstein's remarks on mathematical logic were never well received. A few philosophers argue that maybe the his remarks are not as bad as they were originally thought to be, but it's still far too soon to say that Wittgenstein has any significant influence on mathematical logic. Martin-Löf is much more influential, but Gödel's theorems are really about classical logic. There are many other examples of incompleteness in the intuitionistic predicate calculus. Gentzen is mentioned in the article already; his theorem complements the incompleteness theorem for PA, but it's really an independent theorem from the incompleteness results. Gentzen's proof, by the way, makes particular use of PRA for its foundational significance.

However, this whole business about "computer science" is beside the point. Goedel's theorems are theorems of mathematical logic, not theorems of computer science. If computer scientists are interested in the theorems, that's wonderful. But there's no more reason to cater specifically to computer scientists in this article than there would be to cater to physicists in the article on calculus. — Carl (CBM · talk) 00:17, 15 March 2010 (UTC)

Theorems and proofs don't belong to anyone regardless of whether they are authored by people from computer science or math departments. But the current article has an ancient obsolete viewpoint that is inappropriate.63.249.99.129 (talk) 22:39, 21 March 2010 (UTC)

The current article is stuck in a very narrow point of view that ignores a theme in the literature that has become increasingly important. In the discussion above, the following quotation appeared from the Stanford Encyclopedia on Wittgenstein's Philosophy of Mathematics,

After the initial, scathing reviews of RFM [Remarks on the Foundations of Mathematics], very little attention was paid to Wittgenstein's (RFM App. III) and (RFM VII, §§21-22) discussions of Gödel's First Incompleteness Theorem (Klenk 1976, 13) until Shanker's sympathetic (1988b). In the last 11 years, however, commentators and critics have offered various interpretations of Wittgenstein's remarks on Gödel, some being largely sympathetic (Floyd 1995, 2001) and others offering a more mixed appraisal [(Rodych 1999a, 2002, 2003), (Steiner 2001), (Priest 2004)]. Recently, and perhaps most interestingly, (Floyd & Putnam 2000) and (Steiner 2001) have evoked new and interesting discussions of Wittgenstein's ruminations on undecidability, mathematical truth, and Gödel's First Incompleteness Theorem [(Rodych 2003, 2006), (Bays 2004), (Sayward 2005), and (Floyd & Putnam 2006)].

The current article lacks any discussion of Wittgenstein, Shankar, Priest, Routley, Rodych, etc.98.210.236.39 (talk) 17:56, 15 March 2010 (UTC)

I question whether it's become increasingly important, but, even if it has, its importance before 1985 was 0, so an increase doesn't mean it's sufficiently notable for an encylopedia. — Arthur Rubin (talk) 18:09, 15 March 2010 (UTC)

Wittgenstein was into it from cicra 1930. His viewpoint was anathama to Gödel, who refused to engage the issuess and instead claimed that Wittgenstein did not understand incompleteness. Now that modern computer science has to deal with inconsistency, Wittgenstein has regained prominence.63.249.99.129 (talk) 22:39, 21 March 2010 (UTC)

lecture notes

This looks pretty good, and more "modern" than the textbook presentation I'm used to. (No it doesn't use Turing machines). I think I can read it so I'm going to try. 66.127.52.47 (talk) 07:58, 13 March 2010 (UTC)

The van Oosten notes look good. Their proof method is the same as the one in this article, via the diagonal lemma. There are actually a lot of lecture notes on the web that cover Goedel's theorem. Here are a few more:

• [3] (Stephen Simpson) - proof via the diagonal lemma
• [4] (Itay Ben-Yaacov) - proof via recursive inseparability
• [5] (Jeremy Avigad) - proof via computability, also proves recursive inseparability

I don't think we should put all these into the article; there are probably a dozen more like them. — Carl (CBM · talk) 13:35, 13 March 2010 (UTC)

Methinks the lambs have lost their way

Does anyone have suggestions about how to focus this onto some immediate tasks? For instance what does this article need to become a GA, A, FA ?

RE: mysterious IP-people: I am confused by POV's from the various IP's -- for example are these the same or different people? I can't keep them straight (there's "99" and "98" and "63" and "66" etc). Whoever they are they seem very competent. I wish though, that they would pull back their IP curtain a bit.

There appear to be 2 or 3 "currents" flowing here all vaguely having to do with "history" -- (0) history of how-why incompleteness was a big issue to Hilbert et. al., (1a) history of incompleteness immediately before and after Goedel's incompleteness theorems, (1b) history during Goedel's life but after he went on to other work, (2) history of incompleteness after Goedel's death (3) contemporary research.

Can someone(s) please make some suggestions, give guidance? To me this feels like chaos. Am I alone in this feeling? Thanks, Bill Wvbailey (talk) 18:49, 15 March 2010 (UTC)

I agree the IP address soup is somewhat chaotic. I recognize the 66.xxx address; he or she has been editing math logic articles for a while. The other ones all appear to be associated with Hewitt and, lacking evidence to the contrary, I usually assume they are the same person. But this is not the same person as the 66.xxx editor, unless he or she has a split personality.

The relevance of the incompleteness theorem to the Hilbert program is very important, but I think the article already treats that. The criticism about Wittgenstein, "modern computer science", etc. is not extremely apropos.

As to GA or FA, I try to stay away from them. It's hard enough for me to get the article into a shape that I feel is half-decent, without trying to involve some reviewers who may have no sympathy for the topic whatsoever. It's a lot of effort and I don't personally think it results in a sufficient benefit to offset that.

Re immediate changes, I think adding a brief "history" section would be nice. But in general I think the article has an OK structure and covers the main points that it needs to cover. — Carl (CBM · talk) 01:42, 16 March 2010 (UTC)

What one could do though (although I am not particularly enthusiastic) is use this article for reviving A class reviews. Hans Adler 10:26, 16 March 2010 (UTC)

GA and FA basically are metrics for the number of footnotes and pictures in an article, not its quality. The main purpose of FA as I see it is if you want to present the topic to the public through Wikipedia's main page. For that, you want a topic of reasonably general interest and whose content is not overly technical. This article would have to be overhauled a whole lot to get to that style. The overview mathematical logic article (which is excellent) might be a better candidate. GA just seems pointless as far as I can tell. FA certification is actually not all that hard if you jump through all the hoops and if the subject matter is of general interest. I've been involved in one FA development in the past and the article sailed through FA review even though I personally felt it still had a lot of problems. This led to a bunch of frantic work from several editors the night before it went on the front page, but that just means don't start the process until you feel that the article is ready. 66.127.52.47 (talk) 09:30, 19 March 2010 (UTC)

original statements

I chopped out the original statements from Gödel's 1931 paper, since they used an incomprehensible old terminology and didn't seem to be doing the article any good. Feel free to revert if you think they had some purpose, but it may be better to move them (and some description of Gödel's terminology) to the article about the paper itself. I guess we should also make sure we have a precise technical statement with contemporary terminology that we can wikilink instead, preferably taken verbatim from a respectable textbook, something very mainstream. Anyone got a suggestion? 66.127.52.47 (talk) 09:12, 19 March 2010 (UTC)

The statement in modern language, sourced to Kleene, is still in the article. The older ones were there primarily as historical notes. I don't know if they would fit easily into the article on the paper itself. At the same time, I can't give a strong argument for including them in this article. — Carl (CBM · talk) 11:24, 19 March 2010 (UTC)

I was the "inserter" of these original statements (against the protests of some editors). But . . . the article has come a long way since then. (At that time) I put them there for a good reason -- I came looking for what the heck the "first" and "second" completeness theorems are, and could find nothing to help me out in this article, nor in the published literature(!). In fact I had to go to the original paper (as translated/printed in Davis 1965), and eventually surmised that the "first" is actually "Theorem VI" and the "second" is actually "Theorem XI". So my original intent was to help de-mystify the mysterious, first for myself, and secondly to reduce the "student's angst" when encountering the original paper. (Also -- The now-deleted sections also included the translation for "Bew" which appears in the article as well. Given that "Bew" is defined somewhere as the non-mysterious appreviation for Beweisbar i.e.

“Bew” abbreviates “Beweisbar = provable” (translations from Meltzer and Braithwaite 1962, 1996 edition:33-34) )

then I suppose there's no reason to keep the definitions incorporated in the original statements). In a recent read of the article I also found the paragraphs jarring, so maybe it's time to let them to go. I'd be happier if they were to go into footnotes rather than go althogether. But methinks I won't protest too much. Again, my personal interest here is to demystify the mysterious, to make this accessible to "everyman". Thoughts? Bill Wvbailey (talk) 00:10, 20 March 2010 (UTC)

Trovatore makes a reasonable argument that the article should just be about the publication history, in response to a suggestion that it also go into the surrounding math history. But, maybe it's ok for that article to have an excerpt from the paper itself, along with a brief explanation of the terminology, without going off-topic into other areas. The actual 1931 paper is still fairly readable if you start from the beginning, since it explains the terms as it goes along. But pulling out a chunk from the middle is pretty unreadable even to someone familiar with the concepts in modern language. 66.127.52.47 (talk) 07:47, 20 March 2010 (UTC)

Added: the article still translates "beweisbar" in the "arithmetization of syntax" section. 66.127.52.47 (talk) 10:11, 20 March 2010 (UTC)

One difficulty with quoting something to show "how the paper was written" is that the original is in German, so we would actually be quoting a translation, so we would not actually be showing how the original paper is written, just how the original paper might have been written if it had been written in English. I agree with Trovatore in general about keeping that article focused on the publication and translation history.

It is true that this article uses "Bew" for the proof predicate, which I like as a connection to history. (I also think it helps clarify the distinction between provability and formalized provability if we use a different word for the formalized version, rather than using the word "Provable" for both). — Carl (CBM · talk) 13:35, 20 March 2010 (UTC)

I'm okay with eliminating the original theorems' statements etc as long as we retain the little "original statement" paragraph (as it is presently written seems fine). It probably should be titled in plural as "Original statements" and be inserted above both the 1st and 2nd incompleteness-theorem sections. When we get a history section we might be meld into that section. BillWvbailey (talk) 23:20, 20 March 2010 (UTC)

Sounds like a good plan. I fixed statement/statements. CBM makes a good point about the original original statements being in German. 66.127.52.47 (talk) 03:01, 23 March 2010 (UTC)

Why is this article focused on the deification of Gödel to the exclusion of other viewpoints, e.g., Feferman, Priest, Wittgenstein, etc? 63.249.116.52 (talk) 21:22, 21 March 2010 (UTC)

I think you mean Feferman, Priest, Wittgenstein, and most importantly Hewitt ;-). 66.127.52.47 (talk) 03:01, 23 March 2010 (UTC)

Who is Hewitt? ;-) 98.210.236.39 (talk) 04:33, 23 March 2010 (UTC)

Other

I've just removed this statement from the "limitations" section - //Gödel's theorems only apply to consistent theories. In first-order logic, because of the principle of explosion, an inconsistent theory T proves every formula in its language, including formulas that claim T is consistent.// - on the understanding that such a system would by definition be complete (containing every true statement) but not consistent (containing false statements). Is this right? I'm a little amateurish when it comes to set theory. Noaqiyeum (talk) 16:59, 26 March 2010 (UTC)

To be honest, I'm not quite sure what you're getting at, but the original text also was poorly worded, so I don't mind its removal.

You're right that an inconsistent T is negation-complete, in the sense that it proves every sentence or its negation (in this case, actually every sentence and its negation) but I'm not sure why you see that as refuting the text you removed. The problem with the text you removed is that the theorems do "apply" to all theories. For example, the second theorem says, if T is a consistent theory satisfying the other stipulations, then T does not prove that T is consistent. That is true for an inconsistent T, even though an inconsistent T does prove its own consistency. The reason is that the statement starts with if T is consistent, which is false, and "if p then q" is always true when p is false. --Trovatore (talk) 17:34, 26 March 2010 (UTC)

I think the issue is what "apply" means. I would say that a an offer "if your name is Joe, you can go to Panama for free" is a free offer that only applies to people whose name is Joe. Sure, the offer could be formally interpreted as applying to all people, but only actually giving anything to someone named Joe; that is not how I think most people would interpret it. In this article, you could add "the conclusion of the incompleteness theorems only holds for consistent theories..." but I think it's overkill. — Carl (CBM · talk) 19:51, 26 March 2010 (UTC)

Yeah, but this is not very robust. One way to phrase 2nd incompleteness is "if T proves Con(T) then T is inconsistent". That is true for inconsistent T. --Trovatore (talk) 20:21, 26 March 2010 (UTC)