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

This page is an archive of past discussions. Do not edit the contents of this page. If you wish to start a new discussion or revive an old one, please do so on the current talk page.

Recursion sucx?

By computer science jargon, the theorem says: Recursion sucx!. But we knew that! Said: Rursus ☻ 10:59, 4 August 2008 (UTC)

A criticism of this article (from Usenet)

The following criticism of this article was posted on Usenet. The last edit made by Aatu was apparently on 15 July 2005.

 From: Chris Menzel <...@...>
 Newsgroups: sci.logic,sci.math
 Subject: Re: the problem with Cantor
 Date: Mon, 11 Aug 2008 17:49:38 +0000 (UTC)

 On Mon, 11 Aug 2008 09:05:20 -0700 (PDT), MoeBlee <...@...>
 said:
 > ...
 > My point stands: Wikipedia is LOUSY as a BASIS for study of this
 > subject....

 There are some good articles, of course, but a big problem is that the
 entries are a moving target because of Wikipedia's more or less open
 revisability policy.  Case in point, a few years ago Aatu did a very
 nice job of cleaning up the first few sections of the terrible entry on
 Gödel's incompleteness theorems.  But a number of the problems in the
 article that Aatu had fixed seem to have been reinstroduced.  The
 current statement of the first theorem is now both wordy and inaccurate
 (notably, the statement of the theorem in the first sentence doesn't
 rule out the possibility of a complete but unsound theory).  The article
 also includes both incompleteness theorems as stated in Gödel's original
 paper which, taken out of context, are utterly opaque to the ordinary
 reader.  Aatu's informative section on Gentzen's theorem has been elided
 in favor of a link to an article written, apparently, by someone else.
 And, bizarrely, there is now a paragraph mentioning an extension of the
 first theorem to "a particular paraconsistent logic" -- as if that is
 essential information.

 It appears to me that someone has simply taken on the mantle of Owner
 and Guardian of the article and is vigorously monitoring and
 "correcting" its content.  This could work if the person in question
 were a genuine expert, but the O&G in this case, unfortunately, appears
 to be only marginally competent.  This sort of thing really does make
 Wikipedia a terribly unreliable and unsystematic source of information.

207.172.220.155 (talk) 07:22, 12 August 2008 (UTC)

If Aatu or Menzel would like to help write the article, they would be very welcome. In the meantime, their criticism will be considered when the article is edited.

I tend to agree that Goedel's original statement shouldn't be included. The remainder of the complaint seems to be more personal preferences - to include a longer discussion of Gentzen's result in this article, not to include the one sentence on Hewitt's result.

It's hard to see what Menzel means by "The current statement of the first theorem is now both wordy and inaccurate (notably, the statement of the theorem in the first sentence doesn't rule out the possibility of a complete but unsound theory" - the statement explicitly says the theory must be consistent. Moreover, it's hard to see how to make the statement much shorter. — Carl (CBM · talk) 11:31, 12 August 2008 (UTC)

I think the point about the "complete but unsound" part is that the current statement doesn't exclude the following situation: There is a true statement that the theory doesn't prove, because the theory proves, rather, the (false) negation of the statement. This is a fair point; the theorem does exclude that situation, and we don't currently say that it does. I don't think it's extremely important to the foundational impact of the theorem (who wants to found mathematics on a theory that proves falsehoods?) but it is strictly speaking part of the theorem.

Most of the discussion around this point has been objections to calling the sentence true, which stem mostly from misunderstandings (you can certainly take the view that the sentence doesn't have a truth value, but it's hard to see then how you would assign a truth value to the hypotheses). This is an entirely different point and I'm not entirely sure how to respond to it. It would be nice to keep the point that the sentence is true, precisely as a counter to the muddled presentations by the popularizers. --Trovatore (talk) 17:36, 12 August 2008 (UTC)

What do you make of the sentence "That is, any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete."? It may be that the "that is" is not quite the right choice of words, since the quoted sentence is strictly speaking stronger than the one before it. But the quoted sentence does seem to exclude the possibility that the theory is complete... Maybe we can come up with a better overall phrasing of the theorem; that would be a positive outcome to this discussion. — Carl (CBM · talk) 01:54, 13 August 2008 (UTC)

Hmm, maybe. Maybe just drop "that is" and append the sentence? --Trovatore (talk) 02:17, 14 August 2008 (UTC)

I'd refer Mr. Menzel (assuming he deigns to read Wikipedia at all) to WP:SOFIXIT.Zero sharp (talk) 15:00, 12 August 2008 (UTC)

> Please remember folks: this article is not for academic mathematicians -- you folks already know this stuff -- it's for the rest of humanity. (Carl: you and I have been around the original-statement issue once before, I believe. Forgive me while I repeat myself ...). I inserted Goedel's original statements of his theorems only because I when came to this article as a novice in search of some illumination, I found, as I compared his paper (in The Undecidable), that "the first and second" incompleteness theorems are anything but. I had to actually (sort of) read the paper as best as I could to even figure out which theorems are the supposed "first and second theorems". Maybe common academic parlance calls them this, but I want the article to clarify the fact that for someone confronting the papers, they will need to understand that the paper consists of a sequence of theorems after a rather clear but extremely terse presentation of axioms and then a lengthy and scary sequence of definitions with frightening names. (But not so scary and frightening once they've been explained ....) The theorems' opaqueness is illuminating; their original wording and their subtlety does serve as a caution to the newbie/novice that there's a lot going on here. Perhaps as stated by Goedel the theorms could appear in footnotes -- footnotes can contain expansion material, not just references. I'll reiterate that it continues to drive me (a non-academic) and others nuts (see Talk:Busy beaver ) that the really important mathematics wikipedia articles seem to be written by academics and grad students writing mostly for themselves, at their level of understanding, and they are writing for no one else. As far as I'm concerned most of the value in this article as it is currently written is to be found in the references and my clarification that if you go hunting in the original for a "first" and a "second" incompleteness theorem you're going to be disappointed. The whole article could be about 40 words: "This stuff is hard. You will need some background knowledge. For a good introduction read Nagel and Newman's book. Everybody else: read the original as presented best in van Heijenoort. The meanings of the strange (to-english) abbreviations can be found in Meltzer and Braithewhite" Bill Wvbailey (talk) 17:27, 12 August 2008 (UTC)

Will, are you seriously arguing that the most approachable presentation for non-academics is one written in Gödel's original notation??? --Trovatore (talk) 02:19, 14 August 2008 (UTC)

No, of course not . . . an example of Goedel's (awesomely-difficult) original notation is simply a sampler of the true "taste" of the paper (not unlike like the taste of a very difficult Scotch whiskey (e.g. Lagavulin) . . . wow! whew!). For those who don't have a cc of the original paper, the original notation represents a (cautionary, challenging, fun) taste/flavor of what the original contains. And that is the point! That's part of the "educational experience"! With regards to a superb explication in Wikipedia I propose that really talented editor/s (you, Carl, etc) can craft a presentation that a kid in US high-school senior math could grab. That's a hell of a challenge, I realize ... but I think after a careful presentation of the notion of "Peano axioms" and "[primitive] recursion" and "Goedel numbering" and "diagonalization" such an explication is possible. Bill Wvbailey (talk) 02:56, 14 August 2008 (UTC)

A qualification to the above: My experience with difficult subjects is that, more often than not, the author's original explication/presentation is the best, but it needs to be supplemented with a modern, simplifying 'trot' -- an "Illustrated Classics" and/or a "Cliff's Notes". But this idea is complicated by the fact that Goedel evolved a simpler presentation. His IAS (Princeton 1934) lectures modified, and simplified, his proofs for his English-speaking audience. (For example he reduces his 46 definitions to 17, removes the scary German abbreviations, and actually defines what the 17 mean, he changes his Goedelization method, etc) There's still a lot of spooky symbols and the typography in The Undecidable is off-putting, but here Goedel quickly and clearly defines a "formal system", the notion of "completeness", expands the relationship of his proof to the Epimenides (Liar) paradox, etc. Eventually (in his June 3, 1964 "Postscriptum" to the IAS lectures) he embraced the "Turing machine": "Turing's work gives an analysis of the concept of "mechanical procedure" (alias "algorithm" or "computationa procedure" or "finite combinatorial procedure"). This concept is shown to be equivalent with that of a "Turing machine". A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas. . . . Moreover, the two incompletness results mentioned . . . can now be proved in the definitive form . . . 'There is no algorithm for deciding relations in which both + and x occur'" (p. 72). It would be very interesting to see how, in 2008, Goedel would present, and explain, his proofs. Bill Wvbailey (talk) 11:46, 14 August 2008 (UTC)

I rearranged the statement of the first theorem, which removed the "that is" and made it more clear which statement is more general. I'm planning to work on the article in a little more detail over the next couple days. — Carl (CBM · talk) 12:55, 18 August 2008 (UTC)

A very simple paraconsistent proof

There is a very simple paraconsistent proof in:

http://hewitt-seminars.blogspot.com/2008/04/common-sense-for-concurrency-and-strong.html

--67.180.248.94 (talk) 06:05, 14 August 2008 (UTC)

I removed the Hewitt paraconsistency stuff from the article on the grounds that it is cited to a non-peer-reviewed source and that Carl Hewitt is banned from inserting references to his own work on Wikipedia. It was probably inserted by Hewitt. See further discussion at:

76.197.56.242 (talk) 02:44, 17 August 2008 (UTC)

Poking around the Web, it turns out that the results were published in a refereed journal:

Hewitt, Carl (2008). "Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency". Coordination, Organizations, Institutions, and Norms in Agent Systems III. {{cite web}}: External link in |work= (help) Jaime Sichman, Pablo Noriega, Julian Padget and Sascha Ossowski (ed.). Springer-Verlag.

--67.169.145.52 (talk) 03:30, 17 August 2008 (UTC)

That looks like a conference proceedings, not a refereed journal. See the comments at the "Direct logic" AfD linked above for discussion of this point as applied to this topic.

Unfortunately, you are incorrect, it is was refereed.--98.97.104.6 (talk) 18:51, 17 August 2008 (UTC)

Even if it's in a journal, the linked article appears to have no relevance to Gödel's incompleteness theorems, which are theorems of classical logic.

Unfortunately, you are incorrect. Incompleteness theorems also apply to non-classical logics.--98.97.104.6 (talk) 18:51, 17 August 2008 (UTC)

It also appears to have very limited notability in that Google Scholar finds no citations to it of any sort. If some appear in the future, we can consider it for Wikipedia after that happens.

Unfortunately, Google Scholar tends to be both spotty and tardy in its indexing. Consequently, it doesn't indicate much of anything in academic work. On the other hand, the regular Google index has lots of references to the work.--98.97.104.6 (talk) 18:51, 17 August 2008 (UTC)

So, based on both verifiability and WP:Undue weight, I don't think the reference should be restored. 76.197.56.242 (talk) 07:32, 17 August 2008 (UTC)

The paper has become quite famous. The results have been presented in lectures at AAMAS'07, Edinburgh, Stanford (on at least 3 occasions), AAAI (twice), and no doubt others.--98.97.104.6 (talk) 18:51, 17 August 2008 (UTC)

My general opinion is that the proof warrants a very short exposition here - shorter than what was removed. Since the goal is only to give a pointer to the paper, not explain it at all, it's OK if we leave the text here somewhat vague. — Carl (CBM · talk) 12:53, 18 August 2008 (UTC)

Yes, shorter is better. What was removed is the following:

Recent work by Carl Hewitt^[1] extends Gödel's argument to show that, in a particular paraconsistent logic (that is outside the restrictions on self-reference of Gödel's framework^[2]), sufficiently strong paraconsistent theories are able to prove their own Gödel sentences, and are thus inconsistent about the provability of the Gödel sentence (as well as being incomplete). Here incomplete means that it is paraconsistently provable that neither the Gödel sentence nor its negation can be proved. In this context, questions about the truth of the Gödel sentence do not make any sense.

The key points seem to be the following:

A very short intuitive paraconsistent formal proof of both incompleteness and inconsistency for this kind of reflective logic.
The thesis that the whole notion of "truth" is out the window for reflective logic of the kind envisioned by Feferman.

Would like to try your hand at drafting something shorter?

--12.155.21.10 (talk) 14:44, 18 August 2008 (UTC)

Yes, I'll do that later, along with the section on Boolos' proof. — Carl (CBM · talk) 14:58, 18 August 2008 (UTC)

I added a very short summary. I'm sure the wording can be improved, but I don't think more detail is necessary. — Carl (CBM · talk) 16:46, 20 August 2008 (UTC)

This is a good contribution. However, this business about the Godel sentence being "true" is still a bit mysterious. The article states:

for every theory T satisfying the hypotheses, it is a theorem of Peano Arithmetic that Con(T)→G_T

where Con(T) is the natural formalization of the claim "T is consistent", and G_T is the Gödel sentence for T.

Consider the theory PA+Con that is Peano Artithmetic + the axiom Con(PA+Con) that PA+Con is consistent. Then, from the above,

it is a theorem of Peano Arithmetic that Con(PA+Con)→G_PA+Con

therefore since PA+Con is an extension of PA:

it is a theorem of PA+Con that Con(PA+Con)→G_PA+Con"

Now, since Con(PA+Con) is an axiom of PA+Con, it kind of looks like PA+Con can prove its own Gödel sentence.--216.1.176.121 (talk) 21:56, 20 August 2008 (UTC)

Writing T for your PA+Con, you seem to want to make Con(T) an axiom of T. How are you going to do that, exactly? In the usual way of treating these things, you don't know what Con(T) is until you've already fixed T, so you can't really make it an axiom of T. --Trovatore (talk) 02:23, 21 August 2008 (UTC)

Con(PA+Con) says that an inconsistency cannot be derived in PA+Con even using the proposition that PA+Con is consistent. So PA+Con is fixed.--12.155.21.10 (talk) 15:49, 21 August 2008 (UTC)

Your use of "Con" is confusing me. Starting with PA, we may form G_PA. Let's say R is the theory PA + G_PA. This theory does not include the axiom G_R. If you did somehow construct a theory which did include its own Gödel sentence, that would mean you had constructed an inconsistent theory. But that won't be the particular theory R.

It may be easier to see why PA proves Con(T) → G_T if you look at it in contrapositive form: if G_T fails, that means Bew(G_T) holds, so we want to prove Bew(G_T) implies ~Con(T). This is exactly what is obtained by formalizing the proof of the incompleteness theorem in PA, replacing "provable" with Bew throughout. — Carl (CBM · talk) 16:34, 21 August 2008 (UTC)

Since "it is a theorem of PA+Con that Con(PA+Con)→G_PA+Con" and "Con(PA+Con) is an axiom of PA+Con", PA+Con proves its own Gödel sentence and is indeed inconsistent.--98.210.236.229 (talk) 23:32, 22 August 2008 (UTC)

As Trovatore and I have pointed out, it's not clear at all what the theory you call "PA + Con" is supposed to be. It certainly isn't PA + G_PA. What is it, exactly? — Carl (CBM · talk) 23:38, 22 August 2008 (UTC)

PA+Con is defined by a fixed point construction in much the same was as the Gödelian sentence. It basically is PA plus the axiom "I am consistent" analogous to G_PA (I am not provable in PA). Thus you are correct that PA+Con is not the same as PA+G_PA --67.169.145.32 (talk) 06:01, 23 August 2008 (UTC)

So it is true that the process of adjoining Con(T) to an r.e. theory T has a fixed point. As an example, just let every sentence in the language of arithmetic be an axiom of T. This is an r.e. theory, and you can formulate Con(T) in some standard way based on the (simple!) algorithm that generates its axioms, and you will find out, in the end, that Con(T) was in fact an axiom of T all along.

But of course this T is inconsistent, and so is every fixed point of the process.

By the way, you can't get to such a fixed point via iteration starting with PA. PA is consistent, and so is PA+Con(PA), and so is PA+Con(PA)+Con(PA+Con(PA)), and so on, through not only all finite iterations, but into the transfinite, as far as you can actually make sense of it. Therefore none of these theories contains its own consistency as an axiom. --Trovatore (talk) 07:34, 23 August 2008 (UTC)

So this is quite interesting:

If a theory T has an axiom that it consistent, then T is inconsistent!

--67.169.9.72 (talk) 22:52, 23 August 2008 (UTC)

Yes. This follows easily from the second incompleteness theorem. --Trovatore (talk) 03:15, 24 August 2008 (UTC)

Con(PA+Con) is intuitively true. But adding it as an axiom classically causes the wheels to come off. So we might as well throw in the towel (i.e. admit the inherent inconsistency) and go over to paraconsistent logic.--67.169.9.72 (talk) 13:05, 24 August 2008 (UTC)

That's one way of looking at it, but certainly not the "standard" one. Apart from Hilbert's program, what's the reason to expect that a formal theory of arithmetic will prove its own consistency? Experience has shown there's no real difficulty for mathematicians if the theories they use to study arithmetic, set theory, etc. don't prove their own consistency, since the consistency can be studied by other means, and the questions studied within the theories are typically mathematical rather than metamathematical. — Carl (CBM · talk) 16:58, 24 August 2008 (UTC)

Look, you can't "add Con(PA+Con)", because there's no such thing as PA+Con. You haven't told us, in any useful way, what it's supposed to be in the first place. There are indeed fixed points of the process of adding a theory's consistency to the theory; I gave an example, but it's not in any reasonable way describable as starting with PA and adding the axiom "I am consistent". --Trovatore (talk) 19:14, 24 August 2008 (UTC)

I reworded the footnote and added references throughout. Please feel free to keep rewording it if I've missed any subtle points. — Carl (CBM · talk) 20:12, 21 August 2008 (UTC)

I think that's nicely done—it's clearer and more direct than my original wording, which was more aimed at being a bulletproof response to the quibblers than at explaining what was really going on. Referencing Torkel is also a nice touch. --Trovatore (talk) 20:17, 21 August 2008 (UTC)

Moved 'implications' section to the end

I moved the section 'Discussion and implications' to the end, after the sections that discuss the proofs, etc. I think that attempts to apply G.I.T. outside of mathematics, mathematical logic and philosophy of mathematics are usually borderline nonsense, but that is my opinion; irrespective of this, they are relevant and notable w.r.t the discussion of the theorems and _do_ belong in this article. But, I think they belong at the end once the more germane (again, this is my opinion (not _just_ mine though) ) topics. Zero sharp (talk) 03:16, 18 August 2008 (UTC)

