Misplaced Pages

This is an old revision of this page, as edited by Trovatore (talk | contribs) at 00:03, 25 September 2008 (→Error in new proof: r to Carl). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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 /Archive04

Recursion sucx?

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

A criticism of this article (from Usenet)

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

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

 On Mon, 11 Aug 2008 09:05:20 -0700 (PDT), MoeBlee <...@...>
 said:
 > ...
 > My point stands: Misplaced Pages 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 Misplaced Pages'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
 Misplaced Pages a terribly unreliable and unsystematic source of information.

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

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

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

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

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

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

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

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

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

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

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

No, of course not . . . an example of Goedel's (awesomely-difficult) original notation is simply a sampler of the true "taste" of the paper (not unlike like the taste of a very difficult Scotch whiskey (e.g. Lagavulin) . . . wow! whew!). For those who don't have a cc of the original paper, the original notation represents a (cautionary, challenging, fun) taste/flavor of what the original contains. And that is the point! That's part of the "educational experience"! With regards to a superb explication in Misplaced Pages 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 " recursion" and "Goedel numbering" and "diagonalization" such an explication is possible. Bill Wvbailey (talk) 02:56, 14 August 2008 (UTC)

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

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

A very simple paraconsistent proof

There is a very simple paraconsistent proof in:

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

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

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

• WP:Articles for deletion/Direct logic
• WP:Articles for deletion/Logical necessity of inconsistency
• Misplaced Pages:Requests for arbitration/Carl Hewitt#Remedies and the enforcement log there
• Category:Suspected Misplaced Pages sockpuppets of CarlHewitt

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

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

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

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

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

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

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

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

1. 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 Misplaced Pages after that happens.

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

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

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

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

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

Recent work by Carl Hewitt 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), 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:

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

Would like to try your hand at drafting something shorter?

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

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

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

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

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

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

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

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

therefore since PA+Con is an extension of PA:

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

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

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

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

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

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

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

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

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

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

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

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

So this is quite interesting:

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

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

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

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

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

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

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

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

Moved 'implications' section to the end

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

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

Boolos' short proof

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

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

section on meaning of the first incompleteness theorem

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

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

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

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

Testing the waters

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

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

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

Error in new proof

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

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

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

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

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

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

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

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

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

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

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

• 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