Talk:Gödel's incompleteness theorems

This is the talk page for discussing improvements to the Gödel's incompleteness theorems article. Please place discussions on the underlying mathematical issues on the Arguments page. Non-editorial comments on this talk page may be removed by other editors.
Please sign and date your posts by typing four tildes (~~~~). Put new text under old text. Click here to start a new topic. New to Wikipedia? Welcome! Ask questions, get answers. This is not a forum for general discussion about the article's subject.	Be polite Assume good faith No personal attacks Be welcoming	Article policies No original research Neutral point of view Verifiability
Archives: Index, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11

history section

Re discussion of a history section per Wvbailey, above: I like the idea of a history section, but I've always thought of Gödel's incompleteness theorems as representing the end of a historical period rather than the beginning of one. Consider van Heijenoort's book "From Frege to Gödel" ending where it does, for example. I'd guess the history section could speak briefly about the development of formalized math (Frege to Principia), then discuss some antecedents to Gödel's theorems (e.g. Thue's (hmm, or Dehn's?) work on the word problems for semigroups and groups (I'm not sure what the stories are with these); Post's independent semi-discovery of diagonalization), then talk a bit about the Hilbert program, mention Gödel's correspondence with Herbrand, mention Gödel's presenting the first incompletness theorem at Königsberg(?) and his meeting with von Neumann there, von Neumann independently discovering the second incompleteness theorem but being scooped by Gödel a second time, and von Neumann's seminar about the incompleteness theorems back at the Hilbert school.

I think after the incompleteness theorems, things changed completely, and not much remains to be said in this article. Most things that do come to mind are already mentioned: Rosser's theorem, Gentzen's consistency proof, the (negative) solution of the Entscheidungsproblem, the essential undecidability of Robinson arithmetic, and Chaitin's version of the incompleteness theorem. I guess something could be said of the fate of Part II of Gödel's paper (which was never written), e.g. that the second incompleteness theorem was generally accepted right away even though a fully-worked-out proof didn't come til later, and that Turing (ordinal logic) and Feferman (iterated reflection) pursued the idea of iterating the consistency statement into the transfinite, and found that you can't actually beat the first incompleteness theorem that way. 66.127.55.192 (talk) 07:41, 16 February 2010 (UTC)

---

The above is interesting and I'm unfamiliar with some of it (e.g. the semigroup stuff). Here's my thoughts on the matter up to the mid-1960's, where my knowledge sputters to a halt. For the following the fundamental secondary source is Davis 2000, but there are corroborating sections to be found in Dawson 1997 ("Logical Dilemmas"), in the commentary of van Heijenoort 1967, and commentary of Davis 1965 ("The Undecidable"), in Hodge's biography of Turing (Hodges 1983).

The trick is to tie all of this together into a coherent narrative string: "this happened, then this happened, then this happened . . . voila! Goedel's Incompleteness theorems.

Where exactly the notion of "metamathematics" derives from is unclear. Is it the Vienna Circle discussions? Goedel's take on what happened to Hilbert's "program" (as published in Dial.) would be interesting to read; see the 1937 entry, an addendum to his 1934 Princeton Lectures.