While we're at it, it would be nice to tighten up the referencing in that section. There are several half-done footnotes that should be replaced by complete references. Does anyone have an interest in that area? — Carl (CBM · talk) 12:52, 18 August 2008 (UTC)

Boolos' short proof

Later today, once I obtain the paper from the library again, I am going to severely trim the section on "Boolos' short proof". When I looked at his paper before, I found Boolos' proof somewhat cute because it uses Berry's paradox instead of the liar paradox, and I think it's worth a mention here.

On the other hand, I don't think that it warrants a long section here - just one paragraph would be fine. The current text is also confused about the proof, possibly because Boolos wrote it up in a short sketch suitable for experts. The current text claims that the proof doesn't mention recursive functions, but does mention algorithms (!); that the proof uses Goedel numbers but assumes no number theory (!); and has other similar problems. A complete exposition of Boolos' proof, which carefully proved all the facts in such a way to make it clear which theories it applies to, would have about the same level of technical detail as any other modern proof of the first incompleteness theorem. — Carl (CBM · talk) 12:43, 18 August 2008 (UTC)

section on meaning of the first incompleteness theorem

I moved this section earlier in the article. It is written in a very accessible, friendly way, unlike our section on the second theorem. I think that the "meaning" section complements the first theorem better, and moving it up will encourage readers not to give up when they reach the sec. on the second theorem (assuming they read an initial segment of the article).

The "meaning" section does need copyediting for tone - it has a lot of "we" and "you". The section on the second incompleteness theorem needs editing for structure - perhaps some subsections. — Carl (CBM · talk) 14:08, 18 August 2008 (UTC)

I also think the section on limitations of Goedel's theorems could be merged into the "meaning" section. — Carl (CBM · talk) 14:12, 18 August 2008 (UTC)

Good work, CBM et al. I think the article is beginning to anticipate and address the difficulties that laymen like me have in trying to understand this work (like Brian Greene manages to do so well in his popular books on physics). --Vibritannia (talk) 16:17, 22 August 2008 (UTC)

Testing the waters

Just checking to see if you folks are Ok with a computational proof now.Likebox (talk) 20:56, 24 September 2008 (UTC)

NO! —Preceding unsigned comment added by 71.139.24.118 (talk) 02:04, 25 September 2008 (UTC)

What has changed since the last time this was discussed? The (long) discussion starts at Talk:Gödel's_incompleteness_theorems/Archive03#New_Proof and continues for the rest of Archive03. There was even an RFC where the "computational proof" was rejected. — Carl (CBM · talk) 21:08, 24 September 2008 (UTC)

That is my recollection as well; Zero sharp (talk) 22:07, 24 September 2008 (UTC)

Error in new proof

The new proof also has problems with correctness, such as:

Write the computer program ROSSER to print its own code into a variable R and look for either 1.R prints to the screen or 2.R does not print to the screen. If ROSSER finds 2, it prints "hello world" to the screen and halts, while if it finds 1, it halts without printing anything.

S can prove neither ROSSER prints to the screen nor the negation ROSSER does not print to the screen. So S is necessarily incomplete.

This does not prove the incompleteness theorem without the assumption that when S proves that "R prints to the screen", this actually means there is a computation in which R prints to the screen. The statement "R prints to the screen" is a Sigma^0_1 statement, and so it is still possible for S to be consistent but not ω-consistent, in which case S may well prove Sigma^0_1 statements such as this without there being any actual natural number that satisfies them. That is, S may prove there is a computation history which ends in R printing to the screen, but it may be that the only such histories are encoded by nonstandard natural numbers. Thus it will be necessary to assume S is ω-consistent in order to actually obtain a contradiction.— Carl (CBM · talk) 21:17, 24 September 2008 (UTC)

As I recall, I thought Ron's proof through here, and it did turn out to be correct, though it required a subtle observation that he didn't bother to mention. I don't remember the details at the moment and don't have time to think about it right now. --Trovatore (talk) 21:22, 24 September 2008 (UTC)

If you're thinking of the argument I think you are, there's not nearly enough explanation there to follow it. That is, you may be thinking that if S proves that R prints something, it means that S proves that (S proves R does not print anything). Also, S will prove (S proves R does print something). Thus S will prove (S proves a contradiction). That leaves an argument to be made that S actually does prove a contradiction, especially since we all know that there are consistent theories that prove Pvbl(0=1). — Carl (CBM · talk) 21:41, 24 September 2008 (UTC)

I think the point was something like, if S proves that R prints, or if it proves that it does not print, then R must in fact halt (because it would find the proof), and S must prove that R halts (because S is strong enough to find all proofs of halting). Therefore S must prove both that R prints and that it doesn't print. Or something like that. --Trovatore (talk) 21:49, 24 September 2008 (UTC)

I'm sorry for being so brusque. My overall concern isn't whether the argument is "fatally flawed" - I'll assume, by way of good faith, that it would be possible to patch together a convincing proof using essentially the method provided, even if the current wording isn't there yet. My first concern is that the text provided is not even clear to people who do have a good understanding of what's going on - so it will be incomprehensible to people who don't already have a good understanding. My second concern is that it seems that the only way to actually draw a contradiction from this type of argument is to be more precise about the arithmetization, and this undercuts the general argument that the "computational proof" is clearer because it avoids arithmetization. My third concern is that, since this argument is not presented in texts, we have nowhere to send people who ask "where can I read a full explanation of this argument"? — Carl (CBM · talk) 22:38, 24 September 2008 (UTC)

I'm certainly not saying that Likebox's proof should be included as is (or even, necessarily, at all). It's true that it really ought to be sourced, and I also agree that Ron is not paying enough attention to the need to connect the result with arithmetic (which after all is where the question comes from).

I do think though that it's kind of a nice way to think about it, once you make your way through the land mines. Here's the completion to the argument. Suppose S proves or refutes the claim that R prints. Then R must in fact halt. When it halts, it is either on a proof from S that R prints or a proof from S that R doesn't print, but then it does the opposite. S is then strong enough to prove that R follows that finite sequence of steps and does that opposite thing. Thus in either case, S proves both that R prints and that it doesn't print. --Trovatore (talk) 00:03, 25 September 2008 (UTC)

Thanks, I see. For some reason when I was reading between the lines earlier I was reading a different proof into it. By the way, I thought we ought to have an article on Rosser's trick. — Carl (CBM · talk) 00:28, 25 September 2008 (UTC)

Look, the reason I put it in is because I am still sure that this is the clearest proof for a young person who knows how to program, but doesn't care about the useless gobbledegook that logicians traditionally surround Godel's theorem with. The reason your complaint is not a mistake is explained by Trovatore, and it is something that must be understood to understand Godel's theorem. An axiom system to which Godel's theorem applies proves what the finite time behavior of a computer program is. It will figure out what the final state is for any algorithm that halts. The reason I am checking again is that I figured that once people figured out I was right, they would change their minds.Likebox (talk) 02:46, 25 September 2008 (UTC)

What you put in wasn't a proof at all - it was a claim that a certain construction could be turned into a proof. Please see my comment of 22:38. — Carl (CBM · talk) 02:51, 25 September 2008 (UTC)

That depends on the reader. It is so straightforward to turn the construction into a proof that I left it up to the reader. The reason I keep harping on this is that we need to really put simple proofs for the simple stuff so that the more complicated stuff gets clear. I don't want to wait a hundred years when we can do it today. If you don't want to help, don't help, but please don't stand in the way.Likebox (talk) 03:11, 25 September 2008 (UTC)

It's not at all "so straightforward" to turn it into a proof, particularly when it's written in a way that obfuscates what's going on (e.g. the switch from "halts" to "prints" only adds complexity, as does the use of the recursion theorem). As has been said before, during the RFC: if you want to change the entire field of recursion theory, you should start by publishing a book, rather than trying to push your views here. Wikipedia follows the lead of professional publications, rather than breaking new ground. — Carl (CBM · talk) 03:36, 25 September 2008 (UTC)

In particular, I would specifically like to see a source provided for any mathematical logic text that proves the incompleteness theorem using the recursion theorem (that is, using programs that begin by using their own source code as the input to some process). — Carl (CBM · talk) 03:56, 25 September 2008 (UTC)

Look, you know very well that you're not going to find a published version which presents this proof verbatim. But you also know very well that it is correct and that it is not original research. It's one of those countless things in that grey area where the results and methods are well known, but nobody has the patience to write up and publish (certainly not me). I am asking you to use your judgement to decide whether the article is improved.Likebox (talk) 04:31, 25 September 2008 (UTC)

My judgment is that the article is not improved; that is also what the RFC said. But I'm not asking you to rely on my judgment. If this isn't original research, it has been published at least "in spirit" somewhere else. Where? I don't know of any published text that thought that this method of proof was the right way to present the incompleteness theorems - and they are a standard topic in mathematical logic texts. — Carl (CBM · talk) 04:35, 25 September 2008 (UTC)

If you follow the argument, you can see that it is logically equivalent to Godel's original article, except that it talks about computers, which didn't exist then. It's also the exact same proof in recursion theory textbooks replacing "Kleene's fixed point theorem" with "print your own code" and replacing "phi of phi of x" with a description of what the code does. Look, I simplified it by removing the nonsense notation and by folding in the proof of the undecidability of halting, but that's it. If you can't accept these minor adjustments, I think that the edits you make to this page are going to be counterproductive.Likebox (talk) 04:42, 25 September 2008 (UTC)

>>These are FAR from "minor adjustments" and I take extreme exception to you characterizing them as such, and characterizing other editors' (particularly CBM's) repeated attemtps to _EXPLAIN_ this to you as 'standing in the way' -- it's arrogance bordering on incivility. Zero sharp (talk) 13:54, 25 September 2008 (UTC)

I am trying to be civil. But I am also trying to convince you folks of something that I understand 100% clearly, and that I don't understand why you don't understand. This is frustrating at times. I am sorry if I was rude.Likebox (talk)

Except that texts in recursion theory don't use the recursion theorem at all in proofs of the incompleteness theorem. They use the fact that the set of provable statements and the set of unprovable statements form a recursively inseparable pair of recursively enumerable sets. Can you point out a recursion theory text that does use the recursion theorem in the discussion of Goedel's theorem? — Carl (CBM · talk) 04:45, 25 September 2008 (UTC)

That's what I mean by "folding in". If you prove theorem A and then prove theorem B using theorem A, then you can fold in theorem A by not using it, and instead using the same method of proof. I am never going to cite any recursion theory text, because they are all sucky.Likebox (talk) 04:49, 25 September 2008 (UTC)

We've been through this before, at the RFC. Wikipedia isn't the place for you to pursue an agenda to change the field of recursion theory... What has changed since the RFC? — Carl (CBM · talk) 04:52, 25 September 2008 (UTC)

What's changed? Nothing. Including a) Likebox engaging in tendentious editing in and b) Carl's unbounded patience in explaining why - for one - the proposed change does not improve the article, not just in his judgement, but in the judgement of other WP editors who participated in the RFC, and - for another - absent any publication, book, webpage, lecture note, cocktail napkin *showing* this use of the recursion theorem, it is Original Research. Period. Likebox, please, there are an uncountable infinity of other venues on the internet to present your work, I think it's been amply demonstrated TIME and TIME again that this article, is NOT the place. Let it go. Zero sharp (talk) 13:50, 25 September 2008 (UTC)

The most important thing that's changed is that almost everyone now understands that the proof is correct. If it fails now, maybe next time you will understand that it is equivalent to Godel's original article.Likebox (talk) 19:27, 25 September 2008 (UTC)

>> " almost everyone now understands that the proof is correct." -- O_RLY? Can you point to one _shred_ of evidence to back up that claim? Zero sharp (talk) 00:07, 26 September 2008 (UTC)

I meant that both Trovatore and CBM now understand that it is correct, as you can see by reading the previous comments. CBM was confused about omega consistency for a little bit (to tell the truth, so was I at first, but then again, so was Godel). They might not agree that it should be included, but that's a different story.Likebox (talk) 05:06, 26 September 2008 (UTC)

This proof is so not original research that if you wrote it up and tried to publish it you would be laughed at! Everyone who understands Godel's theorem has some version of this construction in the back of their heads. I will return to this subject periodically (once a year, so as not to be intrusive) until it is accepted or someone comes up with a better way of writing this article.Likebox (talk) 19:33, 25 September 2008 (UTC)

