Misplaced Pages

Revision as of 20:48, 14 November 2007

Mathematics Unassessed Top‑priority

This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Misplaced Pages. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics ??? This article has not yet received a rating on Misplaced Pages's content assessment scale. Top This article has been rated as Top-priority on the project's priority scale.

Philosophy: Epistemology / Logic Unassessed

This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to philosophy on Misplaced Pages. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Misplaced Pages.PhilosophyWikipedia:WikiProject PhilosophyTemplate:WikiProject PhilosophyPhilosophy ??? This article has not yet received a rating on Misplaced Pages's content assessment scale. ??? This article has not yet received a rating on the project's importance scale. Associated task forces: /  Epistemology Logic

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

Archives

/Archive01 /Archive02 /Archive03

Modern Proof

Recently User:CeilingCrash removed the "Modern Proof" section, without (as far as I can tell) discussion on the talk page. He included a detailed comment for why he removed it, but I think it the edit should first be discussed on the talk page. To make sure everyone agrees that the proof is in fact bad before removing it. --DFRussia 11:54, 1 November 2007 (UTC)

I agree with removing that section, and I removed it again. That section didn't actually provide a proof - it instead gave a vague argument about "computer programs". It was alluding to a correct proof using the diagonal lemma, but such a proof would need to be written using the correct terminology (representability of computable functions, etc.) rather than vague statements such as "and that it has enough operations (addition and multiplication are sufficient) to describe the working of a computer." The supposed proof of the second incompleteness theorem was "To prove the second incompleteness theorem, note that the consistency of the axioms proves that DEDUCE does not halt, so the axiom system cannot prove its own consistency" which completely ignores the actual issue there, which is the arithmetization of proof.

This is not ignored. The arithmetization is sidestepped by using a modern computer, where arithmetization is automatic and a part of day-to-day life. It's ASCII and unicode.Likebox 21:53, 1 November 2007 (UTC)

I don't know whether we need a proof via the diagonal lemma in this article; we can discuss that. But if we are going to claim something is a proof it needs to actually prove something. — Carl (CBM · talk) 13:20, 1 November 2007 (UTC)

The proof is complete and correct, as others have verified. Please check the previous discussions first.Likebox 21:53, 1 November 2007 (UTC)

Ceilingcrash is correct -- both Turing and Church used the notion of arithmetization in their proofs. It is this plus Godel's use of a fully-specified proof system plus the "shift from "true" to "provable"" (to quote van Heijenoort) that, e.g. distinguished Godel's proof from Finsler's uncacceptable proof (1926). Whereas these key notions are probably understandable by most lay readers who've come to this article, where and exactly how the diagonal argument enters is absolutely obscure ... At least for me ... I know it's embedded in the "first" theorem somewhere, but I haven't been able to trace the exact steps because of Godel's difficult presentation: it's discussed in Rosser (1939?) but I haven't gotten that far. There's no doubt that Turing's argument is easier to follow for computer-science folks: his machine busily creates diagonal numbers from its "decider algorithm" working on numbers-as-programs until it fails to do so when its "decider" hits its own number to test. Yes, I would like to see more about the incompleteness theorems' diagonalization in this article. Bill Wvbailey 17:56, 1 November 2007 (UTC)

DFRussia was right, i shd have brought the issue up here first. The crux of my argument is that the C-T came some years after G, and uses G's most critical innovations. By using the C-T as a Lemma, we have smuggled in G, which of course makes G easy to then prove, but seems (to me) to mis-attribute the idea and is tail-chasing.

About diagonalization, I agree w/ WvB that the diagonalization trick is a quite vivid way to get incompleteness. (An ancestor of the technique can be seen in Cantor, to prove certain elements are not contained in a lower order of Infinity.) I don't think Godel expressed his argument this way, he finds the 'smoking gun' by beefing up the formal system with some elements of a programming language : string manipulation operators like substitute, concatenate, mapping of godel-number to symbol, etc. Once he has this, he has theorems which can make build theorems, and make assertions about their provability. Finally, he builds a theorem (G) which denies its own provability. An interesting exercise gives a gist of how this axiomatic "introspection" can be achieved :

In any programming language, write a program that prints out precisely its own source code (without resorting to tricks like reading the source from disk or memory.) Hint, you have to be clever about string substitutions, and it is permissible to ASCII codes to generate characters. Anyone who does this will readily understand how Godel made G.

I too would like to see if someone has recast Godel's argument using the diagonalization trick, which is so vivid and comprehensible. updated CeilingCrash 18:42, 1 November 2007 (UTC) 2007 (UTC)

I have edited the proof sketch to emphasize the diagonalization more, and to explicitly use the diagonal lemma. I think breaking that out of the sketch here is good, since it allows the reader to ignore how that formula is constructed for a while when reading this proof, and later investigate the proof of the diagonal lemma. Please let me know what you think; I'm done for this afternoon. — Carl (CBM · talk) 19:09, 1 November 2007 (UTC)|

Hat's off to CBM ! This is very nice indeed. Godel's creation of G is constructive, which is nice, because we get to see exactly what it is. But it is subtle and very difficult to follow. The diagonal argument proves existence - which is all we really need for incompleteness - and much easier to follow. Well done and thank you! (I added Hilbert's 10th problem to the examples just now.) CeilingCrash 19:53, 1 November 2007 (UTC)

Hopefully I did't offend anyone with my original roll-back. I am glad there is now an active discussion. You guys seem to have made a lot of progress on the article over the last hours. Well done --DFRussia 20:58, 1 November 2007 (UTC)

(deindent) Hello, I reinserted modern proof, and I would like to adress the objections raised. First of all, the argument is self-contained. It only uses the "Church-Turing" thesis to argue that formal logic is a computer program, which is not the general Church-Turing thesis, but a special obvious case. The argument is simplified by black-boxing the process of quining, which is an exercise in modern CS curriculum. The argument is otherwise complete. It is designed to be both correct and comprehensible to anyone who knows how to program a computer. It is in my opinion ridiculous to leave out such a simple proof, which is essentially equivalent to Godel and Rosser but much much easier to understand.Likebox 21:38, 1 November 2007 (UTC)

In response to the previous comments--- the persons who wrote them probably don't like this proof, because they have their own favorite proof. This is fine, there is no reason not to have multiple proofs. But there should be no dispute about the correctness of the argument. I included it precisely because it is the shortest, clearest proof.Likebox 21:53, 1 November 2007 (UTC)

Please don't be offended, Likebox, but we have consensus with myself, Wvbailey, and (implied anyway)CBM, who went to the trouble of retrieving the baby from the bathwater (the diagonal lemma) and reworking the Sketch Argument. Our objections to the Modern Proof are not stylistic, they substantive and listed in this discussion. Also, absent a source for it, it is Original Research. Long story short, Church-Turing based their work on Godel, not the other way around. I will roll back the inclusion re consensus, I hope not to spark an edit war.

Can you point us to a source for this version of the proof?CeilingCrash 22:44, 1 November 2007 (UTC)

(added) On second reading, it is a very elegant way to get at GIT, and it would be nice to retain this exposition in some form. It's not clear to me that we should call it a modern *proof*, since certain notions such as Quining and the fact a program can always print itself, would require expanding - and this expansion would lead us right back to godel (or an imitation thereof.)

I think if we retitle this section as something to the effect of, "GIT as seen from an algorithmic point of view", and note that some of these notions - so pedestrian today - owe their genesis to godel, it would be nice section to keep. Basically, if we don't call it a proof i'm cool. Others?CeilingCrash 23:11, 1 November 2007 (UTC)

The source is cited, although this discussion expands a little. The objections are not so substantive. They are right about the history, of course. But this is 2007 after all, not 1931. I am not at all offended, just puzzled. Why do you folks not like it? I really want people to understand Godel's theorem, and I am worried that current expositions are too bogged down in stupid details like arithmetization. This makes it very difficult for nonspecialists. I think every human being should understand Godel's theorem completely.Likebox 23:27, 1 November 2007 (UTC)

(Likebox and I got into an edit conflict.) I must confess to having judged this section too quickly. It is stunningly clear and beautiful, and on closer inspection I cannot substantively object to any part of it. (Upon first reading I thought CT was assumed in its entirety.) I wd be happy to see this text included, with the proviso that certain of these notions originated with godel (however commonplace and obvious to us today.) My apologies to Likebox. I would like to see certain bits expanded upon via link, for example to quining and to self-generating programs, i'd be happy to add these links to the text.

Oh - a few years ago I wrote a self-printing program in C and showed a printout to my coworker. He asked, "is that the source or the output?" At that moment, I achieved enlightenment :-b CeilingCrash 23:39, 1 November 2007 (UTC)

Thanks CeilingCrash. I incorporated a sentence that hopefully adresses your concerns.Likebox 23:44, 1 November 2007 (UTC)

My objection (not a strong one) is that a demonstration via machine computation smears two historically-separable events -- (i) a consistency proof re "arithmetic" versus (ii) an undecidability proof re an answer to the Entscheidungsproblem. Here's my understanding of what happened back then (ca 1930's):

Godel demonstrated (via his "1st" theorem VI) that undecidable "objects" existed, but he had not produced a specific "effectively-computable object" inside his formal system for our observation and amusement. (He was working with "proof systems", not "calculations/computations"). Thus Godel put to rest the Hilbert question of consistency, but the Hilbert question around the Entscheidungsproblem had to wait until the notion of "effectively calculable" was defined enough to proceed.