• 1888, 1889 -- Dedekind and Peano axiomitize arithmetic
• 1890's -- Hilbert's successful axiomatization of geometry (proof of the consistency of geometry? cf Davis 200:116) encouraged his personal belief that all of mathematics could be axiomized and then proven complete;
• 1900-- he announces his 2nd problem, but no one quite knows what it means for 20 years (cf Davis:115)
• late 1890's-early 1900's --The discovery of the antinomies in Frege and Cantor -- in response theoreticians split into factions -- set theorists (Zermelo et. al.), Formalists (Hilbert et. al.), the Logicists (Whitehead-Russell); "constructivists/intuitionists" (Weyl, Poincare, Brouwer); cf Dawson 1997:48-49 and footnote 5 p.49.
• 1910-1925: The collapse of the Logicistic program -- Russell finally abandones his theory of types and axiom of reducibility in the 2nd edition of Principia (ca 1925; it's there, in the introduction, Russell throws down the towel.)
• 1920 -- Post's PhD thesis proves the propositional calculus is complete; the notion of derivability (provability) versus "truth" is changing (cf good discussion in Dawson:51)
• 1923ff -- Hilbert is beset upon by Brouwer and in response modifies his "program"-- the problem of finitism in his proof theory which Hilbert "never defined precisely"(Dawson 1997:50), Brouwer's rejection of completed infinity and the LoEM; Hilbert's student Weyl defects to the Brouwer camp: (e.g. cf Davis 100:114).
• 1924 -- Goedel attends university in Vienna, he changes his studies from physics to mathematics (cf Davis 2000:110)
• 1926-: At the encouragement of his teacher Hans Hahn, student Goedel attends the Vienna Circle discussions. Here the attendees discuss Wittgenstein and PM (cf Davis 2000:111); Goedel rejects their empiricism and finitistic leanings. He is introduced to the notion of metamathematics (by inference: cf Davis 2000:111).
• 1926: Finsler's Formal proofs and undecidability (cf van Heijenoort 1967:438ff). Via diagonalization he presents a proposition known to be false but formally undecidable; Goedel claims not to have read the paper or heard of Finsler. Finsler argues against Goedel's 1931 to the end of Finsler's life. (papers to be found in Dawson's compilation of Goedel's nachlass).
• 1925-1926, 1927 [? multiple papers and addresses -- 1925 "On the Infinite" van H:367ff, 1927 "The Foundations of Mathematics" van H:464ff; cf Dawson:48]. Hilbert presents his finitistic "proof program" (cf Dawson:49) for his "restricted functional calculus" (no quantifiers, choice functions instead, cf Dawson:50) in particular his 1927 address (cf van Heijenoort:464ff, with Bernays Appendix van H:485ff, and Brouwer's rebuttal cf van H:490).
• 1928: Hilbert persists in his quest for a completness proof of arithmetic; he (Hilbert and company e.g. Bernays, Ackermann) define better what his 2nd problem entails -- Hilbert's address at [Bologna?] where he precisely addresses the questions of (1) completeness of mathematics, (2) consistency of mathematics, (3) decidability of mathematics. (cf Hodges 1983:91).
• 1928- Hilbert-Ackermann's text questions whether or not 1st-order predicate calculus is complete [Davis:111, Dawson:52]
• 1930: Student Goedel succeeds in answering the Hilbert-Ackermann question. His PhD thesis proves the Completeness Proof for first order predicate calculus. (Davis claims Goedel rejects the finitistic philosophy promulgated by the Vienna Circle and this allows him "room to maneuver" in particular w.r.t. his Completeness Proof of 1930, cf Davis 2000:110, 114-115).
• 1930-1931: Goedel is now equipped with Hilbert's restricted "system" (Peano arithmetic axioms + PM's axioms of logic + (primitive-)recursion theory, cf van H's commentary p. 592-593). He shifts the question from the notion of "truth" and "falsehood" to that of "provability" (cf commentary van H:138). 1930: Hahn presents Goedel's summary paper of his incompletness results, August 1930 he appears at the Konigsberg conference day 3 he shyly presents his findings: 1931 his "On Formally Undecidable Propositions" is published (Davis 2000:122-123 gives a vivid account of this).
• 1931ff- "So, at least as originally imagined, Hilbert's program was dead!" (Davis 2000:120). Hilbert was angry (I'll have to hunt for this quote), but still persistent. But Goedel's proof is quickly accepted; Von Neumann realizes its import right off. (Davis 2000:122-123).
• 1934- Goedel visits Princeton and presents his lectures that simplify his 1931 paper, plus he proposes the notion of "general" (Herbrand-Goedel-etc recursion), in response to the discovery of the Ackermann function. He rejects Church's "thesis" that the lambda-definability is equivalent to "effective calculability"; he is less skeptical about "Herbrand's definition of recursiveness" (cf Dawson 1997:99).
• 1936- Church uses both lambda-calculus and recursion to answer Hilbert's "decision problem" in the negative: mathematics is not "decidable". In a different manner, Turing will also answer this same question in his 1937.
• 1937- Rosser eliminates Goedel's need for omega-consistency (cf Rosser's paper in Davis 1965:231-235, and Goedel's 1964 commentary in Davis 1965:73) where he also observes "the proof carries over almost literally to any system containing, among its axioms and rules of inference, the axioms and rules of inference of number theory. As to the consequences for Hilbert's program see my paper in Dial. 12(1958), p. 280 and the material cited there. See also: G. Kreisel, Dial. 12(1958), p. 346" (ibid p. 73).
• 1937- Turing's proof is published.
• 1952- Kleene formally presents the notion of "metamathematics" in his text, together with what has become classical (mu-)recursion
• 1963- Goedel accepts Turing's work as the only "precise and unquestionably adequate definition of formal system" (cf van Heijenoort:616 in particular footnote 70).
• 1964- Goedel again accepts only Turing's work as a definition of formal system, and this time he overtly rejects the lambda calculus and his own "general recursion" (cf Postscriptum in The Undecidable -- Davis 1965:71-73, in particular first starred footnote on p. 72).

Bill Wvbailey (talk) 18:23, 16 February 2010 (UTC)

Do we have an article Timeline of mathematical logic? Does Wikipedia have timelines at all? I think that the content you just wrote would be very nice as an article, unless there is some outright prohibition on timelines. It would be a good link from the article on mathematical logic as well as this article. — Carl (CBM · talk) 19:09, 16 February 2010 (UTC)

Since it seems we do indeed have a timeline article, even though I can't find a policy about them: do you mind if I copy your material there and add the references to the bottom? — Carl (CBM · talk) 19:16, 16 February 2010 (UTC)

Please do. The stuff I used is from the following sources:

• Jean van Heijenoort, 1967, From Frege to Gödel: A Source Book in Mathematical Logic, 1979-1931, 3rd printing 1976, Harvard University Press, Cambridge, MA, ISBN 0-674-32449-8 (pbk.). Here are found the papers of Finsler, Post, Gödel, etc.
• Andrew Hodges, 1983, Alan Turing: The Enigma, Sikmon and Schuster, NY, ISBN 0-671-49207-1
• Martin Davis, 2000, Engings of Logic: Mathematicians and the Origin of the Computer, W. W. Norton & Company, NY, ISBN 0-393-32229-7 pbk.
• John W. Dawson, Jr, 1997, Logical Dilemmas: The Life and Work of Kurt Gödel, A K Peters, Wellesly, MA, ISBN: 1-56881-256-1
• Alfred North Whitehead and Bertrand Russell, Principia Mathematica To *56: Second Edition 1927 reprinted 1962, Cambridge at the University Press, Cambridge UK. No ISBN. With respect to his abandoment of the axiom of reducibility, see "Introduction to the Second Edition" page xiii, and especially the last section, VII Mathematical Induction pages xliii-xlv.
• John W. Dawson, Jr [Here my research fails; the books were missing from the library and I got this off the internet somehow]. This is from one of Dawson's volumes of Goedel's works re Finsler -- commentary by Dawson starts at page 406-407. "In his letter to Yossuf Balas (see page 9 of this volume) Gödel attested that he was unaware of Finsler's paper at the time he wortoe his own 1931. But when Finsler brought the paper to his attention he immediately recognized its shortcomings . . . Finsler reacted angrily to Gödel's letter, and his subsequent papers, particularly 1944, reveal a persistent inability to understand the issues involved. Like Gödel he was a stauch Platonist,; unlike Gödel, however, he failed to appreciate the value of formalization and never grasped the fundamental distinction between use and mention that is central to the modern conception of logic." (page 406). Various letters appear 407ff.

BillWvbailey (talk) 20:52, 16 February 2010 (UTC)

(edit conflict) I think most of the timeline above isn't really relevant to the history of the incompleteness theorems (at least for a short treatment like an article section). I guess we could mention Finsler. I'd forgotten about that but sort of remember that there wasn't much to it. Of course the timeline relevant to more general history of logic and using material from it in another article is good. For the Thue and Dehn stuff, see:

• Word problem for groups
• Word problem for semigroups

Here are a couple of interesting articles about Post: [1][2]

RE length: I dunno . . . depends on the reader's background that they bring to the article. It seems too much for this article; it would have to be pruned. Carl's suggestion to put it into a timeline and then have the article reference the timeline might be a way out.

RE Post: I'll dig into your references. Here is something interesting that follows after the above quote from Dawson's Gödel volumes (page 407 of volume ??) that says: "For another putative anticipation of Gödel's incompleteness discovery see Post 1994, as well as Post's correspondence with Gödel in volume V." I'm familiar with Post's crazy "Absolutely Unsolvable Problems and Relatively Undecidable Propositions: Account of an Anticipation" (rejected 1941, published finally in Davis 1965:340) but this paper has to do with Post's claim to anticipating Church's 1936 An unsolvable problem of elementary number theory, not anticipating Gödel's work. So Post claiming to anticipate Goedel is news to me.

RE Finsler: Dawson's discovery of the Finsler-Goedel correspondence etc is the best stuff. But there's an interesting chapter by Herbert Breger titled "A restoration that failed: Paul Finsler's theory of Sets" in: Donald Gillies, editor, 1992, Revolutions in Mathematics, Clarendon Press, Oxford UK 1992, ISBN 0-19-853940-1 (hardback). It goes into a lot of detail about Finsler's "extreme Platonism" with some commentary about Goedel etc on page 257. BillWvbailey (talk) 20:52, 16 February 2010 (UTC)

I can't seem to find an online copy of "Emil Post and His Anticipation of Gödel and Turing", by John Stillwell, Mathematics Magazine, Vol. 77, No. 1 (Feb., 2004), pp. 3-14 (from talk:Emil Leon Post). If you can access it, maybe it would have something. It's best to not spend much space on this Post/Finsler stuff though. It's enough to just mention it and include a wikilink. Re the timeline: it's interesting and important stuff about the history of logic in general, and we should certainly use it someplace. It's just that this article is on the narrower subject of one particular pair of theorems. 66.127.55.192 (talk) 21:07, 16 February 2010 (UTC)

I wish my brain was big enough to read J-Y Girard. He divided 20th-century logic into 3 periods (Locus Solum, p. 4 [3]):

• 1900-1930, the time of illusions: Naive foundational programs, like Hilbert's refuted by Gödel's theorem
• 1930-1970, the time of codings: Consistency proofs, monstrous ordinal notations, ad hoc codings, a sort of voluntary bureaucratic self-punishment
• 1970-2000, the time of categories: [basically what I think of as a computer science-y approach to logic].

So the first of these periods was delimited by Principia at one end and the incompleteness theorems at the other. But, perhaps we can't really call Girard a mainstream source about that sort of question ;) 66.127.55.192 (talk) 19:25, 16 February 2010 (UTC)

• This article by Hao Wang might be useful, though perhaps its contents are also in Wang's 1997 book already mentioned in the article references. 66.127.55.192 (talk) 23:19, 17 February 2010 (UTC)

• Ivor Grattan-Guinness, The Search for Mathematical Roots 1870-1940: Logics, Set Theories, and the Foundations of Mathematics from Cantor through Russell to Gödel. Princeton Univ. Press. ISBN 0-691-05858-X. -- looks promising. 66.127.55.192 (talk) 10:13, 18 February 2010 (UTC)

• Dawson, John W. Jr. (1984). "The Reception of Godel's Incompleteness Theorems". Proceedings of the Biennial Meeting of the Philosophy of Science Association, Vol. 1984,. Vol. Volume Two: Symposia and Invited Papers. The University of Chicago Press on behalf of the Philosophy of Science Association. pp. 253–271. JSTOR 192508. {{cite conference}}: |volume= has extra text (help); Unknown parameter |booktitle= ignored (|book-title= suggested) (help)

I am sorry for repeating myself--- but you are not right about Hilbert being naive--- Hilbert's program was not refuted by Godel's theorem, just the admittedly naive implementation of it by some of Hilbert's followers.

Hilbert wanted to prove the consistency of infinitary systems like set theory using "finitary" (meaning symbol manipulation) means. Godel's theorem does not preclude doing this, but it does show that the method of "finitary" proof will have to involve large countable ordinals and computation. Gentzen implemented Hilbert's program in a satisfactory way for PA, and others have extended this to ordinal analysis of higher theories (as I am sure you know--- I just wanted to emphasize how modern Hilbert's thinking was. It is important to read Hilbert himself, not what people say about him).

Other than the slight to Hilbert, I agree with your timeline. I don't understand what "categories" has to do with anything, though. Do you mean category theory categories? What does that have to do with foundations? Do you mean topoi? I don't get it.Likebox (talk) 04:23, 18 February 2010 (UTC)

It's not my timeline; it's by Jean-Yves Girard, a brilliant and important but rather idiosyncratic logician, a lot of whose writings seem like far-out science fiction. Yes, category theory categories. He gave a longer explanation that I didn't bother typing, but you can look at the pdf I linked. Re categories: I don't think he means anything like topos theory. He means the Curry-Howard correspondence as analyzed from the 1960's exposed a relationship between logic and categories. He is not disrespectful of Hilbert. He says Hilbert had a beautiful idea that was unattainable. He does repeatedly disrespect Tarski, for reasons I don't quite comprehend. (edited) 66.127.55.192 (talk) 10:04, 18 February 2010 (UTC)

Sorry I haven't responded promptly. You've uncovered lots of interesting sources that I've haven't had a chance to investigate. I'm disappeared somewhere in the White Mountains; I'll be back to it in a few days. BillWvbailey (talk) 22:21, 18 February 2010 (UTC)

---

RE whatever happened to the follow-up paper ("Part II") that Goedel expected to publish but didn't and why not: The following comes from a paper by Feferman (and harks back to Dawson's biography):

"⁷Part II of Gödel (1931) never appeared. Also promised for it was a full proof of the

second incompleteness theorem, the idea for which was only indicated in Part I. He later explained that since the second incompleteness theorem had been readily accepted there was no need to publish a complete proof. Actually, the impact of Gödel’s work was not so rapid as this suggests; the only one who immediately grasped the first incompleteness theorem was John von Neumann, who then went on to see for himself that the second incompleteness theorem must hold. Others were much slower to absorb the significance of Gödel’s results (cf. Dawson 1997, pp. 72-75.) The first detailed proof of the second incompleteness theorem for a system Z equivalent to PA appeared in Hilbert and Bernays (1939)." (page from http://math.stanford.edu/~feferman/impact.pdf.

BillWvbailey (talk) 01:30, 23 February 2010 (UTC)

History -- Stephen C. Kleene in Feferman et. al.

I got a cc of Feferman et. al. (editors), 1986, Kurt Gõdel: Collected Works, Volume I, Oxford University Press, Oxford and New York, ISBN 13: 978-0-195-14720-9. On pages 126-128 Kleene presents a condensed history of what led up to Goedel's taking on his proofs (mostly re Hilbert's "program"). This is followed by a 7-part description of the proofs (not trivial, not easy for a layman), and then a very interesting discussion of Hilbert's notion of "finitary proof" and some history in this regard, on pages 138-141. The history abbreviates (but agrees with) what I wrote in the timeline. I'll write a precis here when I have a bit more time. What I'd recommend is anyone interested in the history pursue Kleene's treatment (pages 126-141) of this book and also Grattain-Guiness as noted by our mystery editor above (the Vienna Circle + the encouragement of Hans Hahn are very important elements in this story). Bill Wvbailey (talk) 16:04, 27 February 2010 (UTC)

It might be good to use some of that in the article about the Hilbert program. I don't think it's worth mucking with intricate legalistic analysis of what a finitary proof is or what Hilbert thought it was. The point to remember is that Hilbert himself wasn't a finitist and neither was his opponent Brouwer. Hilbert wanted a minimal foundational system not because he needed to be convinced by it, but in order to quiet anyone else's objections to the infinitary math that Hilbert liked (Cantorian set theory, classical logic). Brouwer didn't go for set theory or classical logic, but I believe he accepted what we now call Heyting arithmetic even though it is infinitary. So Hilbert didn't much care what the outer boundary of finitism was, as long as he was well inside its parameters. Simpson's article that CBM linked someplace explains that pretty well. 75.62.109.146 (talk) 08:13, 28 February 2010 (UTC)

Here's the promised precis of the beginning pages (126-127) of Kleene's commentary before Goedel's 1931 in Feferman et. al. 1986, Kurt Goedel Collected Works Volume I Publications 1929-1936:

In his 1918 and 1921, [does he mean his 1923 “proof theory” paper and his address of 1925 published 1926 per Dawso:49?] David Hilbert addressed the paradoxes that arose in Cantorian set theory [and Frege’s logical system] with a two-part proposal. First, a suitable portion of mathematics should be formalized into a system (call it S) such that deductions “consist simply of mechanical manipulations of the formal objects, with no reliance on their meanings”; second, this formal system S requires proof to be “(simply) consistent, i.e. that no two sequences of its formulas exist of which one is a proof in S of a formula A and the other its negation ~A.” This formal system would become “a new branch of mathematics (to be called “proof theory” or “metamathematics”). Investigations in Hilbert’s “program” “called for using only the most secure methods . . . usually translated as “finitary””.

After he finished his 1929 doctoral dissertation "The completeness of the calculus of logic" Goedel set himself proving Hilbert's challenge -- to prove the consistency of analysis "pursuant to Hilbert's program). (Kleene's commentary preceding Goedel's 1931 in Feferman et. al. 1986:126-129)

There is more to come. BillWvbailey (talk) 22:43, 3 March 2010 (UTC)

Timeline of more-immediate events surrounding Goedel's incompleteness theorems

Not to panic -- this is meant for reference/guidance and not for publishing "as is". With the exception of Tarski, all the major players make their appearance -- Hilbert, von Neummann, Bernays, Zermelo, Finsler, Kleene & Rosser, Post. The following is derived from Dawson 1997 (biography of Goedel) Chapter IV “Moment of Impact” (1929-1931). Some of Grattain-Guiness is derived from this (cf parenthetic note to 9.2.3 in Grattain-Guiness 2000:509), as are parts of Davis 2000 (for example see sources in the footnotes for his chapter 6 “Goedel Upsets the Applecart” on pages 224-233). In turn, Dawson along with Davis and Grattain-Guiness are relying heavily on the assembled papers by Feferman, Kleene, et. al. in ‘’Kurt Goedel Collected Works Volume I Publications 1929-1936’’. Bill Wvbailey (talk) 15:57, 6 March 2010 (UTC)

G-G is an abbreviation for Grattain-Guiness:2000 The search for Mathematical Roots 1870-1940. Bill Wvbailey (talk) 16:09, 8 March 2010 (UTC). Davis 2000 is his Engines of Logic. Bill Wvbailey (talk) 18:28, 8 March 2010 (UTC)

Influences leading to Goedel's incompleteness results

• 1928 - International Congress in Bologna Italy, Hilbert delivers an address that both outlines his "proof theory" and defends it against the assult of Brouwer. With regards to Hilbert's second problem, Ackermann and von Neumann seemed to be making progress toward the "finitary consistency proof for PA" [Davis 2000:116. Hilbert's system is Peano Arithmetic fortified with a set of logical axioms derived from Principia Mathematica and what is now known as primitive recursion: the use of substitution and modus ponens with a limited induction axiom]. However, it will turn out that the restrictions placed on their "system" render the Ackermann-von Neumann proof inadquate to encompass all of PA.