>> Then why are you unable (or unwilling) to produce ONE SINGLE SOURCE OR REFERENCE for this formulation if it's so pervasive, universal and 'in the back of everyone's head' (sad to say, the back of everyone's head in no way meets criteria for verifiable sources in wikipedia). Zero sharp (talk) 00:07, 26 September 2008 (UTC)

Dude, there is no source, but this is mathematics. None of the proofs that appear on Wikipedia are properly sourced. If they are wrong, people just fix them.Likebox (talk) 05:06, 26 September 2008 (UTC)

3rd Opinon

I am requesting a WP:3O, specifically on Likebox's insistance on his changes to the article, despite repeated attempts by multiple editors to explain to them that, irrespective of their correctness, they are not in place in this article. The technical objections have been amply explained, but clearly this edtior needs to understand how WP is supposed to work regards: consensus, no tendentious editing and civility. Zero sharp (talk) 13:59, 25 September 2008 (UTC)

Actually, I think civility is not an issue here (other than that some effort is needed to stay civil when arguing with Likebox – CBM is spectacularly good at that), and tendentious editing is a bit of a red herring. Let's try to stay focused. --Hans Adler (talk) 14:20, 25 September 2008 (UTC)

I am viewing the problem here as a non-mathematician. This proof is so difficult that I cannot even begin to support use of a confounding alternate proof (or proofs) from e.g. Likebox or anyone else. Since the early 1980's -- when I first became aware of Goedel's proof via The Undecidable -- I've been alternately fascinated, intimidated and challenged by it. It's taken me 20 years to understand its jist, but I still can't reproduce its details. Nagel and Newman's 1958 was mandatory (bought at the same time as The Undecidable -- 1984). Due to the way I learn I like to see original papers. Given the difficulty of Goedels' paper, what I really need is a good "trot" -- a side-by-side description of what's going on (e.g. Goedel on the left page and a description of what's going on on the right). Because of wikipedia's restrictive format this unfortunately is not possible. But recently CBM et. al. made a valiant effort to provide something like this in section 7. To repeat, I just want to see Goedel's proof explained -- not someone else's proof (okay to survey the published alternates, but I'd move to the end). [In that regard I do not agree with some of what was written above re omitting the notion of primitive recursion in the explanation of the proofs. Theorem V appears to be the nut of the whole thing, and Goedel only provided a skeleton-proof of it. And re Rosser's trick to be able to read Rosser's 1936 in the original the reader needs to understand what's going on in Theorem V, IMHO.] Bill Wvbailey (talk) 16:05, 25 September 2008 (UTC)

I am trying to say that if you have patience and think things through, you can see that the one sentence constructions that I gave here are exactly this gloss you are asking for. If you keep the construction in mind, that's all you need to follow Godel's original paper with no further additions. The reason Godel's paper is complicated is that he is constructing a very difficult computer program--- the program which performs logical deductions on a given axiomatic system--- in the language of arithmetic using recursive functions as his programming language. If you know modern computer languages, you can see what is going on immediately, and also that this is going to be impossible for anybody else to follow. It requires many arbitrary choices (arithmetization--- Godel's ascii code, choice of subroutines--- his text manipulation functions, etc).

Once he constructs this program (partially-- he never completes the deduction algorithm in his original paper--- but it is clear he could. He promised a second paper which would complete the proof, but it wasn't necessary; people understood that it could be done), he uses it to construct a sentence which is self contradictory. But he uses a trick there to make the sentence self-referential, a trick which is equivalent to printing your own code.

The logical core of the proof is that given a program which deduces the logical consequences of axioms, there is a simple manipulation which produces a Godel sentence, involving printing your own code. The construction I gave just performs the construction explicitly in the clearest way I could manage, and this involves phrasing the Godel sentence as "Godel does not halt", where Godel is described in the article. It follows Godel's paper exactly, and so reproduces the problem Godel had with omega-consistency. The Rosser construction here takes more liberties with Rosser's method, which was more complicated. Rosser used a slightly more nested construction to come up with a contradiction, but it is essentially the same idea.Likebox (talk) 19:20, 25 September 2008 (UTC)

Proposing a different approach for the computability section

After some reflection last night, I think that a large flaw in the existing computability section is that it is narrowly focused on one proof (the one sourced to Kleene), rather than the broader relationship between computability and incompleteness. So I propose that instead of giving any long proof sketches in that section, we briefly discuss several different ways that computability and incompleteness interact. This version is my first attempt at this. I think that this will be more informative to a reader (who is not assumed to have a background in computability theory) than a more technical discussion would. What do you think? — Carl (CBM · talk) 15:25, 25 September 2008 (UTC)

This is the same road we travelled before. Nobody finished the proof here, and I don't think anyone ever will. It's just too pointless today--- who's going to precisely specify "Bew" (the deduction algorithm) in recursive functions? Why not include a complete proof? Anyone can follow it (despite the claims here), and it is equivalent to Godel's original approach (not quite to Kleene's--- but the rephrasing in terms of computer programs is Kleene's), in modern language.Likebox (talk) 19:24, 25 September 2008 (UTC)

Which proof is it that nobody finished? — Carl (CBM · talk) 20:12, 25 September 2008 (UTC)

Sorry--- I meant "Proof sketch for the first incompleteness theorem".Likebox (talk) 20:39, 25 September 2008 (UTC)

The thing that arguably isn't finished there is just the construction of "Bew" (to explicitly make it you have to work very hard, and to make it obvious that it is possible to make it you need to talk about universal computation in arithmetic, and that gets you back to the computational stuff).Likebox (talk) 20:42, 25 September 2008 (UTC)

On the other hand, to make it obvious that Kleene's T predicate is actually represented by an arithmetical formula, as would be necessary to flesh out the computational proofs, you have to work equally hard. Depending on the specific model of computation, it may still be necessary to formalize enough provability to allow the computations to operate on proofs. The arithmetization is always going to be present in some form or another. — Carl (CBM · talk) 21:01, 25 September 2008 (UTC)

True, but that is so intuitive for a computer person that it requires no explanation, because when you program a computer, most of your education is spent "fleshing out the T-predicate". Not so for logical deduction, which is a specialized industry.Likebox (talk) 21:33, 25 September 2008 (UTC)

I should elaborate because I think you are right in a deeper sense: for every foundational advance in mathematics there is a law of "conservation of hard work". There is no magic--- a new result in mathematics is important when it increases the complexity of mathematical thought, and there is a certain level of calculation complexity that one must work through to understand it. You can rephrase the proof, but you are never going to get reduce the work below a certain level.

But what you can do is construct a general framework of simple results which are well accepted and which turn the initially complicated proof into a triviality. For example, the first proofs of the Jordan curve theorem were difficult, but in a general framework of algebraic topology they become simple (although the hard work is just shuffled into the elemetary theorems). In the case of Godel's theorem, it led to the construction of an elaborate framework in the past 70 years, and this is called "computer science". If you have this framework, the difficulties in Godel's proof all vanish, because clarifying these difficulties gave birth to the field.

But at the same time, a parallel framework called "recursion theory" was constructed by academic logicians, and unlike computer science, this framework does not get everyday use. So it is very unfamiliar to the general public, and theorems and proofs phrased in this framework are obscure. This gives Godel's theorem a bad reputation for difficulty, and unlike other parts of mathematics, it doesn't get any easier with time.

Godel was the first to understand universal computation (he conjectured that general recursive functions were the most general computable functions), maybe not as well as we do today, but he knew this was what the main point of his work was, his most lasting contribution. Now that universal computation is sitting on my desk, it's silly not to use it. Using the language and elementary results of universal computation removes all the difficulties in Godel's proof, and makes it accessible to everybody.Likebox (talk) 21:50, 25 September 2008 (UTC)

Place deleted section here (so others can follow the discussion)

I thought that I found the right wording for the computability section this time (I feel it was much improved compared to last time), so I am placing it here for future reference, and so that others can follow the debate above. I can see that the time is not right for it.

For CBM--- the switch from "halts" to "prints" is unfortunate but necessary, because if you just have one bit (halts or doesn't halt) then you don't get the Rosser contradiction. Rosser managed to get his contradiction by nesting Godel constructions to get two alternatives and then making a sentence which asserts that one of the alternatives is realized. I tried to emphasize the freedom in his construction (he could have used any old property) by making it "prints to the screen". It could have been "sets variable froo to zero" or "calls subroutine Bew twice" (I think that's what Rosser did, I don't remember).Likebox (talk) 20:07, 25 September 2008 (UTC)

Computational formulation

Stephen Cole Kleene (1943) presented a proof of Gödel's incompleteness theorem using basic results of computability theory. A basic result of computability shows that the halting problem is unsolvable: there is no computer program that can correctly determine, given a program P as input, whether P eventually stops running or runs forever.

Suppose for contradiction that there exists a computer program HALT(P) which takes as input the code to an arbitrary program P and correctly returns halts or doesn't halt. Construct a program that print its own code into a variable R, computes HALT(R), and if the answer is halts goes into an infinite loop, while if the answer is doesn't halt halts.

Kleene showed that the existence of a complete effective theory of arithmetic with certain consistency properties would decide the halting problem, and this is a contradiction. If an axiomatic theory of arithmetic can be formulated which proves all true statements about the integers, it would eventually prove all true statements of the form "P does not halt" for all computer programs P. To determine if P halts, run it. While to determine if a computer program does not halt, deduce theorems from the axiomatic theory looking for a proof that P does not halt. If the theory were complete, one of the two method running in parallel would eventually produce the correct answer.

Godel's theorem, following Kleene, can be restated: given a consistent computable axiomatic system S, one which can prove theorems about the memory contents of a Turing machine (a computer with potentially infinite memory), there are true theorems which S cannot prove.

Write the computer program GODEL to print its own code into a variable R, then deduce all consequences of S looking for the theorem R does not halt. If GODEL finds this theorem, it halts.

If S is consistent, GODEL definitely does not halt, because the only way GODEL can halt is if S proves that it doesn't. But if GODEL doesn't halt, that means that S does not prove it.

This is Godel's original method, and it works to show that S has counterintuitive properties. But it does not quite work to show that there is a statement undecidable in S because it is still possible that S could prove GODEL halts without contradiction, even though this statement would necessarily be a lie. If S proves that GODEL halts, the fact that GODEL does not halt is not necessarily a contradiction within S, because S might never prove that GODEL does not halt. An S which proves false theorems of this sort is called sigma-one inconsistent.

Write the computer program ROSSER to print its own code into a variable R and look for either 1.R prints to the screen or 2.R does not print to the screen. If ROSSER finds 2, it prints "hello world" to the screen and halts, while if it finds 1, it halts without printing anything.

S can prove neither ROSSER prints to the screen nor the negation ROSSER does not print to the screen. So S is necessarily incomplete.

This is Rosser's trick, used to get around the limitation in Godel's original proof, and it completed the proof of the usual statement of the first incompleteness theorem. The precise assumptions used in the proof are:

S will eventually prove any theorem of the form "A universal computer running for N steps will take memory state A to memory state B" where N and A are prespecified integers and B is the result of the computation. This is true in any theory which includes the fragment of Peano arithmetic without induction.
S can state theorems about computer programs of the form "Forall N program P running for N steps does not produce a memory state M with the k-th bit zero" and conjunctions and disjunctions of these. These are statements with one quantifier in front.

The second assumption is needed to be able to state theorems of the form "R does not halt" in the language of S, while the first assumption ensures that if a program P halts after N steps leaving memory state M, S will eventually prove this statement.

To prove Godel's second incompleteness theorem, one must be able to formalize the proof of the first incompleteness theorem in S. If this can be done, then S cannot prove itself consistent, since from the assumption that S is consistent, it follows that GODEL does not halt. If S proved itself consistent, it would also prove that GODEL does not halt, which is impossible.

Godel's next major paper: Lengths of proofs

Shortly after Godel proved the incompleteness theorem, he proved another theorem which has a long history. It was published in 1936 with a proof that nobody could really understand, and it was considered of dubious validity for a long time. Credit for the theorem is therefore sometimes given to a much later paper by authors whose name I will not mention, who claimed that they fixed the "gaps" in the proof.

This proof appears in The Undecidable on p. 82. It was translated from "the original ariticle in Ergebnisse eines mathematischen Kolloquiums, Heft 7(1936) pp. 23-24, with the kind permission of the publishers, Franz Deuticke, Vienna" (ibid). This version appears with an added "remark added in proof [of the original German publication]:

"It may also be shown that a function which is computable in one of the systems S_i or even in a system of transfinite type, is already computable in S₁. Thus, the concept "computable" is in a certain definite sense "absolute", while practically all other familiar metamathematical concepts (e.g. provable, definable, etc) depend quite essentially on the system with respect to which they are defined" (p. 83).

Bill Wvbailey (talk) 22:07, 26 September 2008 (UTC)

The paper is extremely short, and it was a little difficult for me to follow because of the usual problems with Godel's work--- he understood computation at a time that nobody else did--- and his notion of computation is entirely tied down to the deduction method in formal logic. The reason I am bringing this up here is to explain how close the proof above is to Godel's original reasoning: if you formulate Godel's argument as above, you can immediately see what Godel was thinking in his next paper.

The theorem has three parts:

1. In any (consistent computer-describing) axiomatic system S, there are theorems of length N characters which have a proof whose length exceeds F(N), where F is any computable function of N.

Given a computable function F, construct NROSSER which prints its own code into the variable R, and looks for all proofs of length less than F(N), where N is the length of R. NROSSER looks for the theorem R does not print, and if it finds it, it prints and halts. Once it finishes running, it halts without printing.

Since S is consistent, NROSSER halts and does not print, and S will eventually prove it, but necessarily with a proof of length greater than F(N).

2. If you increase the strength of S by adding "consis S", the proof of some statements is made shorter by an amount which exceeds any computable function, meaning that for any computable function F, there exists a theorem provable in both systems whose old proof is so long, that it is bigger than F(new proof length).

It is easy to prove from consis S that NROSSER does not print. This is a fixed length proof, depending only on the size of NROSSER, not on the value of N or on F.

(Rosser's trick came later than this paper. I don't remember the exact method in this paper, and whether it implicitly had a Rosser trick when turned into an algorithm. It is possible that Godel discovered a Rosser trick here, but didn't notice. I don't know.)

Godel also claimed

3. If you have any system S' which is computationally stronger than S (meaning there is a program P which S' proves does not halt which S does not) then there are proofs in S' which are shorter by an arbitrary computable function, in the same way as 2.

I convinced myself it could be done, but I forget how.

I remember now--- it's a little tricky. Here's the basic idea-- write program TESTP which runs P for N steps where N is huge, to see if P halts. If TESTP finds that P halts, it prints "halts" and halts. If P did not halt after N steps, TESTP halts without printing anything.

The theorem TESTP doesn't print is provable in both S and S' (since P doesn't halt) but the proof in S' is trivial (of fixed size independent of N) since S' proves that P does not halt. The proof in S, on the other hand, has to follow TESTP until it halts, which means the proof in S is much longer.

The trickiness comes in establishing the precise amount by which the proof in S is longer, and the corresponding problem in Godel was the controversial point of the proof. Godel's method was opaque (at least to me).

The way to do this (somewhat) clearly is as follows: you need to establish that if system S does not prove that P does not halt, then it does not have a uniform length proof that P does not halt after N steps. The proof must get longer as N gets longer.

If you had a function SLength(N) which gives you a lower bound on the length of the shortest proof in S that P does not halt after N steps, and if SLength(N) goes to infinity as N goes to infinity, then the theorem would (almost) be proved. Given Slength(N), write TESTP to run for M steps where M is such that Slength(M)>N.

But to make this work, you need to make sure that the implicit function M(N) which determines M in terms of N as above is computable. Then let TESTP run P for M(N) steps where N is the length of TESTP, as above, and the proof is finished.

Lemma1-- if S does not prove P does not halt, then it does not prove P does not halt after N steps with proof of length less than C characters.

This is not obvious--- I found out it is called "Kreisel's conjecture", and it is open. It seemed obvious to me, because if the proof has constant length then as N gets large the finitely many instances should suffice to prove it on N without extra assumptions, which is what formal logic requires to turn a statement into a (forall N) statement. But it is subtle, because the way to patch the proofs together is not immediate, and there is a paper out there claiming to have examples showing why.

Actually, there is the trivial and nontrivial Kreisel conjecture. The nontriviality in Kreisel's conjecture is that it is stated in terms of proof length, not proof size. Proof length is the number of lines in the proof, the number of applications of the rules of deduction, while the length of the individual proof line can become unbounded, and the axiom schema of induction allows for unbounded axioms to be used. Kreisel's conjecture for proof size is a triviality, but Kreisel's conjecture for proof length is a major problem.

Godel states his speed-up theorem in terms of proof length, but he surely meant proof size, since his claimed proof is a simple version of his original method.Likebox (talk) 02:52, 27 October 2009 (UTC)

The proof of the lemma gives a computable function lower bound for SLength which gives a computable upper bound M(N) which finishes the proof. The reason I separate out the lemma is because this is the only place where you need to muck around with logic, and the rest only requires the computational halting stuff.

I want to say--- this possibly marginally crosses the threshold for what I would call "original research", but it's still just an exegesis on Godel.

That's it. This theorem was controvertial for many decades, but Godel was convinced he understood the proof. I think I understand why he found this theorem so intuitive that he gave it a one-page proof--- it's because the deduction programs in his original proof have property 1 and property 2.

This is why I think that this method is the closest in spirit to Godel's original paper--- it reproduces both his mistakes and his future inspiration.Likebox (talk) 21:51, 26 September 2008 (UTC)

P=NP problem

I put in the example about the P=NP problem because I thought it showed an surprising relationship between undecidability and truth. The idea is to show a few other examples of such relationships:

If Goldbach's conjecture is undecidable, then it is true, since if it were false, it would have a testable counterexample and therefore be decidable.
If the twin prime conjecture is undecidable, it could still be either true or false (there might be a largest prime pair (p,p+2), without having a proof exist that the pair is in fact the largest). We would mostly agree that the twin prime conjecture has a truth value which is unknown. Its undecidability doesn't tell us anything one way or the other.
If the continuum hypothesis is undecidable (as was conjectured by Gödel and later proved by Cohen), a mathematical platonist like Gödel might believe it still has an unknown truth value, but others might say that the question is simply meaningless.
If the P=NP problem is undecidable, then like the twin prime conjecture it still has a truth value which is unknown, but consequence of undecidability is a sharp quantitative bound on how far away from truth it could be. It becomes "almost known" in the sense that P and NP are "almost equal". I felt that this quantitative aspect of the consequences of undecidability was interesting.

Does it sound reasonable to put in a paragraph like the above? 67.117.147.133 (talk) 21:13, 26 October 2008 (UTC)

The thing is that, apart from the continuum hypothesis, none of the others (Goldbach conjecture, twin prime conjecture, P = NP conjecture) is actually known to be independent of anything. On the other hand the continuum hypothesis is undecidable in ZFC. The section in the article is "examples of undecidable statements", and I'm not sold on an "examples of things that might be undecidable". This is especially true with P = NP, since there is no reason to think it should be independent of anything, and some heuristic arguments why it shouldn't be [1] [2] [3]. Of course I am not saying these should be in this article either. — Carl (CBM · talk) 22:50, 26 October 2008 (UTC)

More importantly, there is no reason to think that there are any meaningful undecidable statements at all. Maybe everything is either true and provable (in a strong enough system) or false.Likebox (talk) 23:51, 26 October 2008 (UTC)

Well, that's a very different question, The article does point to philosophy of mathematics for the issue of "absolutely undecidable" statements. But the examples given in the article are all for results that are (at least in some sense) meaningful, and also known to be independent of well-studied systems of foundational interest. (And of course any formula φ that is consistent with ZFC is provable in the "strong enough" system ZFC + φ.) — Carl (CBM · talk) 00:50, 27 October 2008 (UTC)

I agree that statements not known to be undecidable shouldn't be in "examples of undecidable statements"; however, I think examples like the above are worth mentioning in the article, presumably in another section. P=NP is probably decidable based on the general belief that NP-hard problems can't be solved in less than exponential time (a stronger statement than P!=NP) plus the theorem I mentioned, which says that if P=NP is undecidable then NP-hard problems can be solved in time just barely above polynomial (way below exponential). Scott Aaronson has also written a long article[4] that I had cited, about the possible independence of P vs NP. Those FOM posts are interesting, and I believe the result I cited is a sharper version of the argument that Tim Chow described. The stuff by Doria and da Costa is just about certainly incorrect, as Ralf Schindler showed. It is very unlikely (maybe proven impossible) that NP=EXP since EXP contains all of PSPACE. 67.117.147.133 (talk) 03:51, 27 October 2008 (UTC)

My general opinion is that the stuff about P=NP is too specialized for this article, but would be good in Independence (mathematical logic).

I think it drifts too far away from the main topic of this article, which is Goedel's theorem. The section on examples of other undecidable statements is already a side topic, and so material about how the hypothetical independence of P=NP would imply a certain bound in computational complexity theory is another elephant entirely.

I do think that the bullets you have above would be nice to cover. It would also be nice to expand Independence (mathematical logic) to a real article, instead of a stub. That article is explicitly about independent statements, so the material in your bullets is less tangential. We should also link to that article from the examples section here (instead of just to the list of statements undecidable in ZFC - that isn't a very satisfying link). — Carl (CBM · talk) 04:08, 27 October 2008 (UTC)

'There is no algorithm for deciding relations in which both + and x occur'

This quote comes from Dr. Goedel himself (in a 1964 Postscriptum to his simplified treatment of the incompletenes theorems delivered to the IAS in 1934: cf The Undecidable, p. 72). Can someone explain to me why this is true? Since we can define multiplication as a sequence of additions I find this a bit surprising. Is it because the multiplier has to work as an unbounded u-operator? But isn't that true of addition as well? (As I write this I'm thinking about the use of a counter machine algorithm wrt the Collatz Conjecture ). Thanks, Bill Wvbailey (talk) 15:28, 10 May 2009 (UTC)

Although you can define multiplication as repeated addition in the real world, there is no way to express the predicate

M(x,y,z)\equiv x\cdot y=z

in the language with just 0, 1, addition, and equality, using only first-order logic. This is just a limit of the expressiveness of first-order logic; in general there are difficulties expressing inductive definitions in weak languages. The undefinability of graph connectedness in first-order logic in just the language of graphs is a similar problem where there is not enough strength to handle the inductive definition of reachability.

In fact, the theory of the natural numbers with 0, 1, addition, and equality, which is called Presberger arithmetic, is not only effectively axiomatizable, it is decidable, and thus much weaker than the theory of the natural numbers with 0, 1, addition, multiplication, and equality, which is very undecidable. The fundamental difference is that arithmetic with the language with addition and multiplication is able to encode and decode finite sequences of natural numbers in a way that allows them to be quantified, while arithmetic with only addition cannot do that. The ability to quantify over finite sequences then allows all primitive recursive functions to be defined. — Carl (CBM · talk) 22:58, 10 May 2009 (UTC)

I'm trying to noodle this out. I suspect the nut of the problem is this: whether or not logical AND(x,y) and NOT(x) can derived from the available functions and formation rules. Without AND and NOT we cannot "do logic" in our system, and therefore we cannot simulate any arbitrary computational machine (e.g. Turing machine) with our system, and therefore our system cannot “make statements about itself”. Thus x*y gives us AND(x,y) when x, y = {1,0}; we can also get it from NOT(x) = 1 ∸ x, and AND(x,y) = x ∸ NOT(y) where ∸ is proper subtraction. The IF x=y THEN ... ELSE ... construction is another source. Bill Wvbailey (talk) 16:38, 12 May 2009 (UTC)

No, it does not have anything to do with AND and OR; both of these are included in any case. The issue is exactly the problem of quantifying over all finite sequences of natural numbers. If one cannot quantify over sequences, one cannot quantify over execution histories of Turing machines, which are essentially sequences of natural numbers. — Carl (CBM · talk) 02:03, 13 May 2009 (UTC)

I had a feeling this is how you'd respond. Does any viable "system" always include "first order logic"? If so, then it must be buried (i.e. tacit) in simple recursion, and in e.g. counter machines and Turing machines -- there are no AND and OR instructions; AND and OR have to be arrived at by a sequence of instructions which include IF test THEN ELSE and composition. Maybe a place to start would be to give me a definition (or example) of what you mean by "to quantify"? Generalize? Count? Thanks, BillWvbailey (talk) 03:14, 13 May 2009 (UTC)

Yes, all the theories that Goedel's theorem is applied to include first-order logic.

By "quantify" I mean quantify as in quantifier. For example, to define multiplication from addition, one might say this:

n\cdot m=p

if and only if "there is a sequence of natural numbers of length m such that the first number in the sequence is n, each number after the first is obtained by adding n to the previous, and p is the last number in the sequence"

The difficulty here is that m is a parameter, which can vary, but the formula that expresses the sentence in quotes would have to have a fixed number of universal and existential number quantifiers independent of m. Thus there is a need for quantifiers that range over finite sequences of natural numbers, along with machinery in the first-order language to manipulate sequences (encode, decode, and check their length). — Carl (CBM · talk) 03:27, 13 May 2009 (UTC)

This helps. Methinks I've conflated "Goedel systems" with Turing- and counter-machines and recursion (recursion being merely a component of a "Goedel system" . . . correct?). Will have to go away and mull. Thanks, Bill Wvbailey (talk) 03:55, 13 May 2009 (UTC)

"Illumination provided by Principia Mathematica "

" === Illumination provided by Principia Mathematica ==="

- In the preface to volume 1 of the Principia Mathematica, it is stated how a very large part of the labour of writing the work was expended on the contradictions that had plagued logic and the theory of aggregates. - After examining a great number of hypotheses for dealing with the contradictions, it gradually became evident to the authors that some form of the doctrine of types had to be adopted if the contradictons were to be avoided. - They chose a particular form of doctrine of types that seemed to them most probable while noting that there were other forms equally compatible with the truth of their deductions. - They then said it should be observed that the whole effect of the doctrine of types is negative: it forbids certain inferences which would otherwise be valid, but does not permit any that would otherwise be invalid, which meant the inferences that the doctrine of types permits would remain valid even if the doctrine of types were ever found to be invalid. - - We can see now, in hindsight, how a question had been raised. - Earlier in the preface, the authors had affirmed that the ideas and axioms with which they had started were sufficient to prove "as much as is true in whatever would ordinarily be taken for granted." - But if the doctrine of types forbade certain inferences which would otherwise be valid, had it been implied that, now, there were truths as-yet-unidentified to which no sequence of inferences would lead?

Could someone explain to me what this section has to do with the incompleteness theorems? — Carl (CBM · talk) 10:37, 12 May 2009 (UTC)

As written, not much that I can see. It's true that Goedel invoked PM as his core and then adjoined the Peano axioms "merely to simplify the proof and [they are] dispensible in principle" (van H:p.599 footnote 16). But I don't quite see what PM's restriction about "types" has to do with it other than to introduce the notion and serve as an unacceptable solution to a knotty problem. It is true that the intro to PM did "illuminate" (itemize, discuss) the paradoxes. What seems to me far more important historically was the challenge thrown down by Hilbert's 2nd problem and his subsequent clarifications in the 1920's, and then the attempts on one hand of Hilbert and Bernays to axiomatize mathematics against an increasingly-strong counter-current surrounding impredicativity, and then Finsler's 1926 (which everybody seems to forget) which as van H notes ". . . presents an example of a proposition that, although false, is formally undecidable. Finsler establishes the undecidability by suitiably modifying the argument used by Richard in stating his famous paradox . . ." (van H: 438ff). While commentators argue that Finsler's proof failed, he did succeed in presenting a formally undecidable proposition. And it's clear from his method (use of the diagonal argument) that there was plenty of activity in this area that has little to do with PM's known flaws. (Goedel says in letters that he wasn't aware of Finsler's work at the time, and subsequently he thought Finsler was a putz). Then there was Goedel's 1930 "Proof of the completeness of the axioms of the functional calculus of logic", shortly followed by his 1931. It seems clear to me that this new section should be condensed into a piece of a history section re what led up to the incompleteness theorems. Bill Wvbailey (talk) 15:24, 12 May 2009 (UTC)

I forgot also the development of "primitive recursion" and its role in Goedel's proofs. Bill Wvbailey (talk) 15:27, 12 May 2009 (UTC) cc'd the expurgated section here for reference purposes. Wvbailey (talk) 03:41, 13 May 2009 (UTC)

Weasle words/ no sources

"Many logicians believe that Gödel's incompleteness theorems struck a fatal blow to David Hilbert's program towards a universal mathematical formalism which was based on Principia Mathematica. The generally agreed-upon stance is that the second theorem is what specifically dealt this blow. However some believe it was the first, and others believe that neither did."

Who are these logicians? Who are the 'some'... etc. Shouldn't there be a banner that more sources should be cited 84.82.112.181 (talk) 14:14, 13 May 2009 (UTC)

Actually, all of that is explicitly sourced at Hilbert's second problem; the issue is that the text here did not properly link to that article. I copyedited it some. — Carl (CBM · talk) 19:02, 13 May 2009 (UTC)

Endless reference and supernatural numbers

Might I recommend adding two new sections: one elucidating the character of Gödel's statement as an endless chain of references rather than a self-referential statement, and another on the possible existence of supernatural numbers as a result of the addition of ~G as an axiom. In the first, we can explain that the chain of reference in the nested theories T, T', T", ... takes the form

G -- states unprovable --> G' -- states unprovable --> G" -- states unprovable --> ...

and that a proof of G would, by a translation theorem resulting from recursive axiomatizability, translate into a proof of G' in the next theory, the very proof that G states does not exist, thereby disproving the internal consistency of arithmetic.

In the second, we can explain how the addition of ~G as an axiom allows for the existence of a supernatural number that does not correspond to any numeral and yet inherits inductive properties in the theory T by playing the role of 'some number' that proves G'.

Such sections could pave the way to a clearer solution of the problem of incompleteness.

Scott7261 (talk) 12:42, 27 May 2009 (UTC)

Mistake in "Background" Section

Hello, I'm not absolutely sure about this, but I think there is a mistake in this article.

"A formal theory is said to be effectively generated if its set of axioms is a recursively enumerable set. This means that there is a computer program that, in principle, could enumerate all the axioms of the theory without listing any statements that are not axioms. This is equivalent to the ability to enumerate all the theorems of the theory without enumerating any statements that are not theorems."

I don't think this is right. It is possible for the set of axioms of a theory to be recursively enumerable, but for the set of theorems not to be. Indeed, we cannot enumerate the theorems without first having an effective decision procedure for whether or not a given sentence is a theorem. But using only an enumeration of the axioms we cannot achieve this - we cannot even decide for sure whether the given sentence is an axiom - it may not have turned up as one of the first 100 axioms in the enumeration, but it might be the 101st...

I believe that "its set of axioms is a recursively enumerable set" should be changed to "its set of axioms is an effectively decidable set".

Thanks. 118.92.139.152 (talk) 13:04, 11 June 2009 (UTC)

The text is correct. If the axioms are just enumerable, that is enough to enumerate all formal proofs, which in turn is enough to enumerate the theorems (= the conclusions of those proofs). This can be done perfectly well without knowing a decision procedure. For example one can enumerate the theorems of Peano arithmetic but there is no decision procedure for them.

Moreover, if a first-order theory has an enumerable set of axioms then it has an equivalent, decidable set of axioms. I forget who first proved this, but it is not difficult to reprove. It gives a second way to resolve your objection. — Carl (CBM · talk) 13:51, 11 June 2009 (UTC)

(edit conflict) You can create algorithms that work as the article describes, based on partial progress: it starts enumerating some of the consequences of the first 100 axioms, then goes onto interleave the consequences of the first 200 axioms, and so on. All theorems can be generated in this way in a desperately infeasible sense of "can". — Charles Stewart (talk) 13:53, 11 June 2009 (UTC)

clarify tag

An IP editor added a clarify tag regarding the word "true" in the statement of the theorem. The article presently states,

"The word "true" is used disquotationally here; the Gödel sentence GT states that no natural number with a certain property exists, and to say GT is true simply means that, in fact, no number with that property exists (see Franzén 2005 pp. 28–33). "

Frankly, I do not believe it can be put any more clearly than that. I would welcome suggestions from the IP or anyone else if that sentence is, in fact, unclear. — Carl (CBM · talk) 11:20, 16 July 2009 (UTC)

I reported "true" together with ref [1] as unclear after re-reading [1] several times, and most readers will agree I imagine. What is the point of writing things that nobody will understand, it needs redoing in a way that people can follow. How does GT for example relate to the text on the page, it's not obvious. Ref [1] seems to read that the word "true" is not necessary so what is it doing in the definition of the theorem on the page? How can anyone follow that twisted logic? It's completely nuts!

Apart from that, Franzel's discussion of the use of the word "true" in this context is quite involved (truth in arithmetic and mathematical statements etc...) and may not support using "true" in the article. I need to have more of a look at that.

There are various possibilities to rectify this: 1) Remove the word "true" from the definition and/or replace with some other wording more like Godel's original Theorem VI. 2) Remove or rewrite ref [1] so it is clear. 3) Get to the bottom of this using more leading references (preferred option) since I think it's important not to spread a popular misconception if it is one. —Preceding unsigned comment added by 92.39.205.210 (talk) 12:10, 16 July 2009 (UTC)

The use of the word "true" as in the statement of the theorem here is the same as in the statements given in all mathematical logic textbooks, so removing the word "true" would be inappropriate. The article directly says, "The implied true but unprovable statement is often referred to as “the Gödel sentence” for the theory." so I don't see much possibility for confusion when the footnote says, "the Gödel sentence GT". Could you be more specific about exactly what part of the sentence from the footnote that I quoted above is unclear? I still don't see how to rephrase it in any beneficial way. — Carl (CBM · talk) 12:26, 16 July 2009 (UTC)

Well, it's mathematically true, but not logically true, since one could hold that, say, PA+~Con(PA) is the right basis for interpreting statements of arithmetic. I think there is a tricky point here: I don't like not adding the appropriate qualifications here, but likewise, they are more likely to confuse matters than clear up the doubts that people like the IP editor have. The second sentence of the footnote, about truth relative to consistency statements over PRA, presents the right way of looking at the incompleteness phenomena, but few people looking up the footnote are going to latch on to this.

The way I've explained it in the past is that if you think the theory in question is true, then you should believe it is consistent. That belief is what commits you to a sufficiently strong interpretation of arithmetic to accept the Gödel sentence as being true. If you can find a way of believing in the truth of some axiomatisation of arithmetic without believing in the theory's consistency... well, this will not be a sticking point for so many readers. — Charles Stewart (talk) 13:28, 16 July 2009 (UTC)

I don't know that the provability interpretation is the "right" one. The disquotational interpretation is equally common. In any case both are included. I still cannot figure out what doubts the IP editor has. — Carl (CBM · talk) 22:43, 16 July 2009 (UTC)

Interesting comments but Franzel 2005 p3 clears this up for us by the definition there of the incompleteness theorem which in this context equates to a rewording as follows:-

Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement in the language of the theory that can be neither proved nor disproved (i.e. is undecidable) in the theory.

So ref [1] can be removed as well as the contentious "true" word. This simplifies and clarifies exactly what is going on with the incompleteness theory. The truth of the arithmetical statement is not mentioned in Theorem VI and such truth is an independent topic. Personally I would say arithmetic comes from assumed axioms too and therefore there is no absolute truth in it either.

Further reading of Franzel 2005 p28-33 did not show justification for using "true" but rather a general commentary on the question. So a reference would be required for its use. In fact Franzel mentions Tarski on p32 showing A is true <--> A, so "is true" is superflous thereby supporting the new rewording above since you should avoid saying the same thing twice (pleonasm). —Preceding unsigned comment added by 92.39.205.210 (talk) 14:53, 16 July 2009 (UTC)

The Goedel sentence of a consistent theory is true. That's just a fact. It is important to state this forthrightly, precisely because the popularizers often don't. --Trovatore (talk) 17:57, 16 July 2009 (UTC)

As to "is true" being redundant, yes, in some sense that's so, but it's needed for grammatical reasons. You can't just say the Goedel sentence of a consistent theory and leave it at that — it's not a complete English sentence. --Trovatore (talk) 18:00, 16 July 2009 (UTC)

If you have access to Franzen's book, look on p. 40, where he explains that Gödel's proof shows, under the assumption that the theory is consistent, that the Gödel sentence is true. The statement in the present article does include consistency as a hypothesis. — Carl (CBM · talk) 22:43, 16 July 2009 (UTC)

Please quote your exact reference(s) at the end of the definition following "Gödel's first incompleteness theorem states that:". The note [1] should then be removed since it is not required if there is a proper reference to the whole text, which is required in disputed cases like this. I have partly quoted my alternative for the above i.e. Franzel 2005 p3 which is Franzel's best definition of the theorem since he states it at the beginning of the book. Why are you rejecting Franzel's definiton? You are not allowed to make up your own definition (original research) so you need a reference with the exact text.

I didn't just say the Goedel sentence of a consistent theory, what I suggested was the following wording from Franzel and you should please say what is wrong with it:-

<prelude> there is an arithmetical statement in the language of the theory that can be neither proved nor disproved (i.e. is undecidable) in the theory.

Why should you possibly need to add the word true? It adds nothing, and the wording is perfectly clear as it is. Popularizers who don't add "true" are right not to.

All of mathematics including arithmetic is based on assumptions and therefore there is no absolute truth in it and never was, it is a game of the mind that's all, opinions of the founders. Mathematical truth just means "derivable from the assumptions" which the average reader who will be non-mathematical will not know. On page 30 Franzel states that mathematicians avoid the word true altogether or put scare quotes around it when talking to non-mathematical audiences to avoid the philosophical problems. Do you dispute this? So why are you not heeding this advice? Do you want to mislead the public and make Wikipedia become a more unreliable source of information that it already is? The average reader will interpret "true" as absolute truth and therefore be misled into thinking the incompleteness theorem is more than it is.

Contrary to Trovatore there are no facts in this. Truth is a complex and ambiguous topic which experts disagree on. In logic there are big problems with the simple bivalent true/not true idea e.g. the liar paradox, and there are even three value logic proposals to resolve it (true, not true, undecidable). Better to talk in terms of provable and unprovable or decidable and undecidable rather than true or false. To use the word true you have to assume that you can speak of arithmetical statements as true or false as Franzel points out on page 29. So the mathematical word true follows from an assumption, and so is clearly not "fact", it is an opinion.

Anyway I haven't got time to keep arguing about this, it just seems common sense to avoid the word true since this can easily be done with Franzel's wording but you wont listen. So if you wish to keep misleading the public and lowering the reputation of Wikipedia still further then please do so, but first quote your reference(s) as I requested above and put them in the article at the end of the disputed definition. Note [1] should then be removed since it is not required if there are proper reference(s) at the end of the definition. As far as I know Wikipedia should operate on references and not Notes.

Unfortunately Wikipedia's control systems are not good and allow bad information to persist but there is nothing I can do without spending loads of time contacting administrators and filing complaints etc.

Sadly I haven't got access to p40 of Franzel since Google books only goes up to about p35. If you could quote the relevant part here it would be appreciated. —Preceding unsigned comment added by 92.39.205.210 (talk) 11:31, 17 July 2009 (UTC)

Here are some references.

Franzen says on p. 40, "All Gödel's proof shows is the implication 'If S is consistent, G is true'." Here S is the theory and G the Gödel sentence.
In the Handbook of Mathematical Logic, Smorynski has an article expicitly about Gödel's theorems. He writes on p. 825 that the Gödel sentence of a consistent theory is "easily seen to be true" because it "asserts its own unprovability and it is indeed unprovable". This is the disquotational meaning of truth presented in the footnote.
Nagel and Newman, on pp. 92–93 of their well-known book Gödel's proof, say
"Why is it so remarkable ... that a formula can be constructed within arithmetic that is undecidable? ... Although the formula G is undecidable if the axioms of the system are consistent, is can nevertheless be shown by metamathematical reasoning that G is true." (their emphasis) They go on to present the disquotational argument for the truth of the Gödel sentence.
Kleene's statement of Gödel's theorem on p. 250 of his Mathematical Logic directly refers to both the truth and the undecidability of the Gödel sentence.

These are just a few references; there are many more available. — Carl (CBM · talk) 12:33, 17 July 2009 (UTC)

My issue with talk of disquotation is that it needlessly brings in another tricky concept, the interpretation of predicative uses of truth, for no payoff whatsoever. The Gödel encoding nowhere treats truth simpliciter, it codes provability with respect to a recursive set of axioms. Why put the interpretation of truth under the spotlight when treating a result that predates the idea of disquotation? I haven't Smorynski's article to hand, but from my recollection, he was concerned with the interpretation of provability relative to PRA, and not abstract truth. I don't see where it supports any theory of disquotation. — Charles Stewart (talk) 13:27, 17 July 2009 (UTC)

Smorynski does go on the discuss relative consistency results, but the text I quoted above refers to a disquotational interpretation of the Gödel sentence. I wouldn't say that the mention of truth is needless. On one hand, the truth of the Gödel sentence is very commonly treated in the literature (I posted above to document that). On the other hand, the key impact of the incompleteness theorem is that it establishes a distinction between truth in the natural numbers and provability within any particular axiomatic framework for arithmetic. One can hardly discuss this impact (as the text below the statement of the theorem does) without using the word "true".

Gödel himself was aware that he could prove the Gödel sentence true, he simply avoided the term because he felt it was out of fashion at the time and might make it less likely for his paper to find acceptance. This is documented on the Stanford Encyclopedia of Philosophy entry on Gödel, and elsewhere, although I don't have the other references at hand right now. [5]

So here is a synopsis of my position:

Many reliable sources go out of their way to explain that the Gödel sentence is not only independent, but also true. Kleene explicitly states the theorem that way. We should do so in our article as well, because the truth of the Gödel sentence is a key aspect of the theorem.
The meaning of "true" most often intended is truth in the standard model, that is, disquotational truth. The Gödel sentence says that there is no natural number with a certain property, and is true in the sense that there actually is no natural number with that property.
The footnote is intended to clarify this, in case someone wonders what is meant by "true". If there is any clearer way to express the second bullet, I would be happy to put it in the article.

— Carl (CBM · talk) 19:59, 17 July 2009 (UTC)

I think you are reading something into the Smorynski quote that isn't there. He makes an observation, using the word true. The fragments you have cited say nothing about how "true" is to be interpreted, and nothing about standard interpretations.

Gödel's incompleteness theorem is one of those results, like Cantor's theorem and Tarski's undefinability theorem, that provoke misunderstanding and should be treated economically. Dangling disquotation and standard interpretations in front of skeptically minded readers suggests to them a hidden assumption.

If we were to introduce the idea of Gödel's encoding of the provability relation into our restatement of the theorem, then we could ditch all talk of truth in favour of talk abour provability. I'm going to WP:BRD this afternoon, since it is probably a little tricky to make clear what I have in mind. — Charles Stewart (talk) 06:09, 18 July 2009 (UTC)

It really doesn't matter much how one interprets the word true here; the Goedel sentence of a consistent theory is true, in whatever sense it's true that the theory is consistent. And you're assuming that sense — it's discharged, by making the consistency a hypothesis.

The bit about disquotation simply offers a deflationary interpretation, for those who might otherwise be frightened by the supposed metaphysical import of the word. --Trovatore (talk) 10:46, 18 July 2009 (UTC)

I don't believe we can or should eliminate all mention of truth from the article. I have said before that it might be a better idea to have an entire section on the truth of the Gödel sentence where it can be discussed more leisurely. But at present the truth of the sentence is briefly covered in the paragraphs below the statement of the theorem. What Trovatore has just said mirrors the Smorynski quote: the Gödel sentence says it is unprovable, and under the assumption of consistency it really is unprovable, and in this sense the Gödel sentence is true. Perhaps you are just objecting to calling that a disquotational interpretation of truth? — Carl (CBM · talk) 12:56, 18 July 2009 (UTC)

fact tag

92.39.205.210 added a fact tag. Normally it is better practice to add the reference directly for things, like that statement, that can be so easily sourced, instead of adding a fact tag. In any case I added a reference to Kleene 1967. The precise statement of Theorem V on p. 250 is:

"In the system N of §38, there is a closed formula

C_{p}

such that (1)

\lnot C_{p}

is true, (ii) not

\vdash \lnot C_{p}

in N, and (iii) not

\vdash C_{p}

in N. More generally, this applies to any formal system N in which, to each a, there can be found effectively a closed formula

C_{a}

(expressing

\exists x\,T(a,a,x)

) such that (a)–(c) (or (b)–(d) below) hold."

The proof that Kleene gives for the truth of the statement uses disquotational truth: "... there is some number p such that $\lnot \exists xT(p,p,x)$ (i.e. (i), by what $C_{p}$ expresses) ..." — Carl (CBM · talk) 13:17, 20 July 2009 (UTC)

reference style, removing refimprove tag

This article use Harvard reference style, which is a standard referencing style on wikipedia. The footnotes are thus used for side comments, while reference information is included directly in the article. Thus the concern that this is not "Wikipedia standard format" is unfounded. I will remove the refimprove tag added for that reason; of course it is still fine to ask for citations for individual things. — Carl (CBM · talk) 12:35, 25 July 2009 (UTC)

I see though that at least a couple of the footnotes are apparently being used as citations; should this be changed?

For clarification, in articles where citations are given as footnotes, is it not also permissible to make side comments in footnotes as well? Sometimes it would be rather awkward not to be able to (as witness the current example). --Trovatore (talk) 20:06, 25 July 2009 (UTC)

Earlier versions of the article (e.g. [6]) have Harvard refs and informative footnotes. The present "reference" footnotes (which lack most bibliographic info) were added later; someone commented at the time that they were not consistent with the former formatting [7]. So I think it would be reasonable to flesh them out to full references in the references section, and parenthetical references in the text, sure.

Some articles that have references in footnotes do also put informative notes there; others use various methods to split the notes into two groups, one for references and one for notes. But I was always under the impression this article uses Harvard-style refs, e.g. [8] — Carl (CBM · talk) 20:21, 25 July 2009 (UTC)

I have no objection to the Harvard style. I was just pointing out that it is not used entirely consistently, and wondering whether that should be cleaned up.

Two of the three (or so) cites in the Notes section relate to the Jaki stuff, which as far as I'm concerned can be removed entirely. I think it's very likely undue weight to mention Jaki at all. --Trovatore (talk) 20:35, 25 July 2009 (UTC)

I tried to look up Jaki's paper that was cited in our article; it seems to have been published through Real View Books (realviewbooks.com) rather than any academic or professional press. I removed the mention of Jaki for now, but I would love to hear any arguments in favor of it, because I think he is right on the edge of suitability for inclusion. I then copyedited and referenced the section on "postmodernism". I think the references now are much more clear than they were before; let me know. — Carl (CBM · talk) 21:38, 25 July 2009 (UTC)

"How to understand the First Incompleteness Theorem"

This section, added by User:Vibritannia, has been removed by Chalst and Trovatore. I also think the section is not appropriate for this article as it stands. The new text duplicates the discussion of the first incompleteness theorem that is already in the article, and moreover is written in a nearly-incomprehensible style. The latter might be less of an issue if the material was not already in the article, but we already discuss the first incompleteness theorem in depth. Once an article is sufficiently thorough, new additions need to be integrated in some way, rather than merely being inserted near the bottom, and new material needs to take into account what is already covered in the article and the way it is covered, so that the article flows as a single document. — Carl (CBM · talk) 13:32, 26 July 2009 (UTC)

Concur. Paul August ☎ 13:17, 27 July 2009 (UTC)

Hi Carl. I didn't realize it was nearly incomprehensible. I thought what I added explained incompleteness in a way that avoided creating the impression that it is paradoxical.

I think I have identified a sticking point in grasping an understanding of incompleteness and provided an addition to the article to tackle it. If we work out what needs to be incorporated where (in the rest of the article) to cover it, we can just delete the section I added. --Vibritannia (talk) 16:40, 26 July 2009 (UTC)

At least I found it very difficult to read in places. Which sticking point were you thinking of? It looked to me like you were saying: the Gödel sentence for a theory T says that a particular sentence G is not provable from T. This in no way means that G might not be provable in some other theory. For example, the theory T' obtained from T by adding G as a new axiom will be able to prove G; if T' is consistent, it will have its own Gödel sentence G' that cannot be proved in T'.

I would like the section on the first incompleteness theorem to be quite accessible. Actually I have never been completely happy with the top two sections on the first incompleteness theorem that are already there. — Carl (CBM · talk) 22:22, 26 July 2009 (UTC)

Yes, I think that's basically it but with the addition of saying 'since G only says it cannot be proved from the axioms of T (which it does so indirectly from within the definitions that are required for its expression), no contradiction is implied if G can be proved in T' (which includes an axiom not mentioned {by its Gödel number} in those definitions). In other words, G does not say it is not provable in T'; it only says it is not provable from a particular subset of the axioms of T'.

Since that is implicit in what you just said, maybe it should have been obvious to me. Unfortunately it wasn't, and I've been struggling for a long time.

Another thing that might be worth a note somewhere in the article is that in Bew_κ, κ is a set of numbers, each of which refers to a string of symbols. Those strings are the ones necessary in order to express G. Without them, what G says is undefined (and it certainly does not express any high-level meaning such as the concept of proof). Maybe Gödel thought that was obvious in his paper, but again I struggled for absolutely ages before that penny dropped.

Another point is, you cannot really just add G to T to get T'. G says nothing without the definitions upon which it depends. You would have to add all the strings contained in the forty-odd definitions required to express G (probably about 100 strings). Those strings don't look much like what we usually think of as axioms (that's why we called them definitions), but to add G as an axiom, they would have to be added too. If you could somehow incorporate them into G directly so that they became superfluous, G as a string would be stupendously long, and so it still wouldn't look very much like what we normally think of as an axiom.

Also the argument assumes that if the interpreted content is correct (or true), the formal content must be true as well (the interpreted content is what you get informally by understanding that the numbers refer to strings of symbols, whereas the formal content is just what you get directly from the meaning of the symbols of the formal system). Is that just supposed to follow from T being a consistent theory? It doesn't ever seem to be explicitly addressed, which makes the argument even more confusing, in my opinion.--Vibritannia (talk) 11:04, 27 July 2009 (UTC)

There are several points there, so I'll respond to the separately.

The article presently says the following, which is meant to address the point from your first paragraph. Perhaps this is slightly too terse, and can be expanded. But I think it should not get larger than a paragraph.

"It is possible to define a larger theory T’ that contains the whole of T, plus G as an additional axiom. In this case, G is indeed a theorem in T’ (trivially so, since it is an axiom). However, this incompleteness theorem then applies to T’: there will be a new Gödel statement G’ for T’, showing that T’ is also incomplete. Each theory has its own Gödel statement."

Re just adding G to T, this certainly is possible. T is a set of formulas, and G is a single formula in the language of T. You are concerned about the fact that Gödel uses a lot of defined abbreviations in his paper. The most common way to look at these is to simply view them all as informal abbreviations for the things they represent. These abbreviations must be removed to obtain the literal formula being described. Thus G is informally written as "~Bew(...)", but this is not itself a formula, just shorthand to avoid having to write a particular very long formula. This way of handling abbreviations is necessary because G is supposed to be a formula in the language of T, and all the defined terms like Bew are most likely not in the language of T. I added a clarification about this just now: [9]

I am not sure what you mean by "interpreted content" versus "formal content". I can guess what you mean by interpreted content, but not what you mean by formal content.

— Carl (CBM · talk) 11:53, 27 July 2009 (UTC)

For your first point, that sounds like a reasonable suggestion.

As for your last point, by interpreted content I just meant the same as Gödel meant by the term in his 1931 paper: it's what you comprehend by knowing that the numbers refer to strings (rather than thinking only about numbers whenever you see a number). By 'formal content' I meant just what you get by applying the formal interpretation, i.e. the formal system contains symbols which are just meaningless squiggles, the formal interpretation specifies what meaning to attach to the meaningless squiggles, so the formal content is just what you get when you know what the squiggles are supposed to mean. (Maybe these words have other more-usual meanings that I don't know about, and for that reason I'm causing confusion.)

As for your second point, it is nowhere near as straightforward as the impression your explanation creates. If all the definitions were simple definitions, then obviously it would just be a simple case of substituting all the abbrevations for what they abbreviate. But in the case of recursive definitions, as far as I have been able to work out, you are forced to resort to using the Gödel beta function, but that function uses the modulo operator which itself has to be recursively defined. So unless you add another symbol to the formal system and specify in the formal interpretation that that symbol is the modulo operator, you won't be able to add G without adding at least 3 other strings. But say I'm mistaken, and you can add G, then in any case, that G will be a hugely long, humanly incomprehensible, dog's dinner of a string. If it looks absolutely nothing remotely like anything we have previously called an axiom, can we reasonably call it an axiom? That is a particularly pertinent point because all the definitions, you could call axioms - as they do in the Metamath project for example. You can satisfy yourself that that is the case by examining Gödel's definition of Bw_κ: it says every string in a proof must be either an axiom, a string referred to by the Gödel numbers in the set κ (i.e. all the strings which constitute the simple and recursive definitions necessary to express G), or an immediate consequence of any strings earlier in the proof. (I just think that the statement that G can be added to T tends to create a misleading impression {though I won't say it is false because I don't know enough to be sure} and for that reason, it could generate confusion.)

You could add "<conjunction of definition-strings> → G", I suppose, but that's not exactly G, is it. When you added that, it would simply be an axiom that the definitions upon which G depends imply it. Hold on! That's interesting. It doesn't sound like an axiom; it doesn't sound like a definition; it doesn't sound like a tautology (because the bit you say second can't be said without having said the bit you said first; so what is it? What kind of a thing is it? --Vibritannia (talk) 10:15, 28 July 2009 (UTC)

break: axioms

The way language is used in contemporary logic, "axiom" simply means any sentence that is assumed as part of a theory. There is no connotation that the axioms must be natural, short, easy to understand, or even true. For example, I could add "0=1" into Peano arithmetic as another axiom, to obtain an inconsistent theory. So you are right that the Gödel sentence of a theory will be very long and hard to read, but that is not an issue that logicians today worry about.

I am afraid that you are slightly mistaken about how the definitions in Gödel's paper work. In principle, it is possible to express the Gödel sentence of Peano arithmetic directly in the language of arithmetic (

\langle 0,1,+,\times ,=\rangle

) with no additional nonlogical symbols. This is one area where a more modern exposition of the theorem will be more clear; Gödel's writing is somewhat terse, and the formal system of arithmetic he considered was the one from Principia Mathematica rather than any modern axiomatic theory of arithmetic.

Regarding the modulo operator, it does not need a recursive definition; here is a non-recursive definition in the language of Peano arithmetic:

a\equiv r{\pmod {n}}\Leftrightarrow \exists m(n\times m+r=a)

These lecture notes by Peter Smith give a thorough explanation of how to get the Gödel sentence for Robinson arithmetic (Q), a weaker system than PA that uses the same language as PA: [10] (see Chapter 10). — Carl (CBM · talk) 13:02, 28 July 2009 (UTC)

Thanks, Carl, for the lecture notes. In chapter 11.3, it asks whether the beta function can be constructed from the functions successor, sum, and product -- and presumably the answer is yes, and presumably it cannot be constructed from just the successor.

But the successor function is the only one you're allowed -- basically, I suppose, because a formal system is supposed to be a system of trivial symbol manipulation, and the successor function is very easy to implement by manipulating symbols (you just stick another one in front -- the number of symbols you had before you stuck another symbol in front is the number you had before applying the successor function, and the number of symbols you have after sticking another symbol in front is the number you have after applying the successor function). That definition of modulo is sort of a cheat -- the definitions of plus and times, when all you have is the successor function, are recursive.

But if I let that slip, you still have to use a beta function, but that seems to me to be a massive problem. How can the interpreted content of the beta function, which only incidentally produces the same relationship up to some finite limit, be deemed to be the same as the interpreted content of the recursive definition it is supposed to replace, which exhibits its pattern with no limit whatsoever. It can't, can it. The interpreted content of G made out of beta functions isn't the same as the interpreted content of G made out of recursively defined abbreviations. And that is fatal because it was only the interpreted content of G, after all, that led us to believe it was true in the first place. So if we haven't properly managed to preserve the interpreted content of G, why would we want to add it as an axiom anyway? (Unless, I suppose, we can (from within the formal system) prove pukka G from pseudo G; I don't know about that.)--Vibritannia (talk) 16:38, 28 July 2009 (UTC)

(←) Two comments:

Gödel's theorem does not go through in first-order arithmetic with only successor, nor with only successor and addition (Presburger arithmetic). The reason that the theory from Gödel's original paper only has successor is that it has more than just variables for numbers, it also has variables for functions, as in second-order arithmetic. It is actually much easier to make the incompleteness theorem go through in that setting; the β function is not required at all, because one can already quantify over sequences in the guise of functions from N to N.
I still do not know what "interpreted content" is. Can you either express that in the terminology of contemporary texts, or give a detailed reference to where you are reading it? I skimmed through Godel 1931 but didn't find it in the translation I have at hand.

I would continue to encourage you to avoid Gödel's 1931 paper until you understand the theorem when it is presented in contemporary terminology. The original paper, while correct, is written in an extremely terse style that was common at the time, so that one has to have a very good idea what is going on to follow it. And many of its quirks (such as the use of higher-type arithmetic) only serve to make the theorem more difficult to understand at first. If you are interested in learning about the theorem, there are many contemporary texts that present it in a thorough and elementary way with few prerequisites. Nagel and Newman's Gödel's proof is a classic. — Carl (CBM · talk) 20:38, 28 July 2009 (UTC)

They are not variables for functions, but I know what you mean. Yes, you have to use those variables to define what you need to create G, but those definitions include amongst them recursive definitions.
Say you had a computer language, but every symbol in it was a Chinese character (assuming you don't read Chinese) -- no spaces, linebreaks, or punctuation marks of any kind. You could write a sequence of Chinese characters and then try to compile it. Just occasionally you would get lucky, and your program would compile. It compiles, so you look up the Chinese characters in the manual that came with the compiler which tells you in English and symbols that you recognize what each Chinese character, or short sequence of characters, means -- that's the formal interpretation. So you translate the program into English and realize that when executed the program writes some numbers to a hardware output port, and that the particular port written to is identified only by a number (that's the formal content of your program). So you go back to the manual to look up what piece of hardware the port with that number is a port to. And the manual rather unhelpfully says 'platform specific' and gives no further information. So you go back to your program and look at the sequence of numbers that will be written to the port if the program runs. Then you take out the hardware specification for your computer platform and work out for each output port in turn, what will happen if that sequence of numbers is written to that port. (For some reason, in the hardware description you have available to you, the ports are named but not numbered). You have 100 ports on your computer. The compiler manual says the port number you supply to the port procedure is taken to be modulo however-many-ports-there-are-on-your-platform, so you know your program will write to a port, you just don't know which one. You start by assuming that the port written to is the first one in your hardware specification. You know what will happen if the sequence of numbers is written to that port. Knowing that, you work backwards through your program interpreting what each part of your program does, knowing what it achieves in the end. You repeat the process for every port, and at the end, you have 100 different descriptions of what each part of your program does (in the light of what it would do as a whole, rather than an abstract descripion that could apply to any port). Each one is an interpreted content of your program, content that you interpreted from the formal content of the Chinese characters.--Vibritannia (talk) 09:54, 29 July 2009 (UTC)

Different codings

I removed two explanations that were based on the idea of different codings. It is true that one could make different Gödel numbering systems, but that is not the reason why the two claims being explained are true. Moreover, in the literature, the standard way to handle the arbitrariness of coding is to simply assume at the outset that an acceptable coding has been fixed, and then ignore all other codings.

In one place, I thought the explanation in terms of codings was misleading. Suppose there are two codings, A and B, and thus two provability predicates Pvbl_A and Pvbl_B. Let #_A(φ) denote the Gödel number in system A of a formula φ, and #_B(φ) the number in system B. Then for many pairs of codings A,B, it will be possible to prove that for all φ,

Pvbl_A(#_A(φ)) ↔ Pvbl_B(#_B(φ)).

So just the existence of different codings does not imply that adding "Pvbl_A(#_A(φ))" to the theory will keep the theory incomplete. — Carl (CBM · talk) 12:19, 5 August 2009 (UTC)

article use for godel sentence?

"The true but unprovable statement referred to by the theorem is often referred to as “the Gödel sentence” for the theory. It is not unique; there are infinitely many"

If there are many, why is it referred to as the Godel sentence? Something should be said, if this is grammatical oddity is correct usage. —Preceding unsigned comment added by 24.90.117.35 (talk) 02:49, 30 September 2009 (UTC)

Well, the point is that it's unique, except for implementation details that we don't really care about. Choose a different coding for the symbol 0, or a different (but not essentially different) way of finding a fixed point (that is, of saying "I am not provable in T"), and you'll get a different Gödel sentence. But it won't be different in ways that we're likely to find interesting. So we pretend that you and I make the same choices of these details (in reality, probably neither of us has bothered to make these choices at all), in which case we would get "the" same Gödel sentence.

That's an explanation; it's not really satisfactory text for the article. I don't really have a suggestion at the moment for how to make this clear in the article. --Trovatore (talk) 02:56, 30 September 2009 (UTC)

I think that the present text of the article goes into enough detail about the situation: the statement constructed in the theorem is called "the Gödel sentence", and there are infinitely many other sentences with the same property (e.g. "G & φ" where G is the Gödel sentence and φ is any logical validity). There's no reason to dwell on this point in detail at that place in the article. There is a separate issue about how to express G itself; this is already discussed elsewhere in the "Second incompleteness theorem" section. — Carl (CBM · talk) 03:04, 30 September 2009 (UTC)

Section 9.2, "Appeals to the incompleteness theorems in other fields

The end of this article states that other disciplines have tried to use Gödel to make observations about non-mathematical subjects. But instead of saying what those uses are, it immediately lists a bunch of scholars who dismiss the project. All the readers of Wikipedia know right now is that some sociologist once defended a sociological use of Gödel but we don't know why or how; only that doing so annoyed someone else. This article really needs to list non-mathematical uses of Gödel. Critiques of those uses are fine but only after we know what the critiques are critiquing. --Hapax (talk) 18:17, 30 September 2009 (UTC)

The article Doxastic logic has at least one non-mathematical application of GIT. Pontiff Greg Bard (talk) 18:46, 30 September 2009 (UTC)

This book (listed in the article's references) goes into that subject (sociological uses, etc.) in depth:

Torkel Franzén, 2005. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. A.K. Peters. ISBN 1568812388 MR2007d:03001

69.228.171.150 (talk) 00:09, 30 October 2009 (UTC)

Modern Proof

When discussing an 80 year old result, it is essential that the proof be streamlined so that it can be followed by a modern reader. This is especially true regarding Godel's paper. The proof in this section can serve as a complete replacement for the section "Proof sketch of the first incompleteness theorem", since it is not a sketch but a full proof. The method follows Godel's original paper closely, although it takes more liberties with Rosser 1936.

The discussions of such modern proofs in the past has been hampered by a lack of consensus about what constitutes original research when editing scientific articles. I hope that the current discussion will be in line with WP:ESCA. Rewriting Godel's paper in terms of computer programs makes the logic of the argument transparent, and allows notorious sticking points like the self-reference, the Rosser trick, and omega-consistency to be discussed precisely and completely with no fuss. This is a vast improvement over the previous presentation, perhaps enough of an improvement to make the other presentations unnecessary.Likebox (talk) 23:28, 14 October 2009 (UTC)

You have proposed this before, and there was neveragreement to include it. What has changed? I see you are still not useing the word "quine" with its usual meaning. A quine prints its own code to the output and then stops. A program that does not print its code at all is not a quine. — Carl (CBM · talk) 01:58, 15 October 2009 (UTC)

In short, the same objections as in 2007 (see this talk page archive) still apply, so I am again going to remove this. — Carl (CBM · talk) 02:02, 15 October 2009 (UTC)

What has changed is that we have a new proposed guideline WP:ESCA, which adresses this issue: when you have text that explains intermediate steps in mathematically verifiable well sourced theorems in terms that are clear and correct, you should evaluate the intermediate steps on their own terms. This policy guideline has supporters, and they might change the previous outcome.Likebox (talk) 02:05, 15 October 2009 (UTC)

Also, if you look at the text, it has expanded to be much more detailed as an explanation, and it does not use the word "Quine" inappropriately.Likebox (talk) 02:06, 15 October 2009 (UTC)

I do generally think of the proofs in much the way that Ron does (the explanation of the Rosser trick is especially nice, really, though the last time I looked at it it failed to make the key point explicitly, which is that the program must always halt). But I don't think this material belongs here. It is too personal in style, and too didactic in intent. It is not within the scope of this article to teach the proof to anybody, and that's exactly what I think Ron wants to do. A fine goal, but not here. --Trovatore (talk) 02:07, 15 October 2009 (UTC)

Re Trovatore: You might consider removing the proof; I did once, but Likebox reverted. — Carl (CBM · talk) 02:11, 15 October 2009 (UTC)

Re Likebox: the problem with your proof is that the literature does not present things that way, and we generally follow the published literature. Also, the text you added still says, "A program which prints its own code in this way is called a Quine.", but the program you are talking about is not a quine. — Carl (CBM · talk) 02:12, 15 October 2009 (UTC)

To trovatore: The Rosser trick explanation can include the main point, which is that the program halts either way, as you say. But the text has been expanded significantly, and it should be evaluated on its own terms. The reason I think it is important to include something like this is because the theorem should be understood as broadly as possible. One of the stated goals of Wikipedia is to make specialist knowledge available as widely as possible. It is a shame to not include text that can do this for a subject as notoriously inaccessible to laypeople as the Godel incompleteness theorems.

To CBM: Your issue is what WP:ESCA is designed to adress. The "literature" on this is 80 years old, and incomprehensible today. The modern "literature" is textbooks, which are written by a different process than research papers, and are not generally very well written. When explaining proofs, it is important to fill in intermediate steps in the clearest possible way, not necessarily in the way that is most common in the textbooks. These filling in of the gaps should be evaluated for accuracy, and clarity, and they should compete on their merits.Likebox (talk) 02:25, 15 October 2009 (UTC)

There is plenty of contemporary literature on the incompleteness theorems and their relationship to computability; there is no need to look at anything 80 years old. The contemporary literature is clear that the diagonal lemma is relevant, but not "programs" nor "quines". This has all been discussed before. — Carl (CBM · talk) 02:40, 15 October 2009 (UTC)

New section tagged as POV violation, rather than summarily reverting. I don't see it as relevant, as less complicated or more understandable than the original proof, nor appearing in the literature. All three are needed for inclusion. — Arthur Rubin (talk) 02:43, 15 October 2009 (UTC)

I changed my mind. It's not in the (current) or original literature, so it shouldn't be here. — Arthur Rubin (talk) 02:48, 15 October 2009 (UTC)

Well, it is in the literature if you reword it to use standard terminology, in which case it is the same as the other proof already in the article. — Carl (CBM · talk) 02:52, 15 October 2009 (UTC)

The Rosser argument does not appear in the article, and neither does a single complete proof of any of the Godel theorems.Likebox (talk) 02:59, 15 October 2009 (UTC)

The article links to Rosser's trick, where the method is explained in detail. If the article does not contain a complete proof, adding another incomplete proof hardly remedies the situation. The same arithmetization work that is required in the standard proof is also required in your proof, and I do not see that we will ever include a complete proof about arithmetization in the article. — Carl (CBM · talk) 03:12, 15 October 2009 (UTC)

The problem is that the Rosser's trick article is written in a way that nobody will understand. This is not acceptable on Wikipedia, when clear presentations exist. The presentation in terms of deduction methods in formal logic is very outdated, since it does not emphasize the computational aspects. There's nothing wrong with keeping it, just don't remove other presentations. Each person has their own preferred proof.

I don't expect to convince you, but I hope other editors have enough common sense to disagree with you.Likebox (talk) 20:04, 15 October 2009 (UTC)

(deindent) To CBM: the proof is a gloss of Godel's paper, which allows the original paper to be understood. This is very important for people who do not already know the result. The section should be evaluate on its merits. This is a well understood topic. If material which is clear and correct cannot be incorporated, then Wikipedia will not be able to serve its purpose. I hope that other editors will not allow this material to be deleted, because that would prevent articles on computability theory in general. Computability theory is one of the few in mathematics which has not been adequately presented on Wikipedia.Likebox (talk) 02:57, 15 October 2009 (UTC)

The disputed section appears below.

"Clear" and "correct" are two key properties (although, as I keep pointing out, the text you add is not really "correct"). But another key requirement is that the content we have here needs to match the published literature. Even if things are clear and correct, Wikipedia isn't the place to change the way that the field of mathematical logic handles the incompleteness theorems. — Carl (CBM · talk) 03:10, 15 October 2009 (UTC)

You say it is "not correct", this is just ignorance. It is self-evidently correct, as both myself and Trovatore have tried to explain. This is what ESCA tries to do--- it tries to get the editors to talk about the content of the material as opposed to the form.Likebox (talk) 20:06, 15 October 2009 (UTC)

As Trovatore has explained, it's correct, and identitical to the standard proof when "quining" is defined. I'm not sure I agree, but T has explained why your material shouldn't be here, as well. — Arthur Rubin (talk) 20:25, 15 October 2009 (UTC)

Actually, I think that was Carl. --Trovatore (talk) 20:25, 15 October 2009 (UTC)

Sorry. But you did also say it shouldn't be here.... — Arthur Rubin (talk) 20:30, 15 October 2009 (UTC)

Ron, I think you're hanging onto an extremely slim reed with this ESCA stuff. Forget that it's only a proposed guideline; let's suppose arguendo that it were in force. The main thrust of the text, as summarized in the "nutshell", is be extremely careful. It's mostly about increased rigor, not about loosening anything.

I can see three things that you might be talking about, and in every case I think you're making a very forced interpretation:

Discussions from first principles are in no way a violation of the ban on original research, ... but this continues since they are conducted on the talk pages. So that doesn't help you.
It does not constitute WP:OR to provide the logical connection between sourced premises and sourced conclusions, since “Carefully summarizing or rephrasing source material without changing its meaning is not synthesis—it is good editing.”. I think the intent of this is that you can fill in small gaps. This is frankly the most problematic sentence in the proposed guideline, even as I think it's intended, but I see no indication that it says you can completely recontextualize an entire argument.
Realise that different approaches or explanatory models are often all correct. Sure. But "correct" is not the same as "appropriate for the article". --Trovatore (talk) 20:33, 15 October 2009 (UTC)

You are not familiar enough yet with the proposed policy and its intention. I had the same reaction when I first read the policy. I am not trying to use the policy to justify this addition--- I am using this addition to justify the policy.

This policy is a deep attempt to change the culture of debate on Wikipedia. The goal is to make sure that people understand material that they challenge, and not challenge simply out of ignorance. Sometimes the exact text is not found in the sources, but that's all right so long as the content is mostly Ok. Sometimes exact text in sources is quoted out of context, and becomes incorrect.

For mathematics and science articles, it is easy to fix these types of errors, so long as the debate focuses as much as possible on content. That means, 1. Is it correct? 2. Is it clear? 3. Is it appropriate?

The debate here has floundered on points 1 and 2, with ignorant people suggesting that the material is incorrect or unclear (you aren't one of these people). Those people should recuse themselves from the discussion, because they have insufficient knowledge (this is also in WP:ESCA). Once they understand the material well enough, they can contribute more knowledgably.

As far as point 3, which is the sticking point between you and me, I am really unhappy that I can explain Godel's theorem in 10 minutes to any layperson and undergraduate, yet I am not allowed to post that explanation here once, so that I can be done with this obligation once and for all.Likebox (talk) 20:52, 15 October 2009 (UTC)

Well, as for your points:

Is it correct?
No, if you use the term "quining" withour further explanation. Yes, if you redefine (or, preferably, eliminate entirely) "quining". However, if you do that, it becomes only slightly different than the standard proof.
Is it clear?
Well, no. A "modern" translation of the standard proof into now-standard notation would be much better.
Is it appropriate?
Hmmm. See point 2. I'd say at most one version is appropriate, and the standard version is superior, as both appearing in sources, and being clearer.

— Arthur Rubin (talk) 21:26, 15 October 2009 (UTC)

To respond:

I did not use the word "quining" at all in this iteration of the text, except as an aside and a link. I just said "Let program P print its code into variable R" without giving this process a name. Later, I said that a program P which prints its own code is called a Quine, to provide a link.
There is no such modern translation of Godel's paper. To translate Godel's paper is a bit of an art. You need to focus on the main ideas, and find just the right notions which allow the proof to be encapsulated properly in terms that everyone understands. This is not done in modern textbooks. I have no problem with including the textbook version also, as long as the much clearer version I provided is included somewhere as well.
You say that the version in the article is clearer, but the version in the article is not a proof of anything, just the barest of sketches. It does not even pretend to prove Rosser's theorem. In addition, the gloss provided "G asserts that it is unprovable" while correct, skimps on the main point of how G talks about itself. This is fixed by the discussion I give, which makes the self-reference obvious. Programs can talk about themselves easily--- they print their own code. Sentences, in order to talk about themselves, have to have a convoluted structure.

As for clarity, I know that this version is superior pedagogically to any other version, simply because anyone who understands Godel's theorem sees that this version is identical and correct immediately, while anyone who does not understand Godel's theorem learns it about one hundred times faster from this version as compared to any other.Likebox (talk) 22:14, 15 October 2009 (UTC)

It's somewhat incredible that you claim there is not modern presentation of the proof, when there are numerous contemporary textbooks that prove it, and these do not simply copy Gödel's original paper. Indeed, the use of the diagonal lemma in the proof already included in this article is a typical characteristic of a modern proof of the incompleteness theorem. The use of "Bew" for the provability predicate is present even in some modern presentations; others use "Pvbl".

I agree the proof included here is just a sketch, but the version you are adding is also just a sketch. The vast majority of the work in the proof is in the results about arithmetization, not the parts about the diagonal lemma. You cannot wish this work away by simply claiming that it is now obvious... to make your sketch into a proof one would need to rigorously demonstrate that there are formulas in the language of arithmetic that allow one to determine whether computer programs halt.

The treatment of Rosser's trick here is very comparable to the way it is treated in many texts – as an aside, usually not even proved in undergraduate textbooks. However there is a full proof of it in its dedicated article, Rosser's trick. — Carl (CBM · talk) 23:23, 15 October 2009 (UTC)

(deindent) The proof is not a sketch, it is a complete and correct proof. You are confusing two different headaches, of vastly different types.

Proving that computations are statements about integers
Proving that deductions in logic are statements about integers

problem 1 is obvious today to everybody, because everybody knows that the memory of a computer is a big integer. Everybody also knows that a processor step is a simple computable function of this integer (if the memory includes the registers). The only slight subtlety is to make sure that the memory can be arbitrarily large. None of these things require any effort at all. Once you are give 1, then 2 is an obvious consequence--- the deductions of logic are obviously a computer program.

None of this requires any work, because the work has already been done by people who make computers. What does require a little bit of work is the following: showing that "SPITE does not halt" is a theorem of arithmetic.

Given the primitive processor step function "f" and the code of SPITE (interpreted as the memory of the computer at the beginning of the computation), then the statement "SPITE doesn't halt" just means, "forall N f(f(f...(f(R))...) isn't in a halting state". That's a statement about integers. For example, you can make spite set memory location 0xFFEE to 7f when it halts, and then the statement is "forall N f(f(f(...(f(R)...) does not have memory location 0xFFEE equal to 7f". The question of whether this is a theorem of arithmetic is then only the question of whether a particular primitive recursive function "f" can be talked about in arithmetic, and whether you can extract the byte at memory location 0xFFEE. These types of things are so obvious to anyone who programs a computer, or who understands arithmetic, that they are beneath saying. They are too trivial to waste time proving.

On the other hand, proving that the "provability predicate" can be formalized within arithmetic requires work, unless you are willing to say that the provability predicate is obviously arithmetic, because it is a computation. The textbooks do a lousy job of this. They obfuscate the subject for no reason.

One of Wikipedia's core policies is jargon-free presentations, whenever possible. This means that ideas must be presented in such a way that they are understandable by a lay-reader, whenever this can be done. While both presentations require some technical knowledge, the technical knowledge that the standard textbooks demand is highly specialized--- it requires the jargon of recursive function theory. The proof that I am presenting is self-contained, and requires only the most rudimentary knowledge of computers. This means that one of Wikipedia's core policies demands that this presentation be kept.Likebox (talk) 01:14, 16 October 2009 (UTC)

An article about recursive function theory should use the standard terminology of recursive function theory. Our goal is not to teach people; it is to be a summary of the literature, and a reference to it. — Carl (CBM · talk) 01:30, 16 October 2009 (UTC)

I disagree--- the job of Wikipedia is to present all of human knowledge in as widely accessible a way as possible. If textbook presentations of a subject are obscure, it is our job to simplify them as much as possible.

This is a core mission of wikipedia.Likebox (talk) 01:34, 16 October 2009 (UTC)

I am afraid there is little support for that, if by "simplify" you mean to recreate the entire framework of fields of inquiry in a way different than the published literature on the theory. It is entirely possible to present things plainly while still following the standard framework and terminology of the literature. — Carl (CBM · talk) 01:50, 16 October 2009 (UTC)

This is not one of those cases. It is very similar to articles on philosophy, where the terminology is often so crappy that you need to constantly translate to english. This is done. Similarly, here, the terminology is so bad that it must be translated to english.Likebox (talk) 04:26, 16 October 2009 (UTC)

Reverted again

Likebox has added the "modern proof" again. In addition to editors at this talk page, several editors at [11] have opined they do not support the proofs that were added to use non-standard "modern" terminology. Directed at Likebox: could you explain what has changed since a few days ago, in terms of support for the addition? — Carl (CBM · talk) 21:42, 18 October 2009 (UTC)

I have taught this proof to several people in the last few weeks, some of whom have made some comments that they would support the additions on this page. I am trying to keep the subject alive long enough to see if they show up (I'd bet against it). Right now, I agree that consensus leans against the material. But it's not OR, as you yourself have said, it is at best a slightly different presentation.

I don't have patience to argue this too much with you, considering that your arguments in the past were uninformed. In addition, your administrative actions make it more difficult to come to a reasonable consensus. We have not had anything resembling the past crises regarding this material.Likebox (talk) 03:31, 19 October 2009 (UTC)

Likebox, if you agree that "consensus leans against the material" as you write above, then it is inappropriate to continue to add this content. Paul August ☎ 14:07, 19 October 2009 (UTC)

We'll see. Consensus changes.Likebox (talk) 21:56, 19 October 2009 (UTC)

Yes it does, but it doesn't seem to have so far, and until it does, you should refrain from re-adding this content. Paul August ☎ 22:33, 19 October 2009 (UTC)

I agree. I'll try again in a year or two.Likebox (talk) 18:47, 20 October 2009 (UTC)

If you don't get a consensus before adding the material, you should be blocked. I still won't block you, although it's tempting. — Arthur Rubin (talk) 19:06, 20 October 2009 (UTC)

Come on, use your common sense. I try, and if I fail, nothing's lost except a small amount of discussion between editors, which has been reasonably productive. I don't think that persistence is in any way a violation of Wikipedia rules. How hard is it to revert and talk?Likebox (talk) 20:40, 20 October 2009 (UTC)

It wouldn't take long if we (sensible, or mathematically inclined) editors only had to revert it once each time. According to the edit logs, I removed it twice on this article and three times in halting problem, and CBM also removed it twice in this article. It might almost be reasonable in halting problem if "write your own code" was replaced by a simple beta-function argument; the precise machine model which is undecidable seems not to be that interesting, and given the proper choice of computer language, it might be more reasonable to do the self-instantation at the computer language level than at the logical expression level. (It's clear it hasn't yet been done on Wikipedia in a manner requiring less advanced logic than the standard proof.) — Arthur Rubin (talk) 15:17, 21 October 2009 (UTC)

I haven't reverted yet, but I'm in line -- nigh on two weeks I've been watching this bullshit with a baleful eye. Speaking for myself here: what I want out of this article is NOT a weird, un-historic "modern" proof, but rather a good list of references plus a high-class explanation of what Goedel was up to, and why (i.e. some historical context e.g. the effects of intuitionism on Goedel's proof method), and the consequences (historical and modern both). In this regard see a very good discussion (pp. 509ff) in Grattain-Guiness 2000. He lists 4 "effects" of Goedel's proofs: (1, 2) the effects of the theorem(s) on logicism and formalism, (3) "the use and potential of recursive functions, and of fintary proof methods", (4) "the necessity to distinguish rigidly meta- from object-, be it logic, language or theory -- and the difficulty often of doing so" (pp. 511-51). W.r.t. Halting problem, please don't hint at adding any freakin' proof that isn't already in the literature. Already I can produce two versions (Martin Davis in Sheen 1980:256, Minsky 1967:148) that are materially different from the one in the article. I believe I have in my archives the original Davis proof, too, plus there's Turing's proof that doesn't invoke halting at all. Maybe someone could create an expansion "alternate proofs" for the Halting Problem article, but again this must be done from published sources. Ditto for this article -- if there's an alternate proof in the literature, I don't know of it any excepting Goedel's simplified version of his Princeton lectures. Bill Wvbailey (talk) 17:57, 21 October 2009 (UTC)

(deindent) You are wrong, and I have explained this to you before, and I will explain it again:

Turing's proof is identical to the modern proof
Godel's proof is identical to the modern proof, with a slight change (shifting the self-reference from the computer program to the logical sentence)

The explanation of what Godel was up to is provided in the section that I added.Likebox (talk) 20:57, 21 October 2009 (UTC)

To arthur Rubin: you are speaking with words that sound like they make sense, but do not. The "beta function" does not belong on halting problem, because it has nothing to do with computation. It is just a way of extracting the prime exponent from an integer. The proof with "print your own code" only differs in syntax from the proof already on the page.Likebox (talk) 20:59, 21 October 2009 (UTC)

Modern version of Gödel's proof

Gödel's original proof of the incompleteness theorems has been considered difficult to read. The notion of a computer and a computer program were not yet defined in 1931, and the ideas of the proof involve computation in an essential way.

Given the basic ideas of modern computer science, the original presentation of Gödel simplifies enormously. The notion of "arithmetization of syntax" in modern terms is just the idea that any statement in a formal language can be written up in ASCII or Unicode, and in this representation becomes a sequence of bytes, or equivalently, a large integer. Any deduction algorithm can be written as a computer program, and is therefore a manipulation of integers. The program itself can be stored in memory, and its code is also a big integer. The first sections of Gödel's paper only show that the algorithm of logical deduction can be encoded within arithmetic, which is obvious today, since the algorithm of logical deduction can be programmed on a computer.

The memory contents of a computer is a large integer M, which is a long sequence of bytes, and for the purposes of the incompleteness theorem, M can become arbitrarily large during the course of the computation. So unlike a real computer, the idealized computer in the proof has an unlimited memory. Each processor step of the computer is a simple function which takes M to f(M), where the function f describes the instruction set of the computer. M includes the registers and the instruction pointer, which also must be allowed to be arbitarily large, and whatever special memory adresses you would like, corresponding to input and output devices. The function f in any computer will be primitive recursive.

The incompleteness theorem talks about an axiom system which is sufficiently strong, which Gödel takes to be the theory of Arithmetic in Principia Mathematica. The details of PM are not essential, the only property which is required of the theory is that it can describe an idealized computer. It is assumed that the axioms will prove every calculational theorem, it will eventually prove that the result of every finite computation is whatever it is. So that if f applied N times to M results in M', which can be verified by computing it, there is a theorem in the axiom system that

f^(N)(M) = f(f(f ...N-times...f(M))..) = M'

This theorem does not involve any quantifiers, and does not require any induction or infinite set theory. In the statement, N M, and M' are finite explicit integers, and f is an explicit computable function.

This means that if a computer program P working on input I produces an answer A in a finite time, the axioms are sufficient to follow the computation and prove this result. It is further assumed that the axioms are consistent, which means that they will never prove a statement and its negation. The last assumption is that the axioms can be listed by a computer program, so that there exists a computer program DEDUCE which will list out the axioms, and find all deductions in the theory by formal logic. A system whose axioms and deductions can be made by a computer program is called computable. Standard logic includes the quantifier "forall", so that a statement of the form "forall N f^N(M) does not produce 0 in memory location 0xFFEE" is a statement of the theory. This means that any statement about the eventual behavior of a computer program is easy to write down.

Under these assumptions, Gödel's first incompleteness theorem is:

Any consistent computable axiom system S that describes a computer has a Gödel sentence G. G is true as a statement about computations on integers, but G cannot be proved by S.

To construct the Gödel sentence G, consider the computer program SPITE:

1. SPITE prints its own code into a variable R

2. SPITE deduces all theorems of S, looking for the theorem "R does not halt".

3. If it finds this theorem, it halts.

Step 1 is not completely obvious--- a program which prints its own code sometimes requires effort to write. If the program does not have read access to its own code in memory, it must include its own code in a suitable way in the subroutine that prints out the code. The subroutine must then use a trick to avoid infinite self-reference, by copying the code variable and printing it twice. A program which prints its own code in this way is called a Quine.

Step 2 makes sense, because the statement "R does not halt" is a statement about computer programs, about integers, so it can be encoded in the language of S by assumption. It is a statement with one forall quantifier in front: forall N, "f^N(R) is not a halting state"

Step 3 is the interesting part: the program is looking for a theorem about itself. Step 3 guarantees that if it finds this theorem, it will do the opposite.

The Gödel sentence G for the theory S is "SPITE does not halt". If the theory proves this, then SPITE will halt in finite time, S will prove that SPITE halts, and this means that S has proved both a statement and its negation. So a consistent theory S will not prove "SPITE does not halt", and this means that SPITE will not halt. G is true, but unprovable.

Gödel's 1931 paper does not explicitly write a Quine. Instead, Gödel uses a peculiar property of sentences in first order logic with variables, which allows self-reference by a different looking trick. This trick was isolated by Kleene, and was later shown to be equivalent to writing a Quine within computer science. Von Neumann made the analogy between the self-reference involved in Gödel's proof and the replication of biological systems, since printing out your own code into a variable is the same as making a copy of yourself. He explored this type of computational self-replication further in his book The Theory of Self-reproducing Automata, a classic of cybernetics. The connection between the self-reference in Gödel's theorem, in biology, and in the process of artistic creativity was also explored in the popular book Gödel, Escher, Bach: An Eternal Golden Braid.

If written out in full, the sentence "SPITE does not halt" is complicated, involving many ideas that are not directly related to logic. After presenting his theorem, Von Neumann asked Gödel for a more elegant statement of the theorem, so that the basic limitation could be more clearly understood. After thinking it over, Gödel came up with the second incompleteness theorem:

Any consistent computable axiom system S describing a computer cannot prove its own consistency.

The previous argument shows that if SPITE halts if and only if S is inconsistent. So if the argument for the first incompleteness theorem can be formalized in S, then if S were to prove its own consistency, it would prove that SPITE does not halt.

The modern statement of Gödel's incompleteness theorem was not proved by Gödel in 1931, but by Rosser in 1936.

Any consistent computable axiom system S describing a computer is incomplete

This theorem is not proved by Gödel's method, because of a subtlety, first noticed by Gödel. Although S cannot consistently prove "SPITE does not halt", S could still prove "SPITE halts" without an explicit contradiction. If S is consistent, then "SPITE halts" is a lie, SPITE doesn't actually halt. But it's not an inconsistency unless S proves that "SPITE doesn't halt" too. There's no reason that S has to do this.

An S which proves "SPITE halts" is in the strange position of asserting that SPITE halts, while it in fact does not. Under the assumptions of the second incompleteness theorem, such an S asserts that it is inconsistent, when it is in fact consistent. Gödel called this type of theory omega inconsistent. The notion has been refined since then, so that the particular type of omega inconsistency involved here has a more specialized name, it is called sigma-one inconsistency.

Gödel's method proves that any omega-consistent (or even just sigma-one consistent) effective system S describing a computer is incomplete. Gödel's incompleteness theorem is also true for omega-inconsistent systems, but the argument is slightly more complicated. To prove incompleteness, construct the computer program ROSSER:

1. ROSSER prints its code into variable R

2. ROSSER deduces all the theorems of S, looking for either a) "R does not print to the screen" or the negation b) "R does print to the screen"

3. If it finds a), it prints "hello" to the screen, and halts. If it finds b), it halts without printing anything.

Since ROSSER halts either if it finds a) or if it finds b), S cannot consistently prove either the statement "ROSSER does not print to the screen", nor the negation "ROSSER does print to the screen". Either way, it would follow ROSSER until it halts, and then it would also prove the opposite. This was the first significant extension of Gödel's method, and it was formulated by Rosser in 1936, using Gödel's original arithmetization of the deduction methods of logic. In the same year, Turing developed the modern notion of computer, making Gödel's methods obsolete. Extensions of Godel's method continued in the 1950's, with the development of the method of injury priority.