Church (1934) and Turing (1936-7), had to do two things: (1) define precisely the intuitive notion of "effectively calculable", and then (2) within a formal system and using their notions of "effectively-calculable", produce an "object" that would be, indeed, "undecidable". Church defined a notion of "algorithm" (lambda-calculus computations) and produced an "algorithmic object" that was "undecidable", but he worried about his proof (and soon emended it)). Turing, on the other hand, produced an indisputably "effectively-computable object" (a machine and an undecidable computation to be done by said machine) that even Godel accepted (in the 1960's) as the sine qua non. The consensus is that Godel could have easily gone the extra last step, defined "effectively computable" (for his purposes), and put an end to the Entscheidungsproblem once and for all, but he was just bored with the whole thing and went on to other stuff...

What we don't want to do is mix up the reader with respect to these various "Hilbert problems". When introduced into Godel's proof, machine computations add this other dimension ("effectively calculable"). At least that's my interpretation of the crux of the problem. It's not that a great machine-based demo can't offered, it's that such a demo may cause confusion. If anything such stuff should go into Turing's proof. Bill Wvbailey 00:55, 2 November 2007 (UTC)

I agree with your sentiment, although not with the conclusion. It is a major historical fib to claim that undecidability preceded incompleteness. But it is a shame to not use undecidability to prove incompleteness, because it makes the proof short and comprehensible. The section made no pretense of being historical, it was just a proof of the theorem using modern notions of computability that everyone recognizes. Perhaps a sentence pointing out that the section is ahistorical would be enough. Likebox 20:09, 5 November 2007 (UTC)

"Everyone" meaning computer programmers, right? I agree that readability by nonmathematicians is a worthy goal. But I have a difficult time calling it a proof, because it is so vague and handwavy about important details (like what language are the programs coded in, how are the desired program transformations coded, and is that language capable of addressing unbounded amounts of memory). —David Eppstein 20:14, 5 November 2007 (UTC)

"Modern proof"

This section is full of things that are either incorrect, completely vague, use the wrong or nonstandard language, or absurd. Examples:

"Assuming that a computer exists, and that formal logic can be represented as a computer program"

Of course a computer exists! But Godel's theorem is not about physical computers. Moreover, it makes no sense to say "represent formal logic as a computer program".

You might not be familiar with the completeness theorem. Godel's completeness theorem is an explicit algorithm to write down all deductions following from a given set of axioms. The algorithm is explicit, and can be written as a computer program. The only "nonphysical" thing about the computer required is the fact that it has infinite memory. That's the only idealization to go from a regular ordinary computer to a Turing machine.Likebox 20:34, 5 November 2007 (UTC)

The Quine lemma

The actual name of the needed result is the recursion theorem. Quines are just one application of the recursion theorem. The result below does not actually follow from quines, but from an application of the recursion theorem. In shor,t this is just wrong.

No it isn't. The recursion theorem is not the quine lemma, it is a confusing piece of obviousness required to prove that quines exist in recursion theory language. In computer science language there is no need for a proof, because you can easily write an explicit quine. The whole point of this proof is to avoid the recursion theorem.Likebox 20:34, 5 November 2007 (UTC)

The Halting lemma: There does not exist a computer program PREDICT(P)

There no such thing as the "Halting lemma". This is completely nonstandard terminology. There is a result relating to the halting problem, which is usually phrased as "the halting problem is unsolvable."

If you notice, the proof does not use the actual halting lemma. This is just presented as motivation.

proof: Write DEDUCE to deduce all consequences of the axiom system.

How is it supposed to do this? Most of an actual proof is spent achieving this!

It does this by the completness theorem. Godel did not prove this in any explicit way, and neither do any modern treatments. This proof is no better and no worse in that regard. Godel just listed a bunch of different algorithms which could be used to make a deduction program, and noted that they are all primitive recursive. Godel stopped writing down algorithms after a certain point, because it was too tedious, and he just noted "the rest of this requires writing a primitive recursive function to do this and this and this", where "this and this and this" is the rest of the algorithm of the completeness theorem. This proof just says flat out "There is an algorithm for deducing consequences of axioms", and does not bother to write any code. The difficulty in Godel's original proof is in the arithmetization, which is required because he did not know what a computer is, and in the quining, which he avoided by a trick.Likebox 20:34, 5 November 2007 (UTC)

Let DEDUCE print its own code into the variable R,

But DEDUCE is already defined - this is a second, different program.

DEDUCE first prints its code into R, then deduces all consequences of the axioms looking for the theorem R does not halt. It halts if it finds this theorem.Likebox 20:34, 5 November 2007 (UTC)

If the axiom system proves that DEDUCE doesn't halt, it is inconsistent. If the system is consistent, DEDUCE doesn't halt and the axioms cannot prove it.

Why? This is another thing that requires explicit justification but is presented with none.

The moment that the axioms prove that R does not halt, DEDUCE halts. Since the axioms can also calculate the finite-time state of DEDUCE, they can follow the operations of the computer program, this means that the axioms also prove that DEDUCE halts. That's a contradiction. So the axioms cannot prove that DEDUCE does not halt.Likebox 20:34, 5 November 2007 (UTC)

The assumption is that the axioms can follow the finite time operation of any computer program. This is an assumption in Godel's paper, where he asks that the value of any primitive recursive function can be calculated correctly by the axiom system. In other words, for any primitive recursive function f, the theorem F(n) = the number F(n) is a finite time deduction of the axiom system. This is true in PA, so he just assumes that PA is embedded in the system. The point of PA is only that the value of any primitive recursive function will eventually be calculated at some point in time as a theorem.Likebox 20:34, 5 November 2007 (UTC)

If the axiom system is consistent, it cannot prove either ROSSER eventually prints something nor the negation ROSSER does not print anything. So whatever its conclusions about DEDUCE, the axiom system is incomplete.

This, again, is just a restatement of what is supposed to be proved.

No it isn't. It's a proof. ROSSER prints its code into R, and looks for theorems about its behavior. If it finds a theorem that says "You do this" it does "not this". If it finds a theorem that says "You do not do this" it does "this". This is exactly ROSSER's argument for avoiding the omega-consistency issues, translated into modern language.Likebox 20:34, 5 November 2007 (UTC)

To prove the second incompleteness theorem, note that the consistency of the axioms proves that DEDUCE does not halt, so the axiom system cannot prove its own consistency

This "noting" does not prove the second incompleteness theorem, which requires a great deal of effort to prove.

It only requires a great deal of effort if you do not understand it. If you understand it, it is obvious. There do not exist theorems which "require a great deal of effort to prove". Either you get it or you don't.Likebox 20:34, 5 November 2007 (UTC)

R. Maimon "The Computational Theory of Biological Function I", arXiv:q-bio/0503028

The reference is an unpublished paper in the arxiv, not any sort of respected logic text.

Respectibility is a political decision. it requires a vote.Likebox 20:34, 5 November 2007 (UTC)

In short, this "modern proof" could only be salvaged by completely rewriting it. But there is already a proof sketch in the article, and if this one were fixed there would be two proof sketches. In any case, the current state of this section is embarrassing;it claims to be a proof but is just handwaving. Removing the section is the right thing to do. — Carl (CBM · talk) 01:44, 2 November 2007 (UTC)

Agree that certain terminology needs tweaking, especially "assume a computer exists." Is there a subtle error in it? I think we shd keep the standard Sketch, but from a pedagogical viewpoint this I think this perspective is valuable provided there are no serious gaps (as CBM claims) and, hopefully, it can be sourced to dead trees. If it is correct, I would be suprised if it's not published. To address one of the alleged gaps, can't DEDUCE proceed by brute force, attempting all rules of inference against all axioms and theorems ? I'd like to see where we could go with some small terminology changes and gap-filling.

It may indeed be very easy to understand GIT from a modern perspective. Much of what Godel had to invent, from Godel-numbering to his string manipulation functions, as well as the conceptual decoupling of symbols from meaning, we get for free if we start with the idea of a computing machine. What is admittedly historical heresy may be pedagogical gold. Seems worth a shot, anyway. CeilingCrash 02:08, 2 November 2007 (UTC)

We don't need two proof sketches, though. We could add in that a consequence of the incompleteness theorem is that, when everything is formalized properly, a consequence of the incompleteness theorem is that there are Turing machine programs that cannot be proven to halt and cannot be proven not to halt (such as the program that searches for a Godel number of a proof of the Godel sentence p from the proof sketch). The proof sketch in the article and the "modern proof" are not actually very different; the recursion theorem used in the "modern proof" is just the computability analogue of the recursion theorem. There are indeed large gaps in the exposition of the "modern proof". This is evidenced by the fact that he other proof sketch is just a sketch, while this is claimed to be a "proof", but this is much shorter. The reason that the proof of Godel's theorem is usually found difficult is because it is difficult. It doesn't serve the reader to claim the "modern proof" is a proof when in fact it doesn't even use existing terminology correctly. — Carl (CBM · talk) 02:12, 2 November 2007 (UTC)

If we repair the terminology, and avoid referring to this section as a 'proof' (which Like has already changed), would that be acceptable? I see it as a perspective, a pedagogical tool. If I had to explain GIT to a modern human, for instance, I think i would do it this way. CeilingCrash 02:43, 2 November 2007 (UTC)

If you would like to rewrite it somewhere in a sandbox, I'd be glad to comment on it. The fact that incompleteness of axiom systems is related to recursive unsolvability of problems is well known, and a section on that would certainly be worthwhile, especially if it didn't try to prove the theorem but just showed how the two are related. In the end, any actual proof has to deal with Godel numbering, arithmetization, etc.

At a bare minimum, the terminology would need to be made standard, and the vagueness would need to be reduced. — Carl (CBM · talk) 02:50, 2 November 2007 (UTC)

Sounds good to me, I'll start a sandbox in my user:Talk soon and post the link here ... CeilingCrash 02:58, 2 November 2007 (UTC)

I have already rewritten it here. — Carl (CBM · talk) 03:00, 2 November 2007 (UTC)

Rewrite

(outdent) I think I have a dead-tree source for this, I can't access the whole article tho (not a member)

A Proof of Godel's Theorem in Terms of Computer Programs, Arthur Charlesworth, Mathematics Magazine, Vol. 54, No. 3 (May, 1981), pp. 109-121. http://links.jstor.org/sici?sici=0025-570X%28198105%2954%3A3%3C109%3AAPOGTI%3E2.0.CO%3B2-1&size=LARGE&origin=JSTOR-enlargePage

CeilingCrash 03:14, 2 November 2007 (UTC)

I'll email you that article; the proof is well known in any case, so there is a source somewhere. I rewrote the section to be more explicit about what's going on. It now gives a sort of proof sketch of how to use the undecidability of the halting problem to prove Godel's theorem. It currently glossed over ωconsistency, which could be fixed. I hope other people will add links and smooth the text some. — Carl (CBM · talk) 03:24, 2 November 2007 (UTC)

Comments by likebox

I am quite familiar with the completeness theorem. It does not show that recursive functions are representable in arithmetic - that proof of representabilily is the first third of the proof of the incompleteness theorem. There is simply no way to prove the incompletness theorem without some sort of arithmetization result. And Godel's original proof did explicitly develop a formula for Bew...

The idea that the recursion theorem can be avoided by a reference to some sort of "quine lemma" is interesting, but there is no result well-known as the quine lemma, and the result needed here is not just the existence of a quine but the existence of a fixed point for a certain recursive operator. Only the recursion theorem is going to give you that.

Statements such as 'It only requires a great deal of effort if you do not understand it. If you understand it, it is obvious. " seem to indicate some unfamiliarity with the idea of a mathematical proof. The idea is to justify statements to a level where they are convincing to the intended reader. "Either you get it or you don't." is not the way things are proved in mathematics.

Can you say what you disliked about the rewritten version? I tried to keep the informal tone while not having all the terminological errors and vague claims of the "modern proof".— Carl (CBM · talk) 21:14, 5 November 2007 (UTC)

The person who wrote this has never written a quine. If you actually spend the time to write a quine, then it will become clear to you that you can turn any program into a quine by adding a quining subroutine. The subroutine will print out all the code before the subroutine, then print itself out, then print out all the code after the subroutine, and it is obvious to anyone who has written a quine that this will produce a printout of the whole code. Manipulating the printout can then simulate the code, and turning the printout into an arithmetic object is automatic, since the printout is already an enormous ASCII integer.

This result does not require a recursion theorem or a fixed point theorem. It only requires about half-an-hours effort to sit down and do it. It is assumed in the proof that the reader has already done this at some point in their life, otherwise the proof will be incomprehensible, since the central event in the proof is the printing out of your own source-code.

Once you understand this, and this is not completely trivial, the rest of the proof is trivial. The whole game of Godel and Turing is really just a game of self-reference, and the self-reference is best stated in a modern programming language where it is self-evident.Likebox 20:57, 7 November 2007 (UTC)

Dude. That result doesn't require a fixed point theorem: it is a fixed point theorem. Face it, when you write about this sort of stuff, you, Likebox, are acting as a recursion theorist. You're just doing so using nonstandard language. But here at Misplaced Pages, our task isn't to invent or popularize new language to describe existing results: it is to explain as clearly as possible those results using the standard language already in use. Anything else would be original research. —David Eppstein 21:39, 7 November 2007 (UTC)

It is not original research. It is original exposition. Those are two different things. Learn to distinguish between them.Likebox 22:13, 7 November 2007 (UTC)

another question

Does the second incompleteness theorem apply as well to second order logic? In particular, can the classical Peano axioms (i.e. with full second order semantics for the set quantifier in the induction axiom) prove their own consistency? Thanks. —Preceding unsigned comment added by 75.62.4.229 (talk) 10:01, 2 November 2007 (UTC)

There are two possible answer, based on what you want "incompleteness" to mean in the absence of the completeness theorem, which does not hold for second-order logic. The following are true; pick the one you want.

• Peano arithmetic in second-order logic has exactly one model. Thus it is semantically complete - every sentence in its language is either a second-order logical consequence of the second-order PA axioms, or the negation of a second-order logical consequence of second-order PA. In this sense, there is no incompleteness theorem for second-order PA.
• There is no complete, effective proof system for second-order logic. Given an effective proof system, the proof of Godel's incompleteness theorem gives an example of a true sentence of second-order PA that is not provable in that system. So in this sense the incompleteness theorem continues to apply. Unlike the first-order case though, this isn't a special property of theories of arithmetic; no second-order theory that has an infinite model can have be given an effective proof system that proves all the logical consequences of the theory.

— Carl (CBM · talk) 12:09, 2 November 2007 (UTC)

Let me expand on Carl's statement that "There is no complete, effective proof system for second-order logic.". Contrary to the situation in first-order logic, the set of consequences of a finite set of axioms may not be recursively enumerable in second-order logic. Worse, the set of consequences may not even be definable in the language of second-order logic. In which case, the "formula" stating that the second-order theory is consistent is not only unprovable, it does not even exist in the language. JRSpriggs 18:45, 2 November 2007 (UTC)

Not a proof

IS TOO A PROOF! Likebox 23:40, 5 November 2007 (UTC)

I see that Likebox has reinserted the "modern proof". I insist that this is not a proof, and cannot be a proof until notions such as what programming language is being used and how it is encoded are nailed down, which would make it not dissimilar in length and content to the standard proof. At best this is a proof sketch. It is also phrased in such a way as to make it sound like original research, although I am sure one can find printed sources for similar expositions. I would like to request that the section either be removed again (my preference), or that it be called a proof sketch, the word "modern" removed, sources provided, and it be incorporated more smoothly into the existing "proof sketch" section rather than trying to stand alone as a separate section. —David Eppstein 21:12, 5 November 2007 (UTC)

Of course there is no exact line between a "proof" and a "proof sketch" (or more precisely, if one attempts to draw such a line, one will find that virtually all published proofs are "sketches"), so let's not waste effort arguing on whether it's a proof or a sketch.

I think we can all agree that a valid proof/proof sketch along these lines is possible (whether Likebox's specifically is such a one, I have not checked), and I agree with Likebox that such an approach more easily connects with many people's intuitions, replacing the tedious proofs of the recursion theorem and arithmetization with such things as correctness of compilers -- things that readers haven't personally checked at a level that could be called "proof", but which they're more willing to believe on the basis of experience.

However I agree with David that the proof needs to be made less personal and idiosyncratic, and that it should be integrated with the other proof. --Trovatore 21:25, 5 November 2007 (UTC)

(e/c) Please note that the "Relationship with undecidable problems" section is the same idea, just rewritten to use more standard terminology. It presents the same proof outline (although it is does a better job of alluding to the fact that any undecidable, r.e. set can be used). It is intended to be a sort of compromise, including the ideas from the flawed "modern proof" section without the expositional problems I described at length above. — Carl (CBM · talk) 21:27, 5 November 2007 (UTC)

I see that there is controversy, and I would like to comment. I respect all sides here, and I am not trying to be a bully. I just wanted to explain.

First I did come up with this proof, but I am not the first person to come up with it. It is ideosyncratic because I don't want to use language which a layperson cannot follow. That is the crucial part, and replacing the discussion with a discussion which uses "standard terminology" is just code for making it obscure. Please do not make a clear discussion obscure.

Using standard terminology has another insidious effect in that it protects those who benefit from a monopoly on knowledge. This authority-reinforcing tendency is natural, but in my opinion, unfortunate.

As for technical precision, this proof is exactly as rigorous, no more and no less, as Godel's original exposition. I took it largely from Godel's paper, except replacing arithmetization with a modern obvious arithmetization (ASCII and TeX), and replacing statements about deductions with statements about computer programs that do the deducing. The proof is identical, but is much easier to follow, because modern readers know what a computer is. There really is no difference in the content in any way. Perhaps the reason it strikes people as implausible is because they think "it can't possibly be that simple!" Sorry folks, it is.Likebox 22:52, 5 November 2007 (UTC)

The difficulty is not whether computers can do things - the halting problem is easy to prove because it is just about what computers can do. Godel's theorem requires proving that some universal model of computation can be faithfully represented within arithmetic. In his original paper Godel explicitly demonstrated this. Now people may be more willing to take it on faith, but any actual proof must still address arithmetization. After Smullyan's influence, the most common "modern proof" is the one using the diagonal lemma. — Carl (CBM · talk) 23:13, 5 November 2007 (UTC)

Look, you're absolutely right. I didn't prove that arithmetic embeds a computer, and Godel did show that arithmetic embeds a "computer" (meaning a computer running the algorithm of the completeness theorem and only the algorithm of the completeness theorem) in a somewhat more explicit way. But if arithmetic doesn't embed a computer, it's a pretty sorry system! If that's true, then you can't make statements about the behavior of computer programs in arithmetic. That's why I stated the theorem about axiom systems which can describe computation, not as a theorem about Peano arithmetic.

To prove that Peano arithmetic embeds a computer, you can use Godel's system--- write an integer as a list of prime powers:

${\displaystyle n=2^{n_{0}}3^{n_{1}}5^{n_{2}}7^{n_{3}}}$ and note that some first order sentence extracts each ${\displaystyle n_{i}}$ from n, since the property of being the n-th prime is primitive recursive.

If you want to embed a turing machine, let ${\displaystyle n_{0}}$ be the state of the head, let ${\displaystyle n_{1}}$ be the position of the head, and let ${\displaystyle n_{2},n_{3}...}$ be the content of the tape. Then you need to construct a first order sentence which says that the update of the quadruple ${\displaystyle (n_{0},n_{1},n_{n_{1}})}$ will be ${\displaystyle (n_{0}',n_{1}\pm 1,0\;\mathrm {or} \;1)}$ with a long list of options to describe different outcomes depending on the state of the head. Do I need to go translate that explicitly into first order sentences? It would require a lot of fiddling around with pairing functions and prime-extraction functions. What's the point? If this couldn't be done we would just throw away Peano arithmetic.Likebox 23:38, 5 November 2007 (UTC)

That's completely backwards - Peano arithmetic is justified as a theory of the natural numbers. The relationship between arithmetic and computability is not a motivation in the mere definition of PA, and PA would still be of interest if it didn't represent computable functions. The entire point of a rigorous proof of the incompleteness theorem is that it has to show that a sufficiently strong theory of arithmetic can represent something - either some basic computability or some basic proof theory.

I copyedited, but didn't remove, the stuff you added. Please work towards a compromise version, rather than merely reverting. Remember that (1) we don't need to prove everything here and (2) the general consensus in this article is not to dwell on the Rosser extension of the theorem, since all true theories of arithmetic are ω-consistent anyway. Try to focus on making the section match the rest of the article. There is a lot of work left to do, but I will leave it alone for tonight. — Carl (CBM · talk) —Preceding comment was added at 23:48, 5 November 2007 (UTC)

Likebox, please quit reverting, and get the "political" chip off your shoulder. None of us wants to hide the Goedel theorems from the common man. But an encyclopedia is not a teaching tool, it's a reference work. You need to make your additions consistent with that, or convince us that a departure from that principle is justified in this case. --Trovatore 23:56, 5 November 2007 (UTC)

That's your point of view. The effect of this point of view is exactly to hide the Godel theorems from the common man.Likebox 01:06, 6 November 2007 (UTC)

Spelling nit

Please, everyone, quit writing "Godel", even in the talk pages; it's a flat misspelling. You don't have to go to the effort of putting in the ö character -- just write "Goedel", which is correct. The umlaut is not a diacritic in the ordinary sense, but a marker for the missing e. --Trovatore 00:00, 6 November 2007 (UTC)

" language that should have been retired decades ago"

Moved from User talk:CBM

Look, I sympathize with your position, but do not edit a proof you think is invalid. Think about it for a few days first. Your edits make it imprecise and vague, by reverting to very, very unfortunate recursion theory language, language that should have been retired decades ago. I worked hard to make it correct and precise.Likebox 23:52, 5 November 2007 (UTC)

It isn't our place to decide what terminology should have been retired when, and a consequence of WP:NOR is that our articles use standard terminology. In the case of Recursion theory means terminology such as "represent all computable functions" and "recursively enumerable set". If you want to change the world, or make people use new terminology, Misplaced Pages is not the place for you.

In the meantime, please try to work towards a consensus version. I have no objection to the idea of a sketch of a computational proof, but several people including me have expressed reservations about the current wording. — Carl (CBM · talk) 23:58, 5 November 2007 (UTC)

I am not asking that the recursion language be scrapped. I am asking that you include a reasonable proof in computational langauge in addition to a proof in recursion language. This might have the effect of causing people to abandon recursion theoretic language in the future, but that's not for me or Misplaced Pages to decide. But there are both people who believe in recursion language, and people who do not. It is ridiculous to assume that recursion language is "preferred" because many people who do research in the field are forced to use it. You must represent all points of view in proportion to their number.Likebox 00:24, 6 November 2007 (UTC)

Also, I don't really care what the language is, so long as the computer programs are spelled out precisely, and their properties are manifest. The edits that you have done have made the proof vague.Likebox 00:26, 6 November 2007 (UTC)

From my perspective, there is no significant difference between computer science terminology and recursion theoretic terminology. If you believe there is, I encourage you to present some references to computer science texts that use your preferred terminology, so that the other people here can see how the terms are defined in those texts. — Carl (CBM · talk) 00:40, 6 November 2007 (UTC)

That is not true. You can easily write self modifying code in computer science language, you can't do it easily in recursion language. The computer science texts are "The C programming language" by Kernighan and Ritchie, and the countless papers in the 1970's on Random Access Machines. The existence of pointers and indirect adressing are crucial, and are hard to mimic in recursion theory. The insights of the 1970's need to be recognized, although they have yet to change any of the recursion theory texts. That doesn't matter. You can keep all your favorite language. Just don't delete someone elses favorite language.Likebox 01:05, 6 November 2007 (UTC)

Kernighan and Ritchie is not a text on theoretical computability, it's about the C programming language... There are lots of computer science texts on computability theory. In my experience, they use virtually the same terminology as mathematics texts on computability theory. If you can provide some counterexamples, I will be glad to look through them. As I said, Misplaced Pages is not the place to right the wrongs of the world. If you can't justify your additions in terms of the existing texts and standard expositions of the topic, it will end of removed. It's up to you to give it more justification than just "I like it". — Carl (CBM · talk) 01:09, 6 November 2007 (UTC)

Can someone please clarify what is meant by 'computer science language'? I am aware that there are two names used for the field 'recursion theory' -- that, and 'computability theory', the latter being the more modern and by some preferred. Do you mean a particular programming language (like C, Perl, Python, ADA, whatever...) Thanks. Zero sharp 01:13, 6 November 2007 (UTC)

Only Likebox can say for sure what he or she means by "computer science language", but it refers to terminology, not a programming language. Based on edits here and to Halting problem (also see my talk page), it seems Likebox dislikes the standard terminology of recursion theory, preferring to use terms like "computer program" instead "computable function", etc. — Carl (CBM · talk) 04:47, 6 November 2007 (UTC)

The distinction between "computer science language" and "recursion theory language" is a distinction between the way in which you describe an algorithm. A recursion theoretic description does not have enough operations which allow you to print your own code in any simple way, nor does it have an easy way to state things like "print Hello World". This is an important terminology distinction, which makes the proof I wrote clear and comprehensible, and makes the proof that is presented in the current version an unacceptably vague sketch.

The current text, while it follows the outline of my proof, does not do it very well. The new text does not prove the Rosser version of the incompleteness theorem at all, and requires an omega-consistency assumption which is not acceptable in any way. The current text does not give a rigorous proof of anything at all, because it does not specify the computer programs precisely enough. It is just a bad sketch. The discussion I gave is a complete and correct proof, as rigorous as any other presentation. To replace a correct proof with a vague sketch is insane.

Finally, this proof has the gall to pretend that Kleene et al. and alls y'all actually understood the relation between halting and Godel's theorem before you read the proof that I wrote. While, in hindsight, after a few weeks of bickering, it is clear to all you folks that quining and the fixed-point theorem are identical, that Godel and Halting are identical, none of you knew exactly how before I told you. If your going to use my insights, use my language and cite the paper I cited. The only reason this is not original research is because some dude wrote a paper in 1981, and because of the reference provided. To pretend that this proof is somehow implicit in the standard presentations is a credit-stealing lie. It was precisely because the standard presentations are so god-awful that I had to go to great lengths to come up with this one.

So I revert to the old terminology, and I ask that you hold some sort of vote among neutral parties. If you are going to prove the theorem, the proof I gave is the shortest, the clearest, and comes straight from Erdos's book. It describes the computer programs completely and precisely, so that any programmer can actually write them. It proves the strong version of the theorem, and it is logically equivalent to Godel's original proof. But the language and presentation are not due to Godel or Kleene. They are due to that dude in 1981 and to a lesser extent to the author of the more recent preprint. Certainly not to any recursion theorist.Likebox 06:22, 6 November 2007 (UTC)

Ok I know I'm late to the party here, but Likebox, can you please cite (and my apologies if you have already done so elsewhere but I"m having a REALLY hard time following this discussion) 'Erdos' book' and "that dude in 1981" Zero sharp 06:40, 6 November 2007 (UTC)

and, for the record, can you explain why this is not Original Research? Thanks. Zero sharp 06:42, 6 November 2007 (UTC)

It's not original research because somebody published it already in 1981. That's this guy, from the discussion above:

A Proof of Godel's Theorem in Terms of Computer Programs, Arthur Charlesworth, Mathematics Magazine, Vol. 54, No. 3 (May, 1981), pp. 109-121. http://links.jstor.org/sici?sici=0025-570X%28198105%2954%3A3%3C109%3AAPOGTI%3E2.0.CO%3B2-1&size=LARGE&origin=JSTOR-enlargePage

The logic of the discussion follows that paper, but the language follows the reference cited. Erdos's "book" is God's book of proofs, the shortest proof of every theorem. It's not a real book, but a mathematician's description of the most elegant proof of a theorem. I am pretty sure that the proof presented here is the book proof of the Godel's theorem.Likebox 06:47, 6 November 2007 (UTC)

I put the reference to Charlesworth in. I would have put it in earlier had I known about it.Likebox 06:53, 6 November 2007 (UTC)

One thing I agree with Likebox about is that this proof concept is not original research (although the citation Likebox gives isn't ideal). It is very well known that Godel's theorem can be proven from the existence of an r.e. undecidable problem. Such a proof does have the advantage of highlighting the role of effectiveness in the incompleteness theorem.

But the language Likebox is proposing is very nonstandard - for example, his "quine lemma" is not a lemma about quines but actually Kleene's recursion theorem. I have no objection to the idea of a computational proof in the article, but it needs to use standard terminology. The text also fails to read like an encyclopedia article, fails to integrate into the rest of the article, and obscures what is going on by dwelling on specific programs too much. I keep editing it to resolve those issues. — Carl (CBM · talk) 12:32, 6 November 2007 (UTC)

I once saw Bob Solovay present a similar proof on a blackboard in about 15 seconds, so it's not as if logicians have never heard of Turing machines. Maybe this situation is best resolved (parties willing) if Likebox were to write up a computer-based proof as a wikibook module, which the encyclopedia article could link to. Wikibooks have more room for exposition than encyclopedia articles do, wikipedia should link to wikibooks in preference to traditional books when it can, and wikibooks.org definitely needs more coverage of logic-related subjects.

Another thought: spin off a new article called Godel incompleteness theorems: Modern proofs or some such, and link it back to this article. Then everyone can discuss it on that page. The fact that there is a published article (I've read it now) should alleviate the O.R. concerns. . Another thought if everyone howls about the first suggestion: create a page in your "user space" as follows User:Likebox/Gödel modern proof and move your proof there until its ready to be moved over to the new sub-article. (If you want, I will create the page for you). Others can contribute on its talk page. I want to look at it as if it were an article, not as part of your talk page or in history. Bill Wvbailey 15:16, 7 November 2007 (UTC)

We don't need another spinoff article/POV fork/whatever it would be. We already have one proof sketch spinoff page; Misplaced Pages is an encyclopedia, not a compendium of numerous expositions of the same proof. Someone else suggested wikibooks as a place Likebox might be able to publish his proof.

There is no difficulty here with original research; the proof is well known. The issue is that Likebox eschews interest in working towards compromise . The proof Likebox is presenting is exactly the proof from Kleene 1943, just rewritten to avoid terminology that Likebox rails against . Even if Likebox were right that the entire computer science and math logic community uses poor terminology for basic computability theory, we're not here to cleanse the world of bad terminology. It's ironic that Likebox motivates his recursion-theoretic proof by saying 'there is not a single shred of insight to be gained from learning any recursion theory'. — Carl (CBM · talk) 15:55, 7 November 2007 (UTC)

I hear you. I think a "semi-formal" (i.e. a really good-quality) "non-recursion-theory" version (i.e. "computational-machine"-based) is not going to be trivial, especially if it does not invoke undecidability of the "halting problem" as a premise (a cop-out IMO). I've deconstructed (and compressed into bullet-points) part of the Charlesworth paper, part of Rosser 1939 and part of Gödel 1934 §6 at User:wvbailey/Explication of Godel's incompleteness theorems -- it's just my holding/working place, I have no further intentions for it at this time. But the deconstructions are quite interesting and may be useful. Bill Wvbailey 17:23, 7 November 2007 (UTC)

Although likebox will no longer touch this encyclopedia page with a ten foot pole, I would like to comment that I came up with my proof indepedently many years before I actually studied any logic or any recursion theory. I did read "Godel Escher Bach" though when I was in high school, so it wasn't a research project, just an exposition project.

Knowing this nifty proof made me curious to see how the professionals do it, so some years later I went and audited a whole bunch of recursion theory classes, and went to logic seminars for two years so I could follow their version of the thing. It was a painful and frustrating experience. All their results were trivial, and expressed in godawful obsolete language that disguised the triviality!

But at least the recursion theorists understand it, or so I thought. But what I discovered, to my horror, was that with the exception of a very few very senior faculty members, none of the students and precious few of the postdocs or junior faculty actually followed the proof of even a result as elementary as Godel's theorem. This made me very sad, and I didn't know what to do.

The way I discovered this was by giving my proof of the theorem to a graduate student, who understood it. He then asked the (incompetent) junior faculty running the recursion theory class "Can you prove that it is undecidable whether a program runs in exponential time or polynomial time on its input?" The junior faculty fiddled around with the "s-n-m theorem" and the "recursion theorem" and the "fixed point theorem" for a long, long, time, and could not do it. This is unbelievable! It's a trivial thing to prove.

The proof is thusly: Suppose PREDICT(R) predicts whether R runs in polynomial time or exponential time on its input. Let SPITE(N) print its code into the variable R, calculate PREDICT(R), all the while ignoring N, then if PREDICT says "exponential", SPITE runs a polynomial algorithm on N, and if PREDICT says "polynomial", SPITE runs an exponential time algorithm on N.

Why couldn't junior-faculty do it? Becuase the Kleene fixed point theorem puts the source code to SPITE on the god-damn input-stream of the Turing machine. It's then hard to say how long the input is. You need to conceptually separate the input part which is the source-code from the input part which is the input, and junior-faculty got confused. This sorry story is still repeating itself in every recursion theory department in the country and in the world.

So here's wikipedia. That's what wikipedia is for--- for disseminating knowledge that's well known. As far as a proper proof, stop kidding yourself. The proof I wrote and that is linked is more rigorous than anything else in the world, and everybody knows it.Likebox 19:02, 7 November 2007 (UTC)

Thank you for putting your work at User:Likebox/Gödel modern proof so I can look at it. Bill Wvbailey 21:55, 7 November 2007 (UTC)

Cool, I'll get a look at it there too. The critical point - and I missed it the first time through myself, is L's proof does not assume CT or Halting. Rather, it proves it so quickly you might miss it. SPITE() is designed to defy a test of halting, H. It feeds itself (using the 'quining' key to self-reference) into H, and does the opposite of what H predicts. Spiteful, that function.

Get Russell a hanky. Conceptually, to my way of thinking, the proof is as simple as this :

a) a statement (S-expression in LISP, piece of code, whatever) can output its own source. (quining.) Try it in any language, it's fun and non trivial.

This gives the key to self-reference. Rather than printing, the output string could be assigned to a variable named Myself. This is counter-intuitive as hell but within the grasp of any student eager to experiment. The point is source code can mention 'Myself' or 'This source code' in a very real and executable way.

b) We can now defeat any proposed Halting test for source code. The function Spite() deliberately breaks the H-test, by using the self-reference trick in a) to feed itself into H, peek at the result, and either hang or crash - whichever makes a liar out of H.

c) It is then a reasonably short trip from Halting to Incompleteness (see main article.)

Whatever one's view of Likebox, the simplicity and clarity of this exposition is stunning. Given this outline, any 'ordinary' mathematician could fill in the gaps to reconstruct a proper proof without, I believe, any notable insight. Any undergraduate, with an affinity for such matters, can grasp the key insights and defend the main thesis. Amazing. The Theory of General Relativity was once hopelessly inaccessible even to many professional scientists, as was Galois Theory. They are not so today. Over time the conceptual landscape changes and new paths are sought to the peaks. Entirely new hills rise and new perspectives emerge from which formerly obfuscated landmarks can be clearly seen. This process is to the greater good.

Any one who doubts this is encouraged to try to extract F=MA from Newton's Principia.

I believe if the reader carefully steps thru L's proof, and ignores trivial matters of terminology (they are easily remedied), s/he will see that it is a) self-contained and b) free of significant gaps. Erdos used to say, when a proof has gotten to the crux od the matter with maximum simplicity, that it was in God's book. If there is a God and He has a book, this proof is in it. updated CeilingCrash 06:55, 8 November 2007 (UTC)

Nobody disagrees that a proof of the first incompleteness theorem can be obtained using computability; this proof is in the article at this moment. The problem is that Likebox's actual exposition is unsuitable for the encyclopedia, as numerous people have pointed out. I'm sure some compromise wording can be found. — Carl (CBM · talk) 13:51, 8 November 2007 (UTC)

When people of good faith compromise with narrow-minded people with a language agenda, the result is an incomprehensible piece of junk. One must defend good exposition from such attacks.Likebox 18:18, 8 November 2007 (UTC)

Reference - Kleene 1943

Since the question of original research came up, I looked up a reference for this proof. It dates back at least to Kleene, 1943, "Recursive predicates and quantifiers". Theorem VIII states:

"There is no complete formal deductive theory for the predicate ${\displaystyle (x){\bar {T}}_{1}(a,a,x)}$."

As the T is Kleene's T predicate, and the bar indicates negation, this is exactly a statement about the halting problem. Kleene explicitly says: "This is the famous theorem of Gödel on formally undecidable propositions, in a generalized form." This paper is available in the book The Undecidable as well. — Carl (CBM · talk) 12:49, 6 November 2007 (UTC)

Dude, this argument was never about content. It was about language.Likebox 19:15, 7 November 2007 (UTC)

Created Archive 03

The talk page was getting very long, so I have moved the discussion prior to the current active one (about the new 'proof') to Archive03 and added a link in the Archive infobox. Zero sharp 16:17, 6 November 2007 (UTC)

Semantic proofs

We now have three proof sketches in the article: the main sketch of the syntactic proof, the section on computability, and the section on Boolos' proof. I pulled Boolos' article today, and it does seem worth mentioning briefly. I think we should rearrange things so that all the proofs are in one section. Within that, the first subsection should concern arithmetization, then the syntactical proof sketch, then a section on semantic proofs including the computability proof and Boolos' proof. Boolos points out in his paper that Goedel gives another semantic proof in the intro to his paper on the incompleteness theorems. The current organization is less than ideal. — Carl (CBM · talk) 16:42, 8 November 2007 (UTC)

Seeking a peace accord

Let me apologize for the length of this. I wrote this for several reasons, not the least of which is that I was first to delete Likebox's proof (then reversed my view), and feel like i sparked off a contentious disagreement which led to a temporary edit-block and some ill feeling.

Also, I have spent roughly equal time in both schools of thought (my dad was a logician), and appreciate both the austere beauty of formal mathematics and the abstract dynamism of the computational view. The conflict between the two schools is visible on any university campus, but in the end it is illusory as both schemas are ultimately bound by an isomorphism.

I have a mixed background in math and comp sci, and I think the discord here is just a result of different perspective. First of all, let me say that L's proof is by no means a formal, mathematical proof (nor a sketch of one) satisfactory in the sense of mathematical rigor. The proof offends the formalist sensibilities, and seems a strangely worded reiteration of points already made elsewhere.

But let me back up a bit. We all know that any real, published proof is not a formal proof but an abbreviation. An actual formal proof of even the simplest theorem would be tedious and impossibly long (in Principia, Russell famously takes 106 pages to get to 2+2=4.) Except for proofs in Euclidean geometry, mathematicians opted long ago for proofs which are really roadmaps to proofs. They serve a social function; whereby a researcher announces to his peers how to do a formal proof. A good proof contains only the non-obvious bits, and omits everything obvious. This is by no means laziness but necessary, else our journals would be filled with obvious explications and one would have to scan 100's of pages of text to get at the crucial ideas.

But obviousness is relative to the audience (even among mathematicians, this changes from generation to generation.) Don't get me wrong - Godel's proof, historically, belongs to the mathematicians and the formalist, mathematical perspective should get top billing. But other audiences are worthy of our attention as well.

Godel's Theorems and CT were written prior to the first real computer program (a credit to their author's inventiveness.) Many young people today have grown up writing computer programs (I wrote my first at 12, which may be been unusual in 1978, it certainly is not so now.) With mathematics, we require our young to spend much time learning to do arithmetic and algebra. It is only through this direct doing that we can internalize these ideas, and develop intuition to guide us in with new problems. It is this training that defines our sense of the 'obvious'.

A person who has been writing programs for many years develops a similar intuitive sense about computing machines, what is possible, what is easy, what is hard, what is obvious. The lambda calculus and turing machine are their native ground. So, to a programmer certain things seem obvious which are not so to a pure mathematician (and vice-versa, i'm sure.) We can see this from the discussion. For instance, at one point an editor objects to Likebox's claim that, basically, 'quining' (the term is due to Hoefstadter) and variations thereof are easy and self-evident. The editor objects - correctly - that Likebox is is really pulling in the recursion theorem. Likebox responds - also correctly - that a person who has actually written quines instinctively knows this to be true and can write such a program in a few minutes. Both Likebox and the other editor know how to make this 'quine'. They simply disagree on whether the reader can be expected to or, even if the reader senses it, does he demand proof anyway. They disagree on the reader's expectations.

It comes down to a question of what is obvious to whom, and this is mostly a function of background. The complete, unexpurgated proof will never be written. What comprises a meaningful proof-map is dependent on the intended audience's background and demand for rigor. The mathematicians certainly come first and foremost, but I think it's OK to provide proof-maps for different audiences in wikipedia. In fact I think it is a very good idea to do so, provided we make clear we are shifting gears in a major way.

For a programmer, several things (which are monumental and visionary unto themselves) are going to be obvious for the simple reason he has already worked with them. The arithmetization of a symbol system is automatic; symbols are routinely coded into integers, and often there are multiple layers to such a mapping. The ability to create 'quines' and variations thereof are going to be evident (after the reader works a few problems on it.) Even the connection from Halting to Incompleteness - while not obvious - is well within the range of mere mortals to fill in. In short, a reader with lots of training in programming is already 1/2 way to intuitively grasping godel's proof. To provide this reader the proof-map for the rest of the trip seems to me a valuable contribution to an article on godel's proof, and doesn't detract from the more formal and historical proof-map.

It's not that programmers have some superior abstract perspective. It is precisely due to mathematicians like Turing and Von Neumann that these computational abstractions were refined, simplified and made real such that any kid can (and does) play with a computer, that certain of these abstractions are now common ground to a new generation. And what could be better than that?

So I advocate we tighten up the wording in L's proof, maintaining the current structure but substituting or clarifying certain language - while granting L a certain license to opt for plain explanations rather than terms familiar to a mathematician. Also we should give some kind of forward about whom the section is intended for, and that it is not in competition with the traditional treatment.

"Yes, I know the garden very well. I have worked in it all my life.

It is a good garden and a healthy one ...

there is plenty of room in it for new trees and new flowers of all kinds ...

I am a very ... serious gardener." - Chance, Being There

CeilingCrash 17:13, 8 November 2007 (UTC)

I don't see even a theoretical benefit to the use of quines and specific programs. It obscures the general phenomenon, which is the relation between provable membership in a set vs. the recursive enumerability of the set. (This is still ignoring the nonexistence of the "quine lemma" etc.) Could you comment on the current wording, explaining what you think is unclear about it? It's exactly the same idea, just expressed more reasonably.

Sure, there is nothing unclear about the present wording on its own terms; it's just a matter of terminology. By "theoretical benefit" i take it you mean 'hypothetical benefit', as we're not claiming an improvement to theory. I'll be more specific in a little while, but the mathematical perspective comes from a higher level of abstraction, where we speak of 'provable membership in a set' and 'recursive enumerability of the set'. The programmer doesn't think in terms of sets, but rather algorithms and their outputs. The programmer would not say a set is recursively enumerable, rather he would say "any of these will be eventually produced by this program." To give a simpler example, a mathematician defines a prime number as having no (non trivial) divisors. A programmer sees it as the output of the sieve of erastothones, or perhaps "what's left out when you multiply everything by everything else." It's a dynamic view. To be sure, the static view is the more formally satisfying because the dynamic view can be seen as shorthand for what really is a static sequence of steps. (Set theory came first. One wonders, however, how things might have gone differently had Church continued with the original intent of Lambda Calculus, which was to ground mathematics on functional, rather than set-theoretic terms.)

From the dynamic view - which very admittedly smuggles in a great number of results formally belonging to recursion theory and other areas - the key ideas are "you can make a quine" and "no algorithm can decide haltingness." These are totally non obvious. All the rest is by no means formally trivial, it is just of little surprise to the reader coming from this view. CeilingCrash 17:57, 8 November 2007 (UTC)

CeilingCrash has said many wise and correct things. But he assumes that the reason I am trying to incorporate CS language in the recursion theory pages is because I am unfamiliar with the methods of mathematicians or do not appreciate their "austere beauty". That is not true. He also assumes that the reason that some recursion theorists erase the proof is because they honestly think that the language I am using is confusing. That is also probably not true. It would take a truly illiterate person to not understand that the proof that I gave is correct. Even if the person thought it was a sketch, there is nothing preventing them from presenting another proof alongside.

But they insist on either deleting the proof or replacing it with language which makes it incomprehensible to a coder.

The real reason is that the people who enter the recursion theory world are forced, by a systematically constructed power structure, to adopt a certain language for their algorithms. This language is inferior in every way to any modern computer language. But if you do not adopt it, you are not politically allowed to call your algorithm a proof, no matter how precise and no matter how clear. You could even write out the code explicitly, and it is not a proof. You could run the code on a computer and have it work, and it is not a proof. It is only a proof if you use the recursion theoretic language to the letter, with all the ${\displaystyle \phi _{e}}$ and ${\displaystyle \phi _{\phi _{e}}}$. If it ain't got the ${\displaystyle \phi }$s it ain't no proof.

To understand why this inferior language dominates, one must look to the academic structures in the 1950s when the modern recursion theory departements were constructed. The people who created these departments wanted a divide between their field and that of theoretical computer science, with Knuth and Minsky on one side, and Nerode and Woodin on the other side. They wanted to establish their field as legitimate pure mathematics, not as a branch of applied mathematics.

To facilitate this artifical division, the recursion theorists constructed a wall of terminology to prevent "code-monkeys" from claiming algorithmic proofs for recursion theoretic theorems. This means that the recursion theoretic world will not accept as legitimate any algorithm which is not written on a Turing machine in Turingese. In order to get a paper accepted in a recursion journal, even to this day, one must write the algorithm so that it is not readable by a person who codes. This is not an accident. It is there by design, and this motivation was explicitly stated by the founders of the respective fields. It was to prevent pseudo-code from infecting mathematics journals.

This division, I am certain, cannot survive in the open marketplace of ideas provided by the internet. But to help along its demise, I try to provide clear proofs in modern computational language of all the classic theorems of recursion theory. The proofs are so much simpler in the natural language of computer programs, that I think recursion theory language will be about as popular in the future as latin.Likebox 19:24, 8 November 2007 (UTC)

It remains the case that Misplaced Pages is not a forum for correcting historical injustices, real or perceived. That should be done elsewhere. Perhaps you could publish a paper somewhere about the faults of recursion theory and its notation. — Carl (CBM · talk) 19:34, 8 November 2007 (UTC)

At least you have finally admitted your position. Now we have a real conversation.Likebox 19:46, 8 November 2007 (UTC)

I have been quite frank about my position. "Misplaced Pages is not the place to right the wrongs of the world." — Carl (CBM · talk) 20:04, 8 November 2007 (UTC)

(deindent) Now that we understand the issues, I would like to admit a little white lie. I never expected the proof to stay on this page. Nor did I expect the quine proof of the Halting theorem to stay on the Halting problem page. In the first few weeks, I had about a 75% confidence level that it would be deleted by somebody who has a recursion theory PhD, and that this person would attack the proof as illegitimate on language grounds.

It took a lot longer than I expected, mostly because it takes a while for the political sides to emerge. But now that the battle is fought, I would like to ask a more profound question. What is the purpose of Misplaced Pages, really? Why can anyone edit any page, even a person who does not have a PhD, like myself? Why is an expert opinion, rendered by a tenured professor of equal value to the opinion of a lay-reader?

The reason, I believe, is the oft-stated principle of radical inclusiveness. It is to make sure that ideas to not stay hidden, even if there are well established power structures that strive to make sure that they stay hidden. This is the reason for my additions, and this is why I defend them from the academic powers that line up to attack them.

This is also the reason that I am optimistic about Misplaced Pages. Because even when the additions are not incorporated, the resulting debate exposes the power structure, and, over the long term, will right the historical wrongs. It has already happened for Ernst Stueckelberg, and it is happening for Wolfgang Pauli, whose genetic ideas were decades ahead of their time.

Historical wrongs were put right long before the internet existed. Look to the history of reconstruction in the U.S., or the history of the conquest of the Americas. But the internet makes the process much faster. I am pretty sure that anyone who has been following this debate will abandon the recursion theoretic proofs. Not everyone. But enough to make a difference.

So I remain optimistic, whatever happens here. For the interested reader, here's the only real proof of Godel's theorem you're going to find on Misplaced Pages:User:Likebox/Gödel modern proof. Likebox 20:08, 8 November 2007 (UTC)

I have a merge in the works to suggest of Carl's and Likebox's exposition (the key difference being only that Likebox's version sketches Halting (and points to a construction which defies a given halt-detector H), collapses some of Carl's finer points for brevity, and inserts some narrative explication of my own. I may not be making sense right now as i'm very tired :) In any case, I hope to arrive at a hybrid acceptable to consensus that is helpful to computer-oriented folk. I am quite sure Likebox will scream bloody murder, but my goal is really to improve the article for the theory-impaired but algorithm savvy. Once editors here take another pass at it, i am sure we can pin it down. In any case, one hell of an interesting discussion and I, for one, have learned immensely. By the way, I had come here by way of the Lambda Calculus article; the introduction to that article had been, er ... plagiarized so had to be deleted. This left a headless article, so i rapidly put together an intro. I am not an expert in this area, so would appreciate some extra eyes on it Lambda_calculus Thanx —Preceding unsigned comment added by 24.128.99.107 (talk) 04:46, 9 November 2007 (UTC)

Oh, and to respond briefly to Likebox, I don't think he is acting out of a lack of understanding of formal math. I believe Likebox is of the view that godel's proof is attainable in a considerably more direct (thus conceptually superior) way, and that his proof is as complete as any of Godel's.

My personal and currently indefensible view is that he right in this, that Godel can be reformulated more clearly from newer ground. However, I am not prepared to enter that debate, haven't thought carefully enuf about it, and in any case that issue is beyond the scope of a mere tertiary source as wikipedia. The reasons I claim for inclusion here are pedagogical, in that the train of reasoning is tractable to coder people. So I'm sticking to that. 24.128.99.107 05:03, 9 November 2007 (UTC)

Note that one of the issues iwth Likebox's proof was brevity; if you remove the unneeded restatement of the incompleteness theorem, the resulting "proof" was far too short, ignoring many important details. But I'll be glad to look at rewrites and we can find some compromise language. I still haven't gotten any actual feedback about the language that is in the article right now, which is the same proof that Likebox wanted, just written up better. — Carl (CBM · talk) 13:23, 9 November 2007 (UTC)

Oh my god! It's too clear! Look, just leave it alone, and put your sketch in another section. As I said, it leaves out no details at all, and is more rigorous than anything else in the world.Likebox 19:17, 9 November 2007 (UTC)

There is no need to have large numbers of different proof sketches in the article. There are already three of them!

And none of them (including yours) are self-contained and complete. Mine is self-contained, complete, more rigorous, and shorter than all of the others.Likebox 23:01, 9 November 2007 (UTC)

As for unclear parts of your proof, you might begin with the phrase "axioms will follow its operation". Axioms, like all other formulas, are immobile.

Could you explain what parts of the current wording you dislike, if you are amenable to compromise, or refrain from commenting here if you have no desire to compromise? Misplaced Pages is not the place to push your POV about how proofs should be written. — Carl (CBM · talk) 19:26, 9 November 2007 (UTC)

What part of the current wording I dislike: first there is no computer program. You don't describe a computer program, so you can't have a proof. Second there is no mention of the Rosser version. That is unacceptable when the Rosser proof is a minor tweak, and the Rosser version is just as easy. Third, it is written obscurely, and cannot be read and understood by a layperson or an undergraduate. Taken together, these objections are fatal.

"Axioms will follow its operation" is explained later in the sentence. It is no more unclear than "Axioms will describe a standard model of computation" in your rewrite.

I have no problem with compromise, so long as the compromiser will read the proof, understand it, and think about it before rewriting it, preserving the ideas and the explicit exactness of the discussion. I think I have already gotten it to the point of no-further improvement possible, but I might be wrong.Likebox 23:01, 9 November 2007 (UTC)

Wait a minute - the quote you give ("Axioms will describe a standard model of computation") is not in the article at all, and it has not been edited since your comment. If you want to give feedback about the article, it would help if you only quote things that are actually there. I agree that the current version could use a little more detail about arithmetization; this is one of the places where your original writeup is particularly weak. Another place where both are weak is on the role of ω-consistency, because of a lack of detail about the T predicate.

The article as it stands doesn't spend any time on the Rosser version; if you would like the article to cover that, it will need to do it in more than just one section, but the previous consensus was not to cover it.

The claim it is written obscurely is likely just your opinion that all standard terminology is obscure. Which particular part do you feel is obscure? It is not necessary to give actual code to have a precise proof, as was established by Rogers' book in the 1960s. — Carl (CBM · talk) 02:58, 10 November 2007 (UTC)

Obscurity is a matter of---can a person who is not familiar with your field read this and understand what is going on? This requires a taste-test of the presentation. I have taste-tested my presentation on lay-people, and they understand it.Likebox 06:45, 11 November 2007 (UTC)

(deindent) I did not delete anybody else's text, so I am not imposing a view. I just added a different style of proof, which is short and to the point. I tried to be clear, but maybe I wasn't perfect. I tried to be accessible, maybe I fell short. I don't know.

Request for comments

Template:RFCsci

The issue is the wording of the section about the relationship of the theorem with computability theory. For details, see above. — Carl (CBM · talk) 19:30, 9 November 2007 (UTC)

also see User:Likebox/Gödel modern proof for the alternate exposition. The main difference is that I used explicit spelled-out computer programs.Likebox 23:03, 9 November 2007

(UTC)

I think, i am pretty sure, i have some tenuous handle on both party's perspectives. The improvements I see for the current section are as follows. Again, i am speaking in terms of pedagogy, not precision. When I say "language X is better" I only mean "language X will be more groovy to programmers.") I put some bolding for skim readers, not for emphasis.

The undecidability of haltingness is invoked from CT. This result is rather shocking to programmers. Likebox does not invoke CT, but gets at un-halting with 'quines' and shows how to construct a counterexample. The programmer is no longer shocked, and given this part of proof, can actually go off to construct a counter-example generator to defy any proposed-halting-detector. He understands. To a mathematician, it seems bizarre because 'quining' sneaks in vast areas of recursion theory, all sorts of other stuff seem left out, it's 'hand-waving' in all the wrong spots. To the coder, who is at heart a constructionist who understands in terms of process, it shows what to do, and that's his mode of understanding. He doesn't want an existence proof of 'quines' (there is one), he wants to know how to make them, which is easy to show. All the rest he sees as details that can be looked up. We should give more references to these 'waved-over' details, which i shall try to do.

The undecidability of halting is really the heart of the matter, to me.

Computational people find intuitive that the Undecidability of Halting implies Incompleteness of Number Theory. They know that a computer is governed by mathematical laws. They think, "you can do mathematical proofs as to whether a certain program halts. If there is a hole in 'haltingness', there is a hole in math." Hand waving, absolutely. That is how these people wave tho. In short, I think we should expand the part on Halting, compress the part on Halting->Godel, shoot up the middle in terms of style between Likebox's more casual style and CBM's more formal, and whatever i forgot to list just now.

Let me take a crack at this, as i have assertions to back up. I am quite sure i wont make the final exposition, but probably a way-point most of which is discarded. But lemme try. I'd urge all editors (myself included) to not get too attached to early drafts. We are (i think) aiming for an effective pedagogy on this directed at coders. To say "we don't think coders will groove on X" does impune the quality of X, and each exposition is beautiful within it's own domain, and we are very much guessing as to what coders groove on.

Oh, and the title of the section, i think shd change. I really have to log off else my partner is going to eject me into the night in a very real and formally decidable way ! Let me take a crack tomorrow (my version will steal heavily from both.) CeilingCrash 01:05, 10 November 2007 (UTC)

I disagree that there is any established consensus for a proof aimed primarily at "coders". I'm not even sure what that means. This is, first and foremost, an article about mathematics. — Carl (CBM · talk) 02:50, 10 November 2007 (UTC)

The incompleteness theorem is not a PhD level recursion theory subject as Likebox seems to imply. It's a basic theorem from mathematical logic, taught in any self-respecting introductory undergraduate course in that subject. I think it's best if the presentation stays in standard mathematical terminology instead of computer terminology, though the article should (and does) link to related results in computability theory. It's true that some computer-inspired proofs (like the one Likebox cited) have been published, so Likebox's proof is not OR. It's also true that logic has been redone from the ground up many times (see sequent calculus, categorical logic, type theory, or ludics for yet more examples), so there are many ways to look at the subject. But my impression is that most introductory logic textbooks use the traditional approach (predicate calculus, FOL, etc), as is natural because the incompleteness theorem is presented along with other basic theorems (completeness, compactness, Lowenheim-Skolem, some model theory, maybe some set theory) that don't fit so well into the computer presentation. See, for example, "A Mathematical Introduction to Logic" by Herbert Enderton. The class I took in college used that book, and it covers the topics listed above and should be pretty readable to anyone who made their way through Gödel Escher Bach.

Basically I agree with CBM that Likebox's proof is better off in an expositional wikibook that wikipedia could link to. I don't understand Likebox's insistence on putting the computer proof into the encyclopedia article (especially the main article about the theorem) and I think devoting much space to its presentation goes against the "undue weight" principle of following what the majority of sources (in this case logic textbooks) do, with a shorter mention of less common approaches. I actually think the article's "proof sketch" section should be shortened a lot further, since it links to another article with a longer proof sketch (perhaps the computer proof could be presented there somehow). It's enough for the main article to explain informally what the theorem says, its significance, its historical context, etc, plus a brief summary of the proof's main ideas. The article is currently too cluttered and should be streamlined in general. —Preceding unsigned comment added by 75.62.4.229 (talk) 05:05, 10 November 2007 (UTC)

Further comment: maybe an expert can correct me on this but I think I see the error in Likebox's references to "language that should have been retired decades ago". It's that Likebox is mostly interested in computer science, and not more traditional (but definitely non-obsolete) areas of mathematics like analysis, topology, probability, etc. Those areas are all based on set theory, and logic (at least as taught in undergraduate math classes, which is as far as I got) is mostly motivated by having to develop axiomatic set theory as the foundation of the rest of mathematics. Set theory is used in math because of (e.g.) all the uncountable structures in subjects like functional analysis that have to be put on a rigorous footing. Computer scientists generally don't care about uncountable structures and they're more interested in decision problems on countable languages, which they study using a somewhat different vocabulary than mathematicians use. The language that Likebox complains about is in fact still necessary and still very actively being used by mathematicians who are nowhere near ready to retire. I.e. if Likebox wants to rework mathematical logic, he or she should also be willing to rework the rest of mathematics starting from set theory the same way, and I don't see that about to happen. So I think we're seeing some cultural chauvinism and/or ignorance on Likebox's part, in what comes across as an attitude that computer theory is the only part of mathematics that really matters and that no one should care about, say, Hilbert space operators (hint: physicists use those all day long). Logic in textbooks is presented the way it is because that's what works best for traditional mathematics even if it's not so great for computer theory. Likebox might like reading Enderton's book that I mentioned above. It gives a much grander view about logic and models than the computer-based approach does. —Preceding unsigned comment added by 75.62.4.229 (talk) 06:03, 10 November 2007 (UTC)

I am skeptical that the comments above are sincere. Since this is a political discussion, perhaps we should limit it to users who do not hide behind a veil of anonymity?Likebox 21:36, 10 November 2007 (UTC)

Actually, on closer reading, maybe they are sincere! Likebox has already reformulated all of mathematics to his own satisfaction from the ground up only using computers and not referencing uncountably infinite sets except as rhetorical devices. It doesn't take as much work as you think. It was essentially done by Godel (closely following Hilbert), when he constructed L. L is defined as the class of all objects predicatively constructed by computer programs deducing from the axioms and running for an ordinal number of steps. It forms a model of Zermelo Frenkel set theory, all of usual mathematics. This seems like a strange idea, but when the ordinals are countable, the computer programs just have lots of while loops which run a countable number of steps. If you take V=L for sets, define proper classes corresponding to what are normally called the "true" power sets, declare that all infinite power classes are Lebesgue measurable, and take as an axiom either that all well-orderable collections are measure zero if you feel conciliatory, or that all ordinals are countable if you are feeling incendiary, you get a good-enough model of mathematics that certainly includes everything any non-logician ever does, including most small large cardinals. It just does not have any truly uncountable sets. These are all proper classes.

Likebox does not care if you agree or disagree with his formulation of mathematics, because Likebox did it only to satisfy himself that it can be done. But he is happy to contribute his decade old proof of Godel's theorem, because it is not original. The only arguably new thing about it is using quining to sidestep Kleene, and that has almost certainly been thought of before.Likebox 22:54, 10 November 2007 (UTC)

The comments are sincere, though it's quite possible that they're incorrect and/or not well-informed, since I'm not an expert on this stuff (that's why I said maybe an expert can correct me). But if you're such an expert, why do you have such trouble with the usual textbook presentation? It worked ok for me (I had a one-semester class using the book that I mentioned). Also, I'm not the anonymous one here: I'm disclosing my personal IP address instead of making up a meaningless nickname like you did (not that there's anything wrong with that).

Dude, I'm not an expert in any way. I just have my opinion. I'm not trying to impose it on other people. I just told you my way of doing math.Likebox 00:46, 11 November 2007 (UTC)

Also, as I tried to make clear, everyone has a problem with the usual textbook presentations. They are incredibly hard to decipher, even for the so-called experts. To see, try to get them to prove that it is undecidable whether a program runs in polynomial or exponential time (without using Rice's theorem).Likebox 00:48, 11 November 2007 (UTC)

But I think trying to jam an unorthodox proof into the article against other editors' judgment (some of whom are experts) counts as trying to impose your views on other people. Otherwise there wouldn't be an RFC. And I don't see what the textbook presentation of the incompleteness theorem has to do with the running time of programs--this isn't a complexity theory article and it's irrelevant that complexity theorists working on complexity topics tend to use different tools than what logicians use on logic topics. Finally I personally thought the incompleteness theorem presentation in Enderton's book was fine. It's a popular book and I think most users (teachers and students) are happy with it. So I can't go along with the claim that "everyone" has a problem with the usual textbook presentations. I can go with "there exists a user with such a problem" which is entirely different, but even if everyone has a problem: as CBM says, Misplaced Pages is not the place to right the wrongs of the world. Maybe your best bet is to write your own textbook and get it published. —Preceding unsigned comment added by 75.62.4.229 (talk) 06:24, 11 November 2007 (UTC)

(deindent) The theorem I was stating about running time is most definitely not a complexity theorem, but a recursion theoretic one, even though it superficially sounds like a complexity theoretic theorem. The theorem is about undecidability of running time, but it really is a version of Rice's theorem, that it is undecidable whether a computer program's output has any definite property. For example, it is undecidable whether a program outputs 1 or 0, and it is undecidable whether a program's output depends on its input. All these things are undecidable for the simple reason that you can SPITE them, but the method in the textbooks is made murky by mixing the input stream with the variable where you print the code. Not to mention unreadable by a nonspecialist.

The proof of Godel's theorem is a single sentence: No computer program P can output all theorems of arithmetic, because then a program which runs P looking for statements about its own behavior can easily and explicitly make a liar out of P. If we are not allowed to say this on this page, there is something wrong.Likebox 06:45, 11 November 2007 (UTC)

As mentioned I'm ok with having a computer proof sketch in the proof sketch article, though the one currently in your user page needs some reorganiztion and style adjustment (e.g. a theory proof shouldn't describe things in terms of techno-artifacts such as cd-roms). CBM and others have made further suggestions that seem good. The computer proof should get less space than the traditional proof by the undue weight principle. I don't think it should go in the main article.

As I said, I will keep the proof on User:Likebox/Gödel modern proof, and not touch this page at all.Likebox 19:07, 12 November 2007 (UTC)

An exposition like User:Likebox/Gödel modern proof is not adequate for an encyclopedia article on a mathematical theorem. It does have the advantage of connecting several topics that are generally considered cool on slashdot.org. It has the disadvantage of being vague to the point that it would be almost impossible to point out an error in the proof without actually disproving the incompleteness theorem. Phrased as an outline of an existing, peer-reviewed proof this would be OK. Unfortunately, exposing something clearly so that laypeople can understand it is not the same thing as conjuring up an illusion of comprehension. Unfortunately, it seems that only mathematicians understand the difference, after many years of having the mistakes in their own proofs pointed out to them by tutors.

The problem is aggravated by the fact that this article has a relatively high profile. In fact, in the past it has been a target of crackpot edits. Too many people have wasted too much time on this discussion. --Hans Adler 20:48, 14 November 2007 (UTC)

Response to RFC

I came to this page in reaction to an RFC. I've spent an hour or so reading through this discussion, and can't claim to understand every point. Some years ago I could have claimed to understand at least one proof of Gödel's incompleteness theorems but it would take me longer than I'm prepared to devote to this to regain that understanding.

What I think I do still understand well is what Misplaced Pages is supposed to be. I would simply urge all participants in this debate to consider whether their view of what should be in this article complies with policies on original research, reliable resources, not being a text book and verifiability, the last of which opens with: "The threshold for inclusion in Misplaced Pages is verifiability, not truth". Phil Bridger 21:58, 12 November 2007 (UTC)

Nobody is arguing about verifiability of correctness. The key issue is whether it is appropriate to use explicit computer programs in a proof, and whether such language is simpler and clearer.Likebox 01:23, 13 November 2007 (UTC)

My point is that the decision on that has to be made on the basis of Misplaced Pages policies. If the use of an explicit computer program in a proof can be sourced to a verifiable reliable source then let's have it in the article. Otherwise leave it out. Misplaced Pages is not the place to argue philosophical issues about what constitutes a valid proof. Phil Bridger 10:10, 13 November 2007 (UTC)

The use of explicit programs has a long history, and this debate is a mirror of an old and longstanding debate in academia. I have left the editing of the article to others, and placed a suggested compromise on the page User:Likebox/Gödel modern proof.

Misplaced Pages is a place where certain questions need to be resolved. What constitutes a valid recursion theory proof is one of those questions. It is not a peripheral issue--- it determines whether simple proofs can be presented on a whole host of other pages, or whether proofs are going to be be cut-and-paste from textbook presentations or absent altogether. Textbook proofs are reworked by secondary authors, and they are, as a rule, the worst proofs in the literature. They are verbose, confused, and inaccurate. It would be a shame if the policy of "no original research" was expanded to "no simplified exposition", because then it will be hard to find anyone to write any proofs of any nontrivial result. In its day, Brittanica included up-to-date discussion of current research, and was not a mirror of the contemporary textbooks. This is part of the reason it was so valuable. Issues of accuracy are easier to adress on Misplaced Pages, since there are thousands of referees for any discussion. Issues of clarity, however, are more insidious, because they have no unique right answer.Likebox 19:41, 13 November 2007 (UTC)

I'm sorry but Misplaced Pages is not the place to resolve the issue of what constitutes a valid proof. As you say this is a long-standing debate in academia, and that is where the debate needs to be, not in an encyclopedia. Phil Bridger 20:10, 13 November 2007 (UTC)

How are you going to write the encyclopedia? It won't get written. If there is more than one way to do something accepted in academia, there should be several presentations on your encyclopedia.Likebox 23:02, 13 November 2007 (UTC)

There is not actually a longstanding debate in recursion theory about what is a valid proof. In particular, since the 1960s it has been very common to avoid writing recursion equations or pseudocode in proofs, and the style developed by Rogers is used by virtually all publications in recursion theory today. I don't understand the claim that textbook proofs are verbose, confused and inaccurate; they are typically much improved from the original proofs in research papers, which are often myopic, focused solely on obtaining a particular result. — Carl (CBM · talk) 20:36, 13 November 2007 (UTC)

You have already made your position clear. Many people believe that you are wrong on this matter, but there is no need for everyone to agree. Write textbook stuff, and let others write review paper stuff. Criticize on notability and verifiability, not on language or style.Likebox 23:05, 13 November 2007 (UTC)

It's perfectly reasonable for editors to be concerned about the way articles are worded. I see no need to have duplicate expositions in the article, and I don't see much support so far in the RFC for duplication. You continue to claim that there is more than one way this is done in academia - could you present a math or computer science text that you are claiming as a model for your sort of exposition? Could you present any evidence that there is a long-running dispute on this issue in academia? — Carl (CBM · talk) 23:16, 13 November 2007 (UTC)

Nope, I am not going to do any of that. I nevertheless maintain my position.Likebox 02:19, 14 November 2007 (UTC)

Sorry, the reason I do not do this is because I do not believe in the authority of experts.Likebox 02:33, 14 November 2007 (UTC)

There is no duplication. You do not prove Rosser, I prove Rosser. Your presentation is imprecise, mine is precise. There is no contest. Your presentation is inferior in every way. That does not mean it should go. That means it should stay, but not overwrite mine.Likebox 02:29, 14 November 2007 (UTC)

I'm sorry, I know we are supposed to comment on content, not on editors, but how much longer are we going to suffer the ravings of this LUNATIC, who has stated repeatedly that he is _not_ interested in consensus, _not_ interested in compromise and who has nothing (it seems) to contribute but bloviating ramblings about how 'his' proof (oh, but it's not OR) is THE BEST PROOF IN THE WORLD EVAR? Is there no recourse for an editor being so C L E A R L Y disruptive? —Preceding unsigned comment added by 71.139.31.151 (talk) 07:46, 14 November 2007 (UTC)

• Unassessed mathematics articles
• Top-priority mathematics articles
• Unassessed Philosophy articles
• Unknown-importance Philosophy articles
• Unassessed epistemology articles
• Unknown-importance epistemology articles
• Epistemology task force articles
• Unassessed logic articles
• Unknown-importance logic articles
• Logic task force articles
• Delisted good articles