Talk:Gödel's incompleteness theorems and User talk:82.1.249.98: Difference between pages

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia
(Difference between pages)
Content deleted Content added
VisualWikitext
Likebox (talk | contribs)
6,376 edits
→‎Godel's next major paper: Lengths of proofs: fix omega-consistency screw up
 
2D (talk | contribs)
Rollbackers
12,860 edits
Message re. John Tejada (HG)
 
Line 1: Line 1:
{| class="messagebox standard-talk" id="talkheader" align="center" style="text-align:center;background-color: #FFFFFF;"
|-
! colspan="2" style="border-bottom:1px solid #C0C090; background-color: #F8EABA;" |
This is the [[Wikipedia:Talk pages|talk page]] for discussing changes to the [[{{PAGENAME}}]] ARTICLE. ''Please place discussions on the underlying mathematical issues on the [[Talk:Gödel's incompleteness theorems/Arguments|Arguments page]]''. Non-editorial comments on this talk page may be removed by other editors.
|-
| style="background-color: #FFFFFF;text-align:left;" |
'''Please sign your comments using four tildes (<code><nowiki>~~~~</nowiki></code>).''' Place comments that start a new topic at the bottom of the page and give them <nowiki>== A Descriptive Header ==</nowiki>. If you're new to Wikipedia, please see [[Wikipedia:Introduction|Welcome to Wikipedia]] and [[Wikipedia:FAQ|frequently asked questions]].
| style="background-color: #FFFFFF;" |
<div style="border: 1px solid #C0C090; background-color: #F8EABA; margin-left: 20px; margin-bottom: 0px; margin-right: 3px;">
'''[[Wikipedia:Talk page guidelines|Talk page guidelines]]'''


== October 2008 ==
Please respect [[Wikipedia:Etiquette|Etiquette]], [[Wikipedia:Assume good faith|assume good faith]] and [[Wikipedia:no personal attacks|be nice]].
</div>
|}


[[Image:Information.png|25px]] Welcome to Wikipedia. The <span class="plainlinks">[http://en.wikipedia.org/wiki/John+Tejada?diff=244866120 recent edit]</span> you made to [[:John Tejada]] has been reverted, as it appears to be unconstructive. Use the [[Wikipedia:Sandbox|sandbox]] for testing; if you believe the edit was constructive, ensure that you provide an informative [[Help:Edit summary|edit summary]]. You may also wish to read the [[Wikipedia:Introduction|introduction to editing]]. Thank you. <!-- Template:uw-huggle1 --> [[User:DavidWS|DavidWS]] ([[User talk:DavidWS|talk]]) 23:00, 12 October 2008 (UTC)
{{maths rating|frequentlyviewed=yes|class=Bplus|importance= top|field=foundations}}
{{philosophy|importance=|class=|epistemology=yes|logic=yes}}

{{DelistedGA|8 May 2006}}

{{archive box|
* [[/Archive01]]
* [[/Archive02]]
* [[/Archive03]]
* [[/Archive04]]
}}



==Recursion sucx?==
By computer science jargon, the theorem says: ''Recursion sucx!''. But we knew that! ''<span style="color: #800000; background-color: #FFFFA0; padding: 1px 2px 3px 2px">Said: [[User:Rursus|<span style="color: blue">Rursus</span>]] [[User talk:Rursus|<span style="color: #800000">☻</span>]]</span>'' 10:59, 4 August 2008 (UTC)

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

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

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

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

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

[[Special:Contributions/207.172.220.155|207.172.220.155]] ([[User talk:207.172.220.155|talk]]) 07:22, 12 August 2008 (UTC)


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

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

:It's hard to see what Menzel means by "The current statement of the first theorem is now both wordy and inaccurate (notably, the statement of the theorem in the first sentence doesn't rule out the possibility of a complete but unsound theory" - the statement explicitly says the theory must be consistent. Moreover, it's hard to see how to make the statement much shorter. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 11:31, 12 August 2008 (UTC)
:::I think the point about the "complete but unsound" part is that the current statement doesn't exclude the following situation: There is a true statement that the theory doesn't prove, because the theory proves, rather, the (false) negation of the statement. This is a fair point; the theorem ''does'' exclude that situation, and we don't currently ''say'' that it does. I don't think it's extremely important to the foundational impact of the theorem (who wants to found mathematics on a theory that proves falsehoods?) but it is strictly speaking part of the theorem.
:::Most of the discussion around this point has been objections to calling the sentence ''true'', which stem mostly from misunderstandings (you can certainly take the view that the sentence doesn't have a truth value, but it's hard to see then how you would assign a truth value to the hypotheses). This is an entirely different point and I'm not entirely sure how to respond to it. It would be nice to keep the point that the sentence is true, precisely as a counter to the muddled presentations by the popularizers. --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 17:36, 12 August 2008 (UTC)
::::What do you make of the sentence "That is, any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete."? It may be that the "that is" is not quite the right choice of words, since the quoted sentence is strictly speaking stronger than the one before it. But the quoted sentence does seem to exclude the possibility that the theory is complete... Maybe we can come up with a better overall phrasing of the theorem; that would be a positive outcome to this discussion. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 01:54, 13 August 2008 (UTC)
:::::Hmm, maybe. Maybe just drop "that is" and append the sentence? --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 02:17, 14 August 2008 (UTC)
:: I'd refer Mr. Menzel (assuming he deigns to read Wikipedia at all) to [[WP:SOFIXIT]].[[User:Zero sharp|Zero sharp]] ([[User talk:Zero sharp|talk]]) 15:00, 12 August 2008 (UTC)

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

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

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

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


I rearranged the statement of the first theorem, which removed the "that is" and made it more clear which statement is more general. I'm planning to work on the article in a little more detail over the next couple days. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 12:55, 18 August 2008 (UTC)

==A very simple paraconsistent proof==
There is a very simple paraconsistent proof in:

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

--[[Special:Contributions/67.180.248.94|67.180.248.94]] ([[User talk:67.180.248.94|talk]]) 06:05, 14 August 2008 (UTC)

I removed the Hewitt paraconsistency stuff from the article on the grounds that it is cited to a non-peer-reviewed source and that Carl Hewitt is banned from inserting references to his own work on Wikipedia. It was probably inserted by Hewitt. See further discussion at:
*[[WP:Articles for deletion/Direct logic]]
*[[WP:Articles for deletion/Logical necessity of inconsistency]]
*[[Wikipedia:Requests for arbitration/Carl Hewitt#Remedies]] and the enforcement log there
*[[:Category:Suspected Wikipedia sockpuppets of CarlHewitt]]
:[[Special:Contributions/76.197.56.242|76.197.56.242]] ([[User talk:76.197.56.242|talk]]) 02:44, 17 August 2008 (UTC)

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

* {{cite web | author=Hewitt, Carl| year=2008 | title=Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency | format= | work=[http://www.springerlink.com/content/tl0638746601/?p=26df887cb7264f41b9167fe5a4e13073&pi=0 Coordination, Organizations, Institutions, and Norms in Agent Systems III] | url=http://hewitt-seminars.blogspot.com/2008/03/large-scale-organizational-computing.html}} Jaime Sichman, Pablo Noriega, Julian Padget and Sascha Ossowski (ed.). Springer-Verlag.

--[[Special:Contributions/67.169.145.52|67.169.145.52]] ([[User talk:67.169.145.52|talk]]) 03:30, 17 August 2008 (UTC)

# That looks like a conference proceedings, not a refereed journal. See the comments at the "Direct logic" AfD linked above for discussion of this point as applied to this topic.
::Unfortunately, you are incorrect, it is was refereed.--[[Special:Contributions/98.97.104.6|98.97.104.6]] ([[User talk:98.97.104.6|talk]]) 18:51, 17 August 2008 (UTC)
# Even if it's in a journal, the linked article appears to have no relevance to Gödel's incompleteness theorems, which are theorems of classical logic.
::Unfortunately, you are incorrect. Incompleteness theorems also apply to non-classical logics.--[[Special:Contributions/98.97.104.6|98.97.104.6]] ([[User talk:98.97.104.6|talk]]) 18:51, 17 August 2008 (UTC)
# It also appears to have very limited notability in that Google Scholar finds no citations to it of any sort. If some appear in the future, we can consider it for Wikipedia after that happens.
::Unfortunately, Google Scholar tends to be both spotty and tardy in its indexing. Consequently, it doesn't indicate much of anything in academic work. On the other hand, the regular Google index has lots of references to the work.--[[Special:Contributions/98.97.104.6|98.97.104.6]] ([[User talk:98.97.104.6|talk]]) 18:51, 17 August 2008 (UTC)
So, based on both verifiability and [[WP:Undue weight]], I don't think the reference should be restored. [[Special:Contributions/76.197.56.242|76.197.56.242]] ([[User talk:76.197.56.242|talk]]) 07:32, 17 August 2008 (UTC)
::The paper has become quite famous. The results have been presented in lectures at AAMAS'07, Edinburgh, Stanford (on at least 3 occasions), AAAI (twice), and no doubt others.--[[Special:Contributions/98.97.104.6|98.97.104.6]] ([[User talk:98.97.104.6|talk]]) 18:51, 17 August 2008 (UTC)

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

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

:Recent work by [[Carl Hewitt]]<ref name=Hewitt2008>[[Carl Hewitt]], [http://hewitt-seminars.blogspot.com/2008/03/large-scale-organizational-computing.html Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency] in ''Coordination, Organizations, Institutions, and Norms in Agent Systems III'', Springer-Verlag,&nbsp;2008.</ref> extends Gödel's argument to show that, in a particular [[paraconsistent logic]] (that is outside the restrictions on self-reference of Gödel's framework<ref name=Feferman1984>[[Solomon Feferman]], [http://links.jstor.org/sici?sici=0022-4812(198403)49%3A1%3C75%3ATUTTI%3E2.0.CO;2-D Toward Useful Type-Free Theories, I], ''Journal of Symbolic Logic'', v.&nbsp;49&nbsp;n.&nbsp;1 (March 1984), pp. 75&ndash;111.</ref>), sufficiently strong paraconsistent theories are able to prove their own Gödel sentences, and are thus inconsistent about the provability of the Gödel sentence (as well as being incomplete). Here incomplete means that it is paraconsistently provable that neither the Gödel sentence nor its negation can be proved. In this context, questions about the truth of the Gödel sentence do not make any sense.

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

Would like to try your hand at drafting something shorter?

--[[Special:Contributions/12.155.21.10|12.155.21.10]] ([[User talk:12.155.21.10|talk]]) 14:44, 18 August 2008 (UTC)

:Yes, I'll do that later, along with the section on Boolos' proof. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 14:58, 18 August 2008 (UTC)

::I added a very short summary. I'm sure the wording can be improved, but I don't think more detail is necessary. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 16:46, 20 August 2008 (UTC)

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

:''for every theory T satisfying the hypotheses, it is a theorem of [[Peano Arithmetic]] that'' Con(''T'')→''G''<sub>''T''</sub>''
:where Con(''T'') is the natural formalization of the claim "''T'' is consistent", and ''G''<sub>''T''</sub> is the Gödel sentence for ''T''.

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

:''it is a theorem of [[Peano Arithmetic]] that'' Con(''PA+Con'')→''G''<sub>''PA+Con''</sub>''

therefore since ''PA+Con'' is an extension of ''PA'':
:''it is a theorem of PA+Con that ''Con(''PA+Con'')→''G''<sub>''PA+Con''</sub>"

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

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

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

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

::::It may be easier to see why PA proves Con(T) &rarr; G<sub>T</sub> if you look at it in contrapositive form: if G<sub>T</sub> fails, that means Bew(G<sub>T</sub>) holds, so we want to prove Bew(G<sub>T</sub>) implies ~Con(T). This is exactly what is obtained by formalizing the proof of the incompleteness theorem in PA, replacing "provable" with Bew throughout. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 16:34, 21 August 2008 (UTC)

:::::Since "it is a theorem of ''PA+Con'' that Con(''PA+Con'')→''G''<sub>''PA+Con''</sub>" and "Con(''PA+Con'') is an axiom of ''PA+Con''", ''PA+Con'' proves its own Gödel sentence and is indeed inconsistent.--[[Special:Contributions/98.210.236.229|98.210.236.229]] ([[User talk:98.210.236.229|talk]]) 23:32, 22 August 2008 (UTC)

::::::As Trovatore and I have pointed out, it's not clear at all what the theory you call "PA + Con" is supposed to be. It certainly isn't PA + G<sub>PA</sub>. What is it, exactly? &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 23:38, 22 August 2008 (UTC)

:::::::''PA+Con'' is defined by a fixed point construction in much the same was as the Gödelian sentence. It basically is ''PA'' plus the axiom "I am consistent" analogous to ''G<sub>PA</sub>'' (I am not provable in ''PA''). Thus you are correct that ''PA+Con'' is not the same as ''PA+G<sub>PA</sub>'' --[[Special:Contributions/67.169.145.32|67.169.145.32]] ([[User talk:67.169.145.32|talk]]) 06:01, 23 August 2008 (UTC)
::::::::So it ''is'' true that the process of adjoining Con(''T'') to an r.e. theory ''T'' has a fixed point. As an example, just let every sentence in the language of arithmetic be an axiom of ''T''. This is an r.e. theory, and you can formulate Con(''T'') in some standard way based on the (simple!) algorithm that generates its axioms, and you will find out, in the end, that Con(''T'') was in fact an axiom of ''T'' all along.
::::::::But of course this ''T'' is inconsistent, and so is every fixed point of the process.
::::::::By the way, you can't get to such a fixed point via iteration starting with PA. PA is consistent, and so is PA+Con(PA), and so is PA+Con(PA)+Con(PA+Con(PA)), and so on, through not only all finite iterations, but into the transfinite, as far as you can actually make sense of it. Therefore none of these theories contains its own consistency as an axiom. --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 07:34, 23 August 2008 (UTC)
:::::::::So this is ''quite interesting'':
::::::::: '''If a theory ''' ''T'' '''has an axiom that it consistent, then''' ''T'' '''is inconsistent!'''
:::::::::--[[Special:Contributions/67.169.9.72|67.169.9.72]] ([[User talk:67.169.9.72|talk]]) 22:52, 23 August 2008 (UTC)
::::::::::Yes. This follows easily from the second incompleteness theorem. --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 03:15, 24 August 2008 (UTC)
:::::::::::Con(''PA+Con'') is intuitively true. But adding it as an axiom classically causes the wheels to come off. So we might as well throw in the towel (i.e. admit the inherent inconsistency) and go over to paraconsistent logic.--[[Special:Contributions/67.169.9.72|67.169.9.72]] ([[User talk:67.169.9.72|talk]]) 13:05, 24 August 2008 (UTC)
::::::::::::That's one way of looking at it, but certainly not the "standard" one. Apart from Hilbert's program, what's the reason to ''expect'' that a formal theory of arithmetic will prove its own consistency? Experience has shown there's no real difficulty for mathematicians if the theories they use to study arithmetic, set theory, etc. don't prove their own consistency, since the consistency can be studied by other means, and the questions studied within the theories are typically mathematical rather than metamathematical. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 16:58, 24 August 2008 (UTC)
:::::::::::Look, you ''can't'' "add Con(''PA+Con'')", because there's no such thing as ''PA+Con''. You haven't told us, in any useful way, what it's supposed to be in the first place. There are indeed fixed points of the process of adding a theory's consistency to the theory; I gave an example, but it's not in any reasonable way describable as starting with PA and adding the axiom "I am consistent". --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 19:14, 24 August 2008 (UTC)
I reworded the footnote and added references throughout. Please feel free to keep rewording it if I've missed any subtle points. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 20:12, 21 August 2008 (UTC)
:I think that's nicely done—it's clearer and more direct than my original wording, which was more aimed at being a bulletproof response to the quibblers than at explaining what was really going on. Referencing Torkel is also a nice touch. --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 20:17, 21 August 2008 (UTC)

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

:While we're at it, it would be nice to tighten up the referencing in that section. There are several half-done footnotes that should be replaced by complete references. Does anyone have an interest in that area? &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 12:52, 18 August 2008 (UTC)

== Boolos' short proof ==

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

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

== section on meaning of the first incompleteness theorem ==

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

The "meaning" section does need copyediting for tone - it has a lot of "we" and "you". The section on the second incompleteness theorem needs editing for structure - perhaps some subsections. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 14:08, 18 August 2008 (UTC)

I also think the section on '''limitations of Goedel's theorems''' could be merged into the "meaning" section. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 14:12, 18 August 2008 (UTC)

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

== Testing the waters ==

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

:<FONT SIZE=1000>NO!</FONT> <span style="font-size: smaller;" class="autosigned">—Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[Special:Contributions/71.139.24.118|71.139.24.118]] ([[User talk:71.139.24.118|talk]]) 02:04, 25 September 2008 (UTC)</span><!-- Template:UnsignedIP --> <!--Autosigned by SineBot-->

:What has changed since the last time this was discussed? The (long) discussion starts at [[Talk:G%C3%B6del%27s_incompleteness_theorems/Archive03#New_Proof]] and continues for the rest of Archive03. There was even an RFC where the "computational proof" was rejected. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 21:08, 24 September 2008 (UTC)

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

=== Error in new proof ===

The new proof also has problems with correctness, such as:
<blockquote>
Write the computer program ROSSER to print its own code into a variable R and look for either 1.R prints to the screen or 2.R does not print to the screen. If ROSSER finds 2, it prints "hello world" to the screen and halts, while if it finds 1, it halts without printing anything.<br/><br/>

S can prove neither ROSSER prints to the screen nor the negation ROSSER does not print to the screen. So S is necessarily incomplete.
</blockquote>
This does not prove the incompleteness theorem without the assumption that when ''S'' proves that "R prints to the screen", this actually means there is a computation in which R prints to the screen. The statement "R prints to the screen" is a Sigma^0_1 statement, and so it is still possible for S to be consistent but not &omega;-consistent, in which case S may well prove Sigma^0_1 statements such as this without there being any actual natural number that satisfies them. That is, S may prove there is a computation history which ends in R printing to the screen, but it may be that the only such histories are encoded by nonstandard natural numbers. Thus it will be necessary to assume S is &omega;-consistent in order to actually obtain a contradiction.&mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 21:17, 24 September 2008 (UTC)
:As I recall, I thought Ron's proof through here, and it did turn out to be correct, though it required a subtle observation that he didn't bother to mention. I don't remember the details at the moment and don't have time to think about it right now. --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 21:22, 24 September 2008 (UTC)
::If you're thinking of the argument I think you are, there's not nearly enough explanation there to follow it. That is, you may be thinking that if S proves that R prints something, it means that S proves that (S proves R does not print anything). Also, S will prove (S proves R does print something). Thus S will prove (S proves a contradiction). That leaves an argument to be made that S ''actually does'' prove a contradiction, especially since we all know that there are consistent theories that prove Pvbl(0=1). &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 21:41, 24 September 2008 (UTC)
:::I think the point was something like, if S proves that R prints, or if it proves that it does not print, then R must in fact halt (because it would find the proof), and S must prove that R halts (because S is strong enough to find all proofs of halting). Therefore S must prove both that R prints and that it doesn't print. Or something like that. --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 21:49, 24 September 2008 (UTC)
::I'm sorry for being so brusque. My overall concern isn't whether the argument is "fatally flawed" - I'll assume, by way of good faith, that it would be possible to patch together a convincing proof using essentially the method provided, even if the current wording isn't there yet. My first concern is that the text provided is not even clear to people who do have a good understanding of what's going on - so it will be incomprehensible to people who don't already have a good understanding. My second concern is that it seems that the only way to actually draw a contradiction from this type of argument is to be more precise about the arithmetization, and this undercuts the general argument that the "computational proof" is clearer because it avoids arithmetization. My third concern is that, since this argument is not presented in texts, we have nowhere to send people who ask "where can I read a full explanation of this argument"? &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 22:38, 24 September 2008 (UTC)
:::I'm certainly not saying that Likebox's proof should be included as is (or even, necessarily, at all). It's true that it really ought to be sourced, and I also agree that Ron is not paying enough attention to the need to connect the result with arithmetic (which after all is where the question comes from).
:::I do think though that it's kind of a nice way to think about it, once you make your way through the land mines. Here's the completion to the argument. Suppose S proves or refutes the claim that R prints. Then R must in fact halt. When it halts, it is either on a proof from S that R prints or a proof from S that R doesn't print, but then it does the opposite. S is then strong enough to prove that R follows that finite sequence of steps and does that opposite thing. Thus in either case, S proves both that R prints and that it doesn't print. --[[User:Trovatore|Trovatore]] ([[User talk:Trovatore|talk]]) 00:03, 25 September 2008 (UTC)
::::Thanks, I see. For some reason when I was reading between the lines earlier I was reading a different proof into it. By the way, I thought we ought to have an article on [[Rosser's trick]]. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 00:28, 25 September 2008 (UTC)

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

:What you put in wasn't a proof at all - it was a claim that a certain construction could be turned into a proof. Please see my comment of 22:38. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 02:51, 25 September 2008 (UTC)

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

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

:::In particular, I would specifically like to see a source provided for any mathematical logic text that proves the incompleteness theorem using the recursion theorem (that is, using programs that begin by using their own source code as the input to some process). &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 03:56, 25 September 2008 (UTC)

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

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

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

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

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

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

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

::::::::: We've been through this before, at the RFC. Wikipedia isn't the place for you to pursue an agenda to change the field of recursion theory... What has changed since the RFC? &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 04:52, 25 September 2008 (UTC)

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

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

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

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

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

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

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

==3rd Opinon==
I am requesting a [[WP:3O]], specifically on Likebox's insistance on his changes to the article, despite repeated attempts by multiple editors to explain to them that, irrespective of their correctness, they are not in place in this article. The technical objections have been amply explained, but clearly this edtior needs to understand how WP is supposed to work regards: consensus, no tendentious editing and civility. [[User:Zero sharp|Zero sharp]] ([[User talk:Zero sharp|talk]]) 13:59, 25 September 2008 (UTC)
:Actually, I think civility is not an issue here (other than that some effort is needed to stay civil when arguing with Likebox – CBM is spectacularly good at that), and tendentious editing is a bit of a red herring. Let's try to stay focused. --[[User:Hans Adler|Hans Adler]] ([[User talk:Hans Adler|talk]]) 14:20, 25 September 2008 (UTC)

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

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

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

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

== Proposing a different approach for the computability section ==

After some reflection last night, I think that a large flaw in the existing computability section is that it is narrowly focused on one proof (the one sourced to Kleene), rather than the broader relationship between computability and incompleteness. So I propose that instead of giving any long proof sketches in that section, we briefly discuss several different ways that computability and incompleteness interact. [http://en.wikipedia.org/w/index.php?title=G%C3%B6del%27s_incompleteness_theorems&oldid=240915376#Relationship_with_computability This version] is my first attempt at this. I think that this will be more informative to a reader (who is not assumed to have a background in computability theory) than a more technical discussion would. What do you think? &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 15:25, 25 September 2008 (UTC)

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

: Which proof is it that nobody finished? &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 20:12, 25 September 2008 (UTC)

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

:: The thing that arguably isn't finished there is just the construction of "Bew" (to explicitly make it you have to work very hard, and to make it obvious that it is possible to make it you need to talk about universal computation in arithmetic, and that gets you back to the computational stuff).[[User:Likebox|Likebox]] ([[User talk:Likebox|talk]]) 20:42, 25 September 2008 (UTC)
:::On the other hand, to make it obvious that [[Kleene's T predicate]] is actually represented by an arithmetical formula, as would be necessary to flesh out the computational proofs, you have to work equally hard. Depending on the specific model of computation, it may still be necessary to formalize enough provability to allow the computations to operate on proofs. The arithmetization is always going to be present in some form or another. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 21:01, 25 September 2008 (UTC)

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

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

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

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

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

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

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

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

=== Computational formulation ===

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

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

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

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

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

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

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

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

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

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

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

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

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

== Godel's next major paper: Lengths of proofs ==

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

:This proof appears in ''The Undecidable'' on p. 82. It was translated from "the original ariticle in ''Ergebnisse eines mathematischen Kolloquiums'', Heft 7(1936) pp. 23-24, with the kind permission of the publishers, Franz Deuticke, Vienna" (ibid). This version appears with an added "remark added in proof [of the original German publication]:
::"It may also be shown that a function which is computable in one of the systems '''S<sub>i</sub>''' or even in a system of transfinite type, is already computable in '''S<sub>1</sub>'''. Thus, the concept "computable" is in a certain definite sense "absolute", while practically all other familiar metamathematical concepts (e.g. provable, definable, etc) depend quite essentially on the system with respect to which they are defined" (p. 83).
:Bill [[User:Wvbailey|Wvbailey]] ([[User talk:Wvbailey|talk]]) 22:07, 26 September 2008 (UTC)

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

The theorem has three parts:

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

: Given a computable function F, construct NGODEL which prints its own code into the variable R, and looks for all proofs of length less than F(N), where N is the length of R. NGODEL looks for the theorem "R halts", and if it finds it, it goes into an infinite loop. Once it finishes running, it halts.

: Since NGODEL halts, S will prove it, but it will necessarily do so with a proof of length greater than F(N).

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

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

:: (I screwed up the previous program and the mistake infected this one: you need an omega-consistent S to make the above true. Rosserize to get a correct proof. Godel actually proved 3 in his paper, so he didn't implicitly use a Rosser trick here. But I still think his intuition was 2.)

:: Write NROSSER to print its code into R, then look for proofs in S of length <F(N) of '''R does not print'''. If it finds it, it prints and halts. At the end of the search, it halts without printing.

:: Now S will prove that R does not print with a long proof, while S+consis(S) will prove that R does not print with a short proof.

Godel also claimed

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

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

:: I remember now--- it's a little tricky. Here's the basic idea-- write program TESTP which runs P for N steps where N is huge, to see if P halts. If TESTP finds that P halts, it goes into an infinite loop. If P did not halt after N steps, TESTP halts.

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

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

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

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

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

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

::: There are only finitely many proofs of length less than C characters, and by putting them together end to end with "ors" between then, you can find a prove that P does not halt.

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

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

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

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

== Post's 1920s paper ==

There is also Post, who in the 1920s examined a system which turned out to be equivalent to a Turing machine, and proved some kind of undecidability theorem, or at least foreshadowed it. There was controversy over whether Godel was directly or indirectly inspired by Post, because there was no attribution. Post later got credit for his work, but it was never made out to be as important as it possibly was.[[User:Likebox|Likebox]] ([[User talk:Likebox|talk]]) 17:37, 27 September 2008 (UTC)

: I don't remember where I read this nor am I sure that it is accurate. I was hoping someone would clarify. Post system here redirects to a 1936 work.[[User:Likebox|Likebox]] ([[User talk:Likebox|talk]]) 20:50, 27 September 2008 (UTC)

Revision as of 23:00, 12 October 2008

October 2008

Welcome to Wikipedia. The recent edit you made to John Tejada has been reverted, as it appears to be unconstructive. Use the sandbox for testing; if you believe the edit was constructive, ensure that you provide an informative edit summary. You may also wish to read the introduction to editing. Thank you. DavidWS (talk) 23:00, 12 October 2008 (UTC)[reply]

Retrieved from "https://en.wikipedia.org/w/index.php?title=Talk:Gödel%27s_incompleteness_theorems&oldid=244867032"