Comments on the text

Let me point out, again, the reasons this should not be in the article. (Please do not put comments between my bullet points.)

"Any consistent computable axiom system S describing a computer is incomplete " is not the "modern statement of Gödel's incompleteness theorem". The modern statement would be something like, "No effective axiom system that is capable of representing every computable function can be both consistent and complete". (For the formal, precise definition of "representing a computable function", see diagonal lemma.) Moreover, the relationship between the incompleteness problems and computability was known at least by Kleene in the 1950s, so this is not a very "modern" statement.
The proof above ignores the main difficulty of the result, which is proving that "SPITE halts" is actually a sentence in the language of Peano arithmetic or other formal theories of arithmetic. Proving this requires, in every exposition I have seen, developing something like Gödel's β function to permit quantification over sequences, and defining something like Kleene's T predicate to capture computability in arithmetic.
- This omission is the key reason why the "proof" here is also a sketch, not a complete proof. Even if we tried to skip this by starting with the language of PRA, we would still need to prove, rigorously, that the function Likebox names f is actually a primitive recursive function, at least for some model of computation. This is essentially the same problem as constructing Kleene's T predicate.
In the section "Relationship_with_computability", we already have a short, simple proof sketch using the unsolvability of Hilbert's 10th problem. We also allude there to proofs that use the Kleene's T predicate, as Likebox's proof would if it were written in the usual manner.