• 1928-1030 - in Vienna, Brouwer lectures on intuitionism, argues for "languagelessness clearly, and near the end he distinguished a notion of 'correct theories', in which the law of excluded middle iwas forbidden as opposed to 'non-contradictory' theories where it was allowed. "Both Carnap and Goedel were impressed by the pessimistic idea that there might be unsolvable problems in mathematics (Koehler 1991a, drawing upon Carnap's diary)" (G-G:504)

• 1926-1930 - Hahn invites his young student Goedel to the Vienna Circle as organized by Schlick its founder; in 1924 " . . . a group of philosphers and scientists continuing in the empriricist-positivist tradition of Mach and Helmholz. Of relevance, this group also included Carnap (Davis 2000:110. Davis observes that Carnap studied under Frege, was a "leading figure in the philosophical tendancy called logical positivism.). (cf a concise history of this invitation-only gathering in G-G 2000:507-508 and his section 8.9 The Rise of Austria in the 1920s: The Schlick Circle. (G-G:497). Carnap would contribute by mail (G-G:507). "Positivism and reductionism were held to govern both epistemology and ontology, and metaphysics was disliked; father figures included Mach and espeically Russell, and Wittgenstein's Tractatus exercised both positive and negative influence (G-G:498; Davis 2000:111 observes that both the work of both Russell and Wittgenstein were discussed in these meetings, and he opines that while Russell's logicism and Wittgenstein's "emphasis on the problems of speaking about language from within language" must have influenced Goedel, "he found himself out of symapathy with much of what he heard" (Davis:111)).

• 1930- Carnap's rejecting "metaphysics". G-G opines that while he rejected the metaphysics of Hegel and Heidegger and his "repulsion is understandable", his own "stance [is] an opposite stupidity which came to weaken VC philosophy (G-G:514).

• 6 July 1929: Goedel’s dissertation (On Completeness of the Calculus of Logic) -- the topic derived from an unproven thesis as mentioned as such in the text of Hilbert/Ackermann (cf G-G:504) -- is formally approved. Dawson opines that “Goedel had already begun to think along the lines of his incompletness discovery

• 22 October 1929: revision of Goedel’s dissertation is received, but it will be a year (on 19 September 1930) before it is published (Dawson:60).

• 6 February 1930: Goedel is granted his PhD. But he cannot work as an unpaided “dozent”, let alone earn money as a lecturer, until he publishes his ‘’Habilitationsschrift’’, i.e. another major paper. 1930: So Goedel sets out to prove a positive solution to the second of Hilbert’s problems – “giving a finitary consistency proof for the axioms of analysis”; his goal being to prove Hilbert ‘’correct’’ (Dawson:63). Davis:118 opines that Goedel was able to transcend the mindset of the Vienna Circle that biased it against any kind of mathematical proof other than provability; rather, "unencumbered by such beliefs, Goedel was led to the remarkable conclusion that on the contrary, no only is there a meaningful notion of mathematical truth, but also its extent goes beyond what can be proved in any given formal system" (Davis:118). In other words, there are true propostions expressible in the system that cannot be proved in the system (Davis:118); this is perhaps a reflection of his Platonistic outlook that he claimed to hold such views since at least 1925 (cf Dawson:100). Dawson opines that Goedel disagreed with both Hilbert’s “naïvely optimistic belief in the limitless efficacy of formal methods” and with Brouwer’s contempt for the very idea of formalization (Dawson:55). G-G opines that "Apparently Goedel found his theorem when he repesented each real number by an arithmetical proposition φ(x) and found that, while 'φ(x) is provable' could also be so treated, 'φ(x) is true' landed him in liar and naming paradoxes (Wang 1996a, 81-85: Hao Wang 1996 A Logical Journey. From Goedel to Philosophy, MIT Press, Cambridge MA). Maybe because of Viennese empiricist doubts over truth, he recast the paradox in terms of unprovability and 'correct' (' richtig ') propositions . . .. (G-G:509).

• ca 1930: Goldstine (another biographer of Goedel) reports (in conversation with von Neumann) that von Neumann was, at the same time, working on Hilbert’s second problem, but he had not recognized the critical “truth-versus-provable” issue that Goedel did recognize (Dawson:71).

Immediate events surrounding Goedel’s incompleteness results

• 26 August 1930: While at a café Goedel announces to Carnap, Feigel and Waismann (all 4 will be attendees at the upcoming Konigsberg conference the next week) that he has obtained the first of his incompletness theorems (Dawson:68).

• 29 August 1930: At the same café Goedel discusses his discoveries further with Carnap (Dawson:68).

The four journey with Hahn and Grelling to Konigsberg (Dawson:68).

• 5-7 September 1930: The conferences in Konigsberg: three societies hold their conferences jointly: (1) Conference on Epistomology of the Exact Sciences (organized by a Berlin Society allied with the Vienna Circle), (2) 91st annual meeting of the Society of German Scientists and Physicians, and (3) 6th Assembly of German Physicists and Mathematicians (Dawson:68-69).

• (conference 1) 5-September 1930 (Friday): 1-hour addresses by Carnap, Heyting, and von Neumann re the three mathematical philosophies (logicism, intuitionism, formalism respectively) (Dawson:69).

• (conference 2) 6-September 1930 (Saturday): Hilbert delivers the opening address to the Society of German Scientists and Physicians where he announces: “The true reason why [no one] has succeeded in finding an unsolvable problem is, in my opinion, that there is no unsolvable problem.” Dawson assert that Goedel was likely in the audience (Dawson:71). Goedel would never meet Hilbert face-to-face (Dawson:72).

• (conference 1) 6-September 1930, 3 PM to 3:20 PM (Saturday): Goedel’s 20 minute “contributed talk” (not about incompleteness; this would come the next day) (Dawson:69).

• (conference 1) 7-September 1930 (late in the discussion, Sunday): Roundtable discussion of Friday’s addresses. Godel, “without warning and almost offhandedly, quietly announced that some propositions while true are unprovable in the formal system of classical mathematics” (Dawson:69).

Transcript by recorder Reichenbach shows no follow-up discussion of Goedel’s announcement nor even of Goedel’s attendance (Dawson:69).

von Neumann may have been the only one to grasp the significance, he apparently draws Godel aside for discussion (cf Dawson:69).

• 16 October 1930: Carnap records Goedel’s refutation of Behmann’s claim that “every existence proof could be made constructive”. His counterexample is similar to one of Brouwer’s. (footnote 9 Dawson:73). But G-G:521 asserts that "Goedel clarified that he had not refuted Behmann but had shown that unrestricted type theory would generate paradoxes independently of the forms of nominal definitions".

• 23 October 1930: Goedel submits an abstract of his paper (“Some metamathematical results on completeness and consistency” cf ‘’Collected Works Volume 1’’ pp. 140-143) to the Vienna Academy of Sciences (Dawson:70).

• 17 November: the editors of Monatshefte fur Mathematic und Physic receive the full paper (Dawson:70).

Unexpected competition (von Neumann)

• 20 November: von Neumann writes Goedel to announce that he had discovered “that in a consistent system any effective proof of the unprovability of 0=1 could itself be transformed into a contradiction”; Godel’s response has not been located. (Dawson:70).

• 29 November: von Neumann writes Goedel to thank him for the preprint. “von Neumann was not accustomed to being anticipated, and the tone of his second letter . . . conveys his disappointment” (Dawson:70). von Neumann soon curtails his own research efforts in logic; he remains a friend of Goedel throughout their lives (Dawson:70); see 1932 below.

General confusions, and a suggestion from Herbrand to enhance the notion of recursion

• ca early 1931: Paul Bernays on behalf of Hilbert writes to thank Goedel for a reprint of his paper, he requests galley prints (Dawson:70, also footnote 6).

• December 1930: Hilbert delivers a talk that will become his 1931a, b (see below) introduces the “ω-rule” (footnotes 7, 8 Dawson:72-73); Goedel et al consider this to be contrary to Hilbert’s “basic principles (Dawson:73)

• 15 January 1931: Goedel speaks before the Schlick [aka Vienna] Circle [cf a long discussion of Carnap's and Behmann's work at this time in G-G:513-523]. Hahn (Goedel's mentor/thesis advisor), Felix Kaufmann and Schlick express their confusions and misunderstandings. Goedel quotes Brouwer’s belief that no formal system could comprise all intuitionistic mathematics (Dawson:73); see 16 October 1930.

• 18 January 1931: Bernays thanks Goedel for the galleys. “So at that point, if not before, Hilbert must have become aware of what Goedel had done” (Dawson:72). Constance Reid, Hilbert’s biographer, reports that Bernays told her that Hilbert was angry. Bernays asks for clarification of points in Goedel’s proof; Dawson opines that Bernays found the proofs “difficult to assimulate”; Bernays would write also on 20 April, and 3 May; he is confused by an earlier finite consistency proof of Ackermann and von Neumann, one whose “restricted applicability is difficult to understand” (Dawson:73)

• 7 February 1931: Bernays meets with Goedel, confesses his work “hard to understand” (Dawson:73)

?? 1931a, 1931b: Hilbert “dealt with [the consequences of the incompleteness theorems] in a positive way”; however, neither paper cites Goedel’s work (Dawson:72-73).

• 25 March 1931: 100 cc’s of the incompleteness paper is sent to Goedel; he sends two to Bernays. Bernays passes the galley prints to Herbrand (Dawson:74).

• 7 April 1931: Herbrand sends Goedel off-prints of his own work, comments about implications of the incompleteness theorems, suggests a more-general recursion schema (Dawson:74). Goedel would take up this matter and present Herbrand’s suggested “general recursion” in the Princeton lectures of 1934.

• 25 July 1931: Goedel responds to Herbrand, but Herbrand is killed in a mountaineering accident the day the letter arrives. Goedel states that he is not convinced that the second incompleteness theorem “contradict[s] Hilbert’s formalistic viewpoint” (Dawson 74:75).

A strong detractor (Zermelo) and a priority challenge (Finsler)

• 15 September 1931: Goedel’s talk encounters Zermelo “his first and most vocal detractor . . . a very irascible person” (Dawson:76).

• 21 September 1931 -- writes Goedel to announce that he has found “an essential gap in Goedel’s argument” (Dawson:76).

• September 1931 -- the Bad Elster lectures: Zermelo The Deutsche Mathematiker-Vereinigung holds its annual meeting in Bad Elster (G-G:512), with Zermelo and Goedel presenting papers. Zermelo rejects the notion of "finitude in proof" and presents his theory of infinitely long proofs (containing "infinite con- and disjunctions") and "especially the message of the lecture 'On the existence of undecidable arithmetical theorems in formal systems of mathematics' that was given by Goedel.

• 12 October 1931: Goedel replies to Zermelo with a 10-page letter and hopes that now Zermelo will be convinced of his proofs. (Dawson:75, G-G:512-513 gives a detailed account

• 29 October 1931: Zermelo continues to misunderstand and publishes his criticisms in print (see below). Goedel “no doubt thought it pointless to pursue the matter any further.” Carnap agrees with Goedel that Zermelo completely misunderstands. (Dawson:76)

• 1932 - Zermelo writes up his lectures at Bad Elster for publishing and incluudes a "rather scathing paragraph on his young competitor" (G-G:513) G-G opines that Zermelo's work did not gain much attention nor traction in infinitary logics after WWII. (ibid).

• 1932 – von Neumann lectures in Princeton NJ about Goedel’s results; student Stephen C. Kleene first hears of Goedel (Dawson:70-71).

• 25 June 1932 – Goedel presents his paper as his Habilitationsschrift (Dawson:81).

• 3 December 1932 – Goedel is granted his post-doctoral “doctorate” “Dr. habil.” (Dawson:87).

• 11 February 1933 – Finsler, citing his 1926, challenges Goedel’s priority re the incompleteness results (Dawson:89).

• 25 March 1933 – Goedel bluntly points out where Finsler’s proof fails (Goedel would state that he was unaware of Finsler’s paper and it “contain[ed such] obvious nonsense” (Dawson:89).

• ca June-July 1933 – Finsler studies Goedel’s offprints, “retorts angrily”. Goedel does not reply (Dawson:90). (Commentary by Dawson and letters etc to be found in Volume ?? of Goedel's Collected Works).

Aftermath -- After proposing Herbrand's more-general recursion, Goedel exists recursion theory

• Fall 1933, 1934 – Princeton NJ: Alonzo Church is concerned that “the incompletness theorems were somehow dependent on the particularities of formalization”, Goedel seeks to dispel this notion in his lectures (a refined version of his consistency proofs) as transcribed by students Kleene and Rosser (cf Dawson:101). At the end of the lectures Goedel also proposes “general recursion” as suggested by Herbrand. Goedel suggests this, rather than Church’s lambda-calculus, as a foundation necessary to prove undecidability (cf Dawson:101). Goedel exits further work in recursion theory (Dawson:102).

• 1936 – Rosser’s paper demonstrates that simple consistency rather than ω-consistency is adequate to demonstrate incompleteness of a formal theory (Dawson:112).

• October 1938 – Goedel is in New York, meets Emil Post who “had also come close to obtaining the incompletness theorems” (Dawson:130); Post outpours his ideas, and his heart, to Goedel of his “anticipation” but without malice acknowledges Goedel’s achievement (Dawson:131).

• 1939 – a full proof of the second incompleteness theorem is published in Hilbert and Bernays 1939 (cf footnote 6 Dawson:70).

• ? 1950’s – posthumous Wittgenstein's ‘’Remarks on the Foundations of Mathematics’’ seems to “betray a particularly glaring lack of comprehension’’ (Dawson:77 with caveat in reference. This caveat appears as footnote 179 on page 283 that in turn references Juliet Floyd 1995 On Saying What You Really Want to Say: Wittgenstein, Goedel, and the Trisection of the Angle. In Jaakko Hintikka, ed., From Dedekind to Goedel: Essays on the Development of the Foundations of Mathematics 373-425. Boston and Dordrecht:Kluwer.).

According to 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)]. —Preceding unsigned comment added by 98.210.236.39 (talk) 19:04, 8 March 2010 (UTC)

Wow! BillWvbailey (talk) 04:37, 15 March 2010 (UTC) What I meant to say is I'm really impressed with this research. Bill Wvbailey (talk) 04:39, 15 March 2010 (UTC)

• April 1963 – Bertrand Russell admits that he finds Goedel’s work puzzling (Dawson:77).

Why Goedel and not Skolem or the team of Hilbert-Ackermann-Bernays?

• 7 December 1967: In a letter to Hao Wang Goedel concluded that the failure to discover the completeness theorem (i.e. the theorem of his doctoral thesis) was indeed surprising. Davis opines that "there was little novelty in his methods, all perfecctly well known to logicians at the time". But Davis goes on to apply this failure more widely than to the specific completeness theorem:

"The completeness theorem is indeed an almost trivial consequence of [Skolem 1923b]. . . . This blindness . . . . of logicians is indeed surprising. But I think the explanation is not hard to find. It lies in a widespread lack, at that time, of the required epistemological attitude toward metamathematics and toward non-finitary reasoning . . . . [The easy] reference from [Skolem 1923b] is definitely non-finitary, and so is any other completeness proof for the predicate calculus. Therefore these things escaped notice or were disregarded" (Davis:115 quotes the italicized phrase and in footnote 6 references Dawson:58, who in turn references Hao Wang in a letter from 7 Dec 1967).

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" ([4] specifically [5]). 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:

• [6] (Stephen Simpson) - proof via the diagonal lemma
• [7] (Itay Ben-Yaacov) - proof via recursive inseparability
• [8] (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)

"Incompleteness theorems" redirects here?

The topic incompleteness theorems currently redirects to this article, which, unfortunately is missing a large part of the story. How can this be remedied? 68.65.169.201 (talk) 21:57, 12 April 2010 (UTC)

That depends greatly on exactly which material you're concerned about. — Carl (CBM · talk) 00:56, 13 April 2010 (UTC)

There would seem to be several considerations:

• assumptions used in incompleteness proofs
• whether incompleteness entails inconsistency
• role of metatheory in proofs of incompleteness
• etc.

64.9.240.145 (talk) 03:02, 14 April 2010 (UTC)

Could you explain what you have in mind for the third one? The article certainly already discusses the assumptions of the theorems, and the answer to "does incompleteness entail inconsistency" is "no", since the whole point of the theorems is that consistent theories with certain properties must be incomplete. — Carl (CBM · talk) 03:06, 14 April 2010 (UTC)

It's as those you have never heard of the work of Wittgenstein, Routely, Priest, etc. I know that Wikipedia hates Hewitt, but Incompletness Theorems has a concise overview. What do you think?68.65.169.149 (talk) 23:57, 15 April 2010 (UTC)

I don't believe it's accurate to say anyone here hates Hewitt. I have always advocated including, not removing, a link to his paper on paraconsistent logic. Recently, some collection of West-coast IP addresses added a very poorly written "proof sketch" to the article, which anyone could tell was not going to fit in. But the reference to Hewitt's paper is still in the article as I write this.

I do think this article could use a "history" section, which could mention Wittgenstein's remarks and the near-universal opinion that they are not of the same acuteness as Wittgenstein's other writings. I recently looked at the new book An Introduction to Goedel's theorems by Peter Smith, the philosopher at Cambridge. This is a 360pp book on the theorems that is quite comprehensive; I was unable to find a mention of Wittgenstein in it. In mathematical logic references, Wittgenstein is essentially never mentioned. So Wikipedia is far from the only place that does not emphasize Wittgenstein in its coverage of the incompleteness theorems. — Carl (CBM · talk) 03:12, 16 April 2010 (UTC)

There are two prominent points of view on the matter:

• In the box: The traditional one of Hilbert, Gödel, Peter Smith etc.
• Out of the box: Starting with Wittgenstein [1930] through his later writings along with Routley, Priest, etc.

You are firmly stuck in the POV "in the box" and completely deny the existence of the POV "out of the box."17.244.70.121 (talk) 15:55, 16 April 2010 (UTC)

From time to time I ask myself whether the article really covers enough. I didn't write most of it, although I fixed some issues. But when I actually look at what's in the article, it seems pretty reasonable for a general-level encyclopedia article. I can think of some topics that could be covered in more depth (e.g. inexhaustibility and formalization), and the "discussion" section could use work, but all the major topics are included in the article as it stands. — Carl (CBM · talk) 03:28, 14 April 2010 (UTC)

It may not be such a terrible article on "Gödel's incompleteness theorems" with the emphasis on Gödel. But current article is not adequate for the topic of Incompleteness theorems in general.68.65.169.149 (talk) 00:06, 16 April 2010 (UTC)

Could you point me to an printed reference for "incompleteness theorems" in general? I can think of Smullyan's book on self-reference as one possibility, but I doubt that that is what you have in mind. — Carl (CBM · talk) 03:12, 16 April 2010 (UTC)

You might try reading the following from 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)].

In addition there are many other published papers on the POV "out of the box."17.244.70.121 (talk) 15:55, 16 April 2010 (UTC)

Also see April 23, 2010: Carl Hewitt: Wittgenstein versus Gödel on the Foundations of Logic (Cordura 100 from 12:00 to 1:30:

This talk (in four parts) explains how some of the writings of Ludwig Wittgenstein can be interpreted as precursors of important developments in the foundations of mathematical logic for information systems applications. Wittgenstein's writings stand in almost exact opposition to the views of Kurt Gödel.

• FIRST PART: The current state of foundations of mathematical logic for information systems applications is overviewed with regard to issues of expressiblity, incompleteness, and inconsistency tolerance.
• SECOND PART: The above developments have precursors in writings of Wittgenstein.
• THIRD PART: The above views are contrasted with the almost opposite ones of Gödel.
• FOURTH PART: How do the above views provide framework and guidance for the further development of logic for information systems applications?

FURTHER READING: Common sense for concurrency and inconsistency tolerance using Direct Logic ArXiv:0812.4852

17.244.70.121 (talk) 15:55, 16 April 2010 (UTC)

Above material mysteriously disappeared. But I found a way to bring it back so I could comment that the following quotes by Wittgenstein are relevant:

• Let us suppose I prove the unprovability (in Russell'ssystem) of P [where P is 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. Does it do any harm here?

• Indeed, even at this stage, I predict a time when there will be mathematical investigations of calculi containing contradictions, and people will actually be proud of having emancipated themselves from consistency.

With respect to the necessary elements required before incompleteness can be demonstrated for a "system", Goedel listed 5 criteria:

• (1) The system is "formal: and it is constructive ["... a rule's being constructive, that is, of there existing a "finite procedure" for carring out the rule" cf Davis's commentary in his The Undecidable 1965:39]. With the exception of constructive he defines the notion of formal system elegantly in two paragraphs at the outset of his 1934 Princeton lectures (cf Martin Davis 1965:41 and 61-62). To satisfy the notion of constructive he offers us his [primitive] recursion. Note in particular Goedel is specifying provability in his formal system, not "truth".
• (2) The formal system permits forming the positive integers into "meaningful formulas z_n" for the positive integers, i.e. expressions such as the Goedelization from his 1934 (this is different than his 1931, here the star represents arithmetic multiplication. At this point the "formula" has passed from a concatenation of symbols to its encoding into a number):

0 => 1, 1 => N(0) => 2²*3¹²*5¹*7¹³, 2 => N(N(0)) => 2²*3¹²*5²*7¹²*11¹*13¹³*17¹³, . . .

• (3) The formal system contains the symbol ~ (NOT) and two symbols v and w for variables, such that the relation with their numerals (defined in (2) i.e. for v => z_p and w => z_q and R(z_p, z_q)) is provable if the relation R(v, w) is provable, and that the relation ~R(zp, zq) is provable when the relation of R(v, w) is not provable.
• (4) The formal system contains the symbol Π with its meaning to be the logical product of the form ΠxF(x)( i.e. for for all positive integers x, x satisfies F(x) ). If this is provable then the formula F(z_k) must be provable for all positive integers k (here again z_k is the numeral that represents the positive integer k).
• (5) The formal system is "free of contradiction" -- he defines this in terms of the expressions in (3) and (4).

Later he goes on to state the well-known observation that "There is no algorithm for deciding relations in which both + and x occur." This derives from his proof that "There exists no formalized theory that answers all Diophatine questions of the form (P)[F=0)". (cf pages 69 and 72 in Davis: 1965).

I haven't thought through what a minimal formal system would look like that satisfies the above 5 stipulations. Clearly it needs at least a few symbols: 0, s (successor), ~, Π, x, y. This seems close to the minimal symbol- and instruction- set that a register machine would embody: 0, increment x, jump-if-equal x, y, jump-if-not-equal x, y; x is a register, y is a register. There must be someone out there who's noodled this out in detail. Bill Wvbailey (talk) 14:43, 16 April 2010 (UTC)

You are stuck hacking in the weeds. All you need is roundtripping.17.244.70.121 (talk) 15:55, 16 April 2010 (UTC)

For those who are unfamiliar, roundtripping proposition P is that ⌊⌈P⌉⌋ ⇔ P, i.e. P is logically equivalent to abstraction of reification of P.98.210.236.39 (talk) 12:58, 17 April 2010 (UTC)

It seems tht it is Arthur Rubin who has been deleting material from this discussion.99.29.247.230 (talk) 20:53, 17 April 2010 (UTC)