There are also some expositional problems:

The proof blurs the distinction between an actual computer and a computable function. An actual computer has a finite memory and so can only be in a finite number of states. A RAM machine is a theoretical device that, while similar to an actual computer, is not the same, and so it is misleading to call it a "computer".
The text about von Neumann and Gödel begs for a source.
Priority arguments are not an "extension of Godel's method" in any visible sense. Priority arguments are used to obtain various sorts of incomplete r.e. sets, while Godel's method was used to construct an independent sentence in arithmetic.

— Carl (CBM · talk) 11:16, 19 October 2009 (UTC)

I mostly agree with the comments above. It is very important to stress that by a "computer", one means a RAM machine. The essential simplifications of the proof are due to using a RAM machine model of computation, which allows variables of arbitary size, rather than a Turing machine model, which is limited to a single input stream. The architecture of modern computers is, in my opinion, similar enough to a RAM machine that there is no danger in conflating the two notions a little bit. The only difference is that a RAM machine has unlimited size memory and unlimited size registers.

The distinctions you are making between "Any consistent computable axiom system S describing a computer is incomplete" and "No effective axiom system that is capable of representing every computable function can be both consistent and complete" is overpedantic, in my opinion.

"Computable axiom system" is a synonym for "effective axiom system", except replacing the word "computable" for "effective" or "one whose axioms are recursively" enumerable, which is encouraged by some modern writers. So this distinction is not a distinction.
"capable of representing every computable function" is the same as "describing a computer", except it is less immediately visualizable. To say that the axioms "describe a computer" means that for the given complete function f, the result of f(f...(f(..(M))...) = M' where M and M' are given integers and the iteration is of fixed length, is a theorem of the axiom system. I describe it in detail in the text, so there should be no confusion.
As for representing "f" in the axiomatic system of arithmetic, I gave a detailed response on your talk page, which I will copy and paste here.

From CBM's talk page (with some additions for clarity):

In primitive recursive arithmetic, there is nothing to do, of course. Any primitive recursive function f can be represented, including the instruction set of a RAM machine. In multiplication/addition Peano arithmetic, there is a little work. I was going to assume that the Godel beta-function is given, which means that you already know that the extraction of the prime exponent is allowed by first order logic and PA. If that needs justification, it can be spun into a separate article (this is some pages of Godel 1931). Once you have the beta-function, the point is that you only need one computationally complete function f, and you are done. You don't need any other PR function.

For example, a one-sentence embedding of a computer in arithmetic is using Cellular automata. For any nearest neighbor rule, you can write the operation in first order logic on PA as follows: the integer which stores the automaton is: 2^n3^a1 5^a2 7^a3 11^a4 ..., n is the current working location. The operation to extract the n-1-th exponent, the n-th exponent and the n+1-st exponent are expressible in the theory. Any finite transition table is expressible in the theory. Replacing the n-th quantity with the new value from looking up the transition table is expressible in the theory, and incrementing n by 1 is expressible in the theory. Also, you need rules to extend the automaton consistently, and to loop back once n reaches the end of the automaton. One way of doing this is adding a 1 at the end of the list every other step, and have an expression that if nth prime does not divide the integer storing the automaton, set n to 0.

From here on in, it's all reconstructing a Turing machine from automata, then reconstructing a RAM machine from a Turing machine. These are standard CS results, which can be referred to appropriate pages.Likebox (talk) 04:10, 16 October 2009 (UTC)

This is simpler than embedding the T predicate, because you don't need to focus on Turing machine as a model of computation. Cellular automata are easier to embed. The proof that a cellular automaton can describe a Turing machine, while a Turing machine can describe a RAM machine, is well known in CS. But even showing that the "f" for a RAM machine is primitive recursive is not hard.Likebox (talk) 20:53, 20 October 2009 (UTC)

about this comment: Priority arguments are not an "extension of Godel's method" in any visible sense. Priority arguments are used to obtain various sorts of incomplete r.e. sets, while Godel's method was used to construct an independent sentence in arithmetic.

This is true in the most literal minded sense: priority arguments are actually an extension of Turing's method. But since this discussion freely uses CS results without a big ado, the essential similarity between the method of Godel and that of Turing is emphasized. Godel himself would often say that Turing's methods made the language of recursive functions, which he himself had worked so hard to build, cumbersome and obsolete. In this sense, and in this sense only, priority arguments are similar to Godel's methods.

Given Turing's results, which are an outgrowth of Godel's results, and modern CS, the method of injury/priority extends the computer programs used in the proofs in nontrivial ways. Because these proofs are deeply computational, they are treated with difficulty and confusion in textbooks, and they are sometimes treated with suspicion in modern journals. This means that the proofs of priority theorems are not presented frequently, and they are not presented well. They are usually buried in obscurity. This is a historical injustice which is easy to rectify on Wikipedia--- just tell people what's really going on in terms of computer programs.Likebox (talk) 21:01, 20 October 2009 (UTC)

Proofs that use priority arguments are perfectly standard, and indeed very common, in recursion theory. Students in recursion theory are introduced to priority arguments early and often (see the TOC of Soare's Recursively enumerable sets and degrees, the standard contemporary textbook). Talks about recursion theory results typically describe exactly what sort of priority argument is used in the proof even when the proof itself is not presented. So priority arguments are in no way "buried in obscurity". However, even if there were an historical injustice, Wikipedia is not the place to rectify it. — Carl (CBM · talk) 00:09, 21 October 2009 (UTC)

I agree that there are many people who understand injury/priority well enough to work with it. However they are all specialists in the field. The knowledge has definitely not percolated out of this small community, and this makes it obscure, in the way that, say, Ricci flow is not. This is a great pity, because the methods should not be obscure--- everybody should know this, the same way everybody knows what a Hilbert space is.

I learned all this stuff from Soare, so you don't need to point me to him. It was because his presentation is so obtuse that I started editing this page. The injury/priority arguments are swept under the rug, and written in incomprehensible ways, precisely because none of the mathematicians want to put something that looks like a computer program in a proofs. This makes the injury/priority results obfuscated to the point where a nonspecialist has absolutely no hope of understanding them.

I believe that the core mission of Wikipedia is to clarify results, where possible. For injury/priority, this can be done to the point of hit-me-over-the-head-because-it's-so-obvious.Likebox (talk) 00:49, 21 October 2009 (UTC)

You are arguing that Ricci flow is commonly understood by non-specialists?

Soare hardly sweeps priority arguments "under the rug", when the majority of the text is devoted to them. Actually, there is a more contemporary way of looking at priority arguments, in terms of trees, which is often taught in recursion theory classes these days. But this method is postponed quite late by Soare's book (chapter XIV), although he says that if he rewrites the book he may change that. — Carl (CBM · talk) 01:08, 21 October 2009 (UTC)

Ricci flow was developed in mathematics and within string theory at almost the same time, and so is accessible to non-specialists from either field. The language is no more complicated than it needs to be, and it is easy to get used to.

On the other hand, the priority arguments in Soare's presentation (and everyone else's) are needlessly obscure. Here is a sample of Soare's writing on Post's argument about simplicity:

"Fix a recursive enumeration {a_s}s\in W of the r.e. set A={<e,x>: x\in W_e & x>2e}. Define an r.e. set B \subset A by enumerating a_s = <e,x> into B if there is no a_t =<e,y> for t<s and y \ne x. Since B is single valued, it represents the graph of some partial recursive (p.r.) function \psi; i.e. \psi(x)=y iff <x,y> \in B. Let S=range \psi. (intuitively, enumerate W_e until the first element \psi(e)>2e appears in W_e and then put \psi(e) into S.)"

To be fair, the pairing function <,>, the code e, the recursive function W_e, are all standard, and once you get used to the notation, it is not impossible to decode what he is saying, and to verify that it is the same as the "intuitive" statement in parentheses. Also to be fair, this is from the published literature, not a textbook, and is pretty comprehensible compared to textbook treatments.

Here's a translation to computational language:

Any routine which takes an integer and returns an integer is called a recursive function. In C-ish code, the declaration is "integer R(integer){code}". The code of the program will be called "R", and it is a largish integer in memory, which, when it is thought of as an integer, will be called [R].

A set of integers (or codes) is recursively enumerable (r.e.) or computably enumerable (c.e.) if there is a computer program which outputs all them eventually, in any order.

A set S is simple when there are infinitely many integers which are not in S, but only finitely many of them can be printed out by a computer program. To define a simple recursively enumerable set:

loop over all codes R which define recursive functions
for each R, loop over all possible inputs x
run each R with input x on a separate thread, with the condition that if R(x) returns an answer, and if this answer is bigger than 2[R], then print this answer out, and shut down all the other R threads.

This program prints out a set of numbers, and any R produces at most one output, which by necessity is greater than 2[R]. So in the interval 1,2,3...N, there are at most N/2 outputs. The list of outputs S has infinitely many numbers missing, and these missing numbers have density greater than 1/2 in the integers.

Still, even though more than half of all numbers are missing from S, it is impossible to print out more than finitely many of them with a computer program. The reason is that any program that lists infinitely many numbers can be made into a function "integer R(integer)" which takes as input the integer I and returns the I'th listed number. If this R returns infinitely many answers, one of the answers will be bigger than 2[R], and this answer will already be included in S, it will not be missing from S.

Why doesn't Soare say it this way? First, he pretty much does. This is a straightforward translation of his proof to common language. But this language is not acceptable within this literature, because every author is playing a game of "hide the computation". By using obscure notation, the proofs are made to look like those of other branches of mathematics, with sets and fixed points, as opposed to computer science, with programs and outputs.Likebox (talk) 02:57, 21 October 2009 (UTC)

I don't have any difficulty reading the quote from Soare. For example, when he says, "Define an r.e. set B \subset A by enumerating a_s = <e,x> into B if there is no a_t =<e,y> for t<s and y \ne x.", he is explicitly saying how to do a computation. Nothing is hidden. The focus on sets is due to the fact that classical recursion theory is the study of sets of natural numbers and computable functions between them, not the study of computer programs. — Carl (CBM · talk) 10:57, 21 October 2009 (UTC)

(deindent) You don't have any difficulty reading the quote from Soare, but I do, and so do most people, including students of all levels, and nonspecialists. It would take me about 20 minutes of translation to decode that paragraph and turn it into an algorithm. I am not going to go along with this silly substitution-cypher method of writing. If you want all your computations to be presented in rot-13, then go ahead and write it that way. I will write the same thing in english.

Since the content is unchanged, the one which is understandable by the broadest majority of people should be favored. Your assertion that classical recursion theory is the "study of sets of natural numbers" is absurd, since "computer programs" define the "computable functions between them" that are the real subject of study.Likebox (talk) 20:50, 21 October 2009 (UTC)

You said, "The proof that a cellular automaton can describe a Turing machine, while a Turing machine can describe a RAM machine, is well known in CS.". But the whole proof of the incompleteness theorem is well known in CS; this doesn't mean one can simply replace the proof with "This is well known." The point of a complete proof is that everything is proved.

It seems you are saying that we can simplify the proof of the incompleteness theorem by replacing the arithmetization of formulas with the arithmetization of cellular automata (which will still require something akin to the β function), and then adding the representation of Turing machines via automata (which requires a correctness proof), and then the representation of RAM machines via Turing machines (which also requires a correctness proof). And you are claiming that the combination of all those proofs is somehow shorter than just proving the results about arithmetization of formulas? — Carl (CBM · talk) 00:09, 21 October 2009 (UTC)

It's not exactly that. The arithmetization of cellular automata can be done in several ways, and I haven't given much thought to which way is best. It depends on the exact way in which arithmetic is axiomatized. Proofs that cellular automata include computation, that any computer's instruction set is a simple primitive recursive function which can be formally described in first order arithmetic, are conceptually straightforward today. It is the construction of the Godel sentence itself which is interesting.

In that regard, using "G asserts that it is unprovable" is problematic, because in order to formalize that sentence, you need a way for G to talk about itself within first order logic, which requires mucking around with logic to the point where you are comfortable with free variables. The first simplification is to make sure G only talks about computer programs, and that the computer programs do all the self-referencing.

This is in fact the proof which you have presented here, the one that uses the T predicate to say "If an arithmetic were consistent, complete, and correct, then it would solve the halting problem". This is enough to make the general idea of Godel's original theorem clear. The version I am suggesting simply folds in the proof of undecidability to make a self-contained exposition.

To prove Rosser's theorem in the same way requires a modification. I am not going to tell you what it is, though, because I expect you would then just put it in and say "I prove Rosser's theorem, we don't need new proofs".

All proofs involve trade offs about what to explicitly show and what to leave as an exercise for the reader. But what the reader knows changes from era to era. In the modern era, the statement that a computer's instruction set can be represented explicitly by a first order arithmetic sentence is blindingly obvious, but recursion theoretic constructions of fixed points are obscure.

The black boxes which we have inherited from previous generations are the fixed point theorem, the T predicate, and logical deduction. I am suggesting that a more conceptually straighforward collection of black boxes is modern computation (RAM machines), logical deduction, and "print your own code" for a RAM machine (equivalent to the fixed point theorem). The change is miniscule, superficial really, but the presentation is easier for some people to understand.Likebox (talk) 00:40, 21 October 2009 (UTC)

You said, "Proofs that cellular automata include computation, that any computer's instruction set is a simple primitive recursive function which can be formally described in first order arithmetic, are conceptually straightforward today." This is true, but proofs of the arithmetization of syntax withing theories of arithmetic are equally conceptually straightforward. There's nothing that is truly surprising in either case (apart from the number theory needed to prove that the β function works, which is also needed in your proof). On the other hand, if it really were conceptually simpler to work with computer programs, you would think that the literature would do it that way.

My experience with students is that "a computer's instruction set can be represented explicitly by a first order arithmetic sentence" is not blindingly obvious. If I ask them how one would go about actually writing such a sentence in the language of Peano arithmetic, they would not be able to just rattle it off the top of their head. Indeed, even though I know how to do it, it would take me quite a while to explain how one would go about formalizing the T predicate in Peano arithmetic. — Carl (CBM · talk) 01:08, 21 October 2009 (UTC)

The whole literature does work that way. They just don't bother to tell you what they are doing. That's what annoys me.

As far as students go, I urge you to take a poll. Present the proofs side by side, and see which one produces understanding. I know the answer already.Likebox (talk) 05:33, 21 October 2009 (UTC)

break: on Rogers

Have you read the section of Rogers' book about the informal use of Church's thesis to argue that particular functions are computable? — Carl (CBM · talk) 10:57, 21 October 2009 (UTC)

No I haven't, but from the title it seems irrelevant to the discussion.Likebox (talk) 20:46, 21 October 2009 (UTC)

Really. That section is somewhat a manifesto for the change in technique in recursion theory, from a very formalized style where all details of programs were written out, to a more informal style. From Rogers 1967 §1.7:

In recent theoretical work, the phrase "Church's thesis" has come to play a somewhat broader role than that indicated above. In Parts II and III of the Basic Result, we noted that a number of powerful techniques have been developed for showing that partial functions with informal algorithms are in fact partial recursive and for going from an informal set of instructions to a formal set of instructions. These techniques have been developed to a point where (a) a mathematician can recognize whether or not an alleged informal algorithm provides a partial recursive function, ... (b) a logician can go from an informal definition for an algorithm to a formal definition. ... Recursive-function theory, of course, deals with a precise subject matter: the class of partial functions defined in §1.5. Researchers in the area, however, have been using informal methods with increasing confidence. We shall rely heavily on such methods in this book. They allow us to avoid cumbersome detail and to isolate crucial mathematical ideas from a background of routine manipulation. ... Such proofs will be called proofs by Church's Thesis.

It is worthwhile to read the entire section, actually. Rogers' opinion there was extremely influential in recursion theory. It is what Soare is alluding to in Recursively enumerable sets and degrees, p. 15:

From now on we shall describe an algorithm for a recursive function in ordinary mathematical terms and leave it to the reader to convince himself that this algorithm could be translated into one of the formalisms above. Such a demonstration will be called a "proof by Church's Thesis".

As Rogers says, the point is not to obscure the computational content, but to focus on the mathematical content instead of routine matters relating to specific models of computation. — Carl (CBM · talk) 21:07, 21 October 2009 (UTC)

I am familiar with this thread in the literature. It would be nice if the algorithm description was actually made informally, the way a computer programmer describes algorithms. But in reality, the "informal description of algorithm" is not really made informal by Soare, it is left partially encoded in the language of recursive sets (see the quote from Soare). The result requires laborious translation back and forth to understand the algorithm and to see how it proves the result. There is absolutely no gain, neither in precision, nor in clarity, by using this jargon. The precision is the same as that of an algorithm stated in english.

I didn't like the way that they call this business "Church's thesis", because the content of Church's thesis is slightly more physical and real. Church was saying that any computable function in nature is a computable function on a Turing machine. This is a statement about the laws of physics, what type of computations these allow, not so much about the simple specific algorithms that are the subject of "proof by Church's thesis". The physical content of Church's thesis here is identified with a mass of trivialities--- like the fact that a specific algorithms like that in Post's proof can be programmed on a computer. Any specific algorithm can be programmed on a computer, and for any given algorithm, this isn't Church's thesis, but an obvious exercise in translation. Church's thesis states that an arbitrary process which produces a definite answer can be programmed on a computer. It is essentially the statement that any physical process can be simulated on a Turing machine.

But quibbles aside, the text above doesn't adress the question of how informal algorithms should be presented. Should they be presented as sets and recursive functions, or as pseudo-code?Likebox (talk) 21:42, 21 October 2009 (UTC)

For the purposes of Wikipedia, all that matters is how they are presented in the literature. Apparently people who are more familiar with recursion theory feel their way is better for some reason. Simply because you feel, as a matter of personal opinion, that the literature is poorly written, does not mean it is so. Wikipedia doesn't even permit experts to get by solely on personal opinion. — Carl (CBM · talk) 22:49, 21 October 2009 (UTC)

This is a question of policy. You are right that on Wikipedia you don't get to invent new results, but there is no reason that you can't simplify existing discussions by de-jargoning them and presenting them in straightforward language. This is important for literature that is opaque. It is not reasonable to make a policy that clarifying text is to be deleted.Likebox (talk) 01:25, 22 October 2009 (UTC)

(deindent) As far as the literature about Rogers' approach, Shoenfield says exactly what I said above. He calls the use of Church's thesis for a specific algorithm "inessential", and points out the whenever it is used in recursion theory to turn an informal algorithm into a recursive function that this is an "inessential use" (what he means is that it is possible to write the code explicitly and in this way avoid invoking Church's thesis). The "essential" use of Church's thesis is when you argue that any computable function in a recursive function, and this is difficult to make precise with examples, precisely because it is obviously true.

One way of having a violation of Church's thesis within Newtonian mechanics is by building "halving machines". You build a machine to test case 1 of the halting problem, then build a machine half as big that runs twice as fast to check test case 2 of the halting problem, and build a machine half as big that runs twice as fast to check test case 3 etc. This will produce a solution to the halting problem in finite time, assuming an appropriate Newtonian mechanics for point particles. You need the appropriate force laws to allow halving machines (1/r potentials are probably enough, because they obey a time-distance scaling law for the orbits and are likely sufficient to build a Turing machine, but you might need other force laws to stabilize the orbits, so that the computation is stable to small deformations). Of course, in our universe, the laws of physics prevent these kinds of shenanigans in infinitesimal regions or using infinite volumes because of the restrictions posed by quantum mechanics and relativity.Likebox (talk) 19:06, 22 October 2009 (UTC)

Shoenfield also presents recursion theory with register machines, which are closer to RAM machines than to Turing machines. The simplification in his presentation is considerable as contrasted with Soare.Likebox (talk) 21:56, 22 October 2009 (UTC)

I also should point out that halving machines require infinitely many particles which can communicate in finite time, to allow for infinite memory. This is doable if you have no speed limit, because you can use Newtonian particles to zip around very fast between far-away regions, so that they compute more and more in shorter and shorter times. Relativity forbids this in real life.Likebox (talk) 22:24, 22 October 2009 (UTC)

You misunderstood the quote from Rogers. In the mid 20th century, recursion theory proofs would usually explicitly prove that various functions were computable, by presenting instructions in particular models of computation. This is very similar to your idea of adding pseudocode to the proofs here. Rogers' text (1967) was part of a change towards a different proof style where, instead of explicitly presenting code, the proofs simply describe how to compute something using normal mathematical English, and the reader is left to verify that the description actually gives a computable function. As Rogers says, proofs of this sort "allow us to avoid cumbersome detail and to isolate crucial mathematical ideas from a background of routine manipulation." This change was quickly adopted by the recursion theory community because they found it a superior way to present proofs. It's great that you feel that the entire field of recursion theory was wrong to move in this way, but (as I said) not even experts are permitted to edit based solely on their personal opinion. — Carl (CBM · talk) 02:11, 23 October 2009 (UTC)

I don't think I misunderstood Rogers. I agree with your assessment of what was happening, but where you say "normal mathematical english" (which is what Shoenfield uses) you are including radically different styles, ranging from the impenetrable to the lucid. I agree that the algorithm descriptions are important.

On a different tack, I can prove a theorem by these methods that might be new. I am not sure, so I will run it by logicians to see if it is in fact new. If there is a new result which can be understood this way, the method might have a small amount of originality. Although for standard results (like Godel's theorem) it is just a rehash of Kleene.Likebox (talk) 22:16, 23 October 2009 (UTC)

Upon rereading your comments, it finally dawned on me what you are saying. You think that, way back when, it was traditional to present computer programs explicitly with code. Then, there was a shift, and suddenly it was OK to present the computer programs informally, in english, and this is what the literature does today.

This is a pure myth, which I heard in recursion theory classes, but which does not reflect the actual literature. The original literature is precise about algorithms at exactly one point. That is when Godel was defining recursive functions, and Church was defining expressions in lambda calculus. Even Godel and Church don't spell out every line of their codes. The only person who wrote code detailed enough to be debugged was Turing. Already starting with Post, long before Rogers, informal algorithm description was OK.

The real story here is that recursion theory decided to standardize its language around recursive sets, as opposed to programs, with heavy handed conventions for what code is supposed to look like (it looks like phi(e)). This was a shift in language from the informal description of algorithms to equally informal description of algorithms in infantile jargon. Within the field, people describe programs in a bunch of different ways, all of which are vastly more informal than any programming language. Algorithms should be described here as informally as possible, so that the widest possible audience can understand what they are doing.Likebox (talk) 19:01, 27 October 2009 (UTC)

Von Neumann and the Second Incompletness Theorem

On page 200 of "recursive functions and metamathematics" by Roman Murawski, there appears the following account of the Konigsberg conference of 1930, where Godel presented his results:

John von Neumann (1903-1957) seems to be the only participant of the conference in Konigsberg who grasped the meaning of Godel's theorem. After Godel's talk, he had a long discussion with him and asked him about details of the proof. Soon after coming back from the conference to Berlin he wrote a letter to Godel (on 20th November 1930) in which he announced that he had received a remarkable corrolary from Godel's First Theorem, namely a theorem on the unprovability of the consistency of arithmetic in arithmetic itself. In the meantime Godel developed his second Incompleteness Theorem and included it in his paper "Uber formal unentscheidbare Satze...".

So that's the source for the claim in the text.

Likebox (talk) 01:05, 23 October 2009 (UTC)

formalizations

I added some cites of a couple of noteworthy formalized proofs of the incompleteness theorem, which I hope are appropriate for here. Shankar's was the first formalization of any version of the theorem, while O'Connor's is the first to actually prove the incompleteness of arithmetic (Shankar's is about the hereditarily finite set theory Z2). I think there may also be a HOL Light one by Harrison from 2008 but I can't find a cite. O'Connor refers to a 2005 proof by Harrison of something that seems a bit different and I think that's also what Wiedijk's article [12] refers to. Maybe it should go here. The current HOL manual mentions a proof of the incompleteness theorem for arithmetic and also Tarski's undefinability theorem, but I haven't looked further. 69.228.171.150 (talk) 15:35, 24 October 2009 (UTC)

^ Carl Hewitt, Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency in Coordination, Organizations, Institutions, and Norms in Agent Systems III, Springer-Verlag, 2008.
^ Solomon Feferman, Toward Useful Type-Free Theories, I, Journal of Symbolic Logic, v. 49 n. 1 (March 1984), pp. 75–111.

[Hewitt2008-1] Carl Hewitt, Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency in Coordination, Organizations, Institutions, and Norms in Agent Systems III, Springer-Verlag, 2008.

[Feferman1984-2] Solomon Feferman, Toward Useful Type-Free Theories, I, Journal of Symbolic Logic, v. 49 n. 1 (March 1984), pp. 75–111.

[1]

[2]