Talk:Gödel's incompleteness theorems/Arguments/Archive 3

Archive 1

Archive 2

Archive 3

Hilarious

There is an old cartoon showing a fellow sitting in a restaurant having consumed his meal, with a waiter standing over him with a bill, and the fellow muses "I was always fascinated by the possibility that the foundations of mathematics may contain a contradiction which would then invalidate these calculations". It seems to have come true in the world of C.H. admirers. I hereby invite comments to clarify this (in addition to Carl's comment above which apparently should have been sufficient). Tkuvho (talk) 06:03, 4 January 2011 (UTC)

How about we not poke the trolls? —David Eppstein (talk) 06:17, 4 January 2011 (UTC)

Of course, inconsistencies have been common to logic for thousands of years. The traditional approach for dealing with logical inconsistencies has been to further restrict the rules of logic. The difficulty posed by the Gödelian paradox was that the classical logicians wanted to have the proof of the incompleteness theorem while at the same time preserving classical mathematical logic. So Gödel invented the convoluted "meta-theory" exception (a theory is for some reason not allowed to speak of its own provability) igniting the whole controversy. Which is preferable: transitioning to inconsistency robust logic or imposing the "meta-theory" exception? 67.169.144.115 (talk) 06:54, 4 January 2011 (UTC)

Impposing Gödel's meta-theory restrictiuon would be a great hardship in computer science. For example, it woud not be possible to express the following:

P, (P ⊢ Q) ⊢ Q

71.198.220.76 (talk) 17:22, 4 January 2011 (UTC)

On the other hand, classical mathematical logic has over 2,500 years of tradition behind it. 99.29.247.230 (talk) 17:42, 4 January 2011 (UTC)

The original development of metamathematics is due to Hilbert, not Gödel. Hilbert began using metamathematical methods in the early 20th century and used the term "metamathematics" in print in 1925. Gödel attended lectures by Hilbert in 1928, where Hilbert surely would have spoken about these things.

Moreover, Gödel did not in any way "limit" his systems; it's just an inherent property of consistent formal systems that they cannot define their own truth predicate (see [1]). It's not as if the systems Gödel studied had this ability before he somehow removed it. — Carl (CBM · talk) 18:35, 4 January 2011 (UTC)

Metamathematics was developed as the mathematical study of mathematics iteself. For example Gödel's Completeness Theorem for First-Order Logic is a theorem of metamathematics. However, inconsistency emerged when Gödel developed his incompleteness proof for Principia Mathematica. So Gödel imposed the restriction that statements like the following are not allowed:

P, (P ⊢ Q) ⊢ Q

Note that the above statement is about provability (⊢) and not about truth. Consequently the theorem on the Undefinability of Truth[2] (first proved by Gödel although he did not press the point of piority) that you quoted is not relevant.71.198.220.76 (talk) 19:20, 4 January 2011 (UTC)

As far as anyone knows, Principia Mathematica is consistent. Indeed, there are published consistency proofs of it. — Carl (CBM · talk) 19:57, 4 January 2011 (UTC)

The problem comes from the principle that Gödel introduced in proving incompleteness to roundtrip between numbers and provable propositions. There are no convincing proofs that Principia Mathematica+Roundtripping is consistent. 63.249.116.52 (talk) 22:04, 4 January 2011 (UTC)

Gödel didn't introduce, define, or mention "roundtripping". The systems that Gödel studied are consistent, so they don't have any way to assert that the formula named by a Gödel number is true. — Carl (CBM · talk) 22:34, 4 January 2011 (UTC)

Unfortunately, User:CBM (above) again confused provability with truth. The roundtripping between numbers and provable propositions introduced by Gödel to prove incompleteness was defined purely in terms of provability. However, Gödel number roundtripping introduced new power into Principia Mathematica because incompleteness cannot be proved in Principia Mathematica without using Gödel number roundtripping. 171.66.73.158 (talk) 00:50, 5 January 2011 (UTC)

Principia Mathematica was finished before Gödel's work, so it was impossible for him to add anything new to it. The incompleteness theorems apply to Principia and to consistent first-order theories like Peano arithmetic. The incompleteness theorems can be proved in much weaker theories, in particular they can be proved in primitive recursive arithmetic (PRA). None of these theories has "roundtripping", at least in the sense that none of them has any way to express that the formula corresponding to a given Gödel number is true. Somehow all the standard literature on the incompleteness theorems manages to get by without roundtripping, as well. — Carl (CBM · talk) 01:30, 5 January 2011 (UTC)

As mentioned previously, Gödel number roundtripping is about provability and not about truth. User:CBM keeps missing this elementary point. Of course it is possible to add Gödel number roundtripping to Principia Mathematica in order to prove incompleteness, which is what Gödel did to map back and forth between numbers and provable propositions. And literature since then has used roundtripping to prove incompleteness of a variety of theories. Even Hewitt used roundtripping in his article Common sense for concurrency and inconsistency robustness using Direct Logic(TM) and the Actor Model and video Wittgenstein versus Gödel on the Foundations of Logic. 171.66.90.148 (talk) 02:36, 5 January 2011 (UTC)

The term "roundtripping" itself was invented by Hewitt, and has no general meaning in logic outside of Hewitt's work. Hewitt's definition "roundtripping" includes an operation (Hewitt calls it "abstraction") that takes a Gödel number and asserts (the truth of) the corresponding formula. Gödel's incompleteness theorem does not assume that the theory at hand has any such operation, and no consistent theory will have one. In particular, neither the object theory nor the metatheory in Gödel's proofs include an abstraction operation that takes a term for a Gödel numebr and converts it into a formula. Therefore Gödel's proof does not have "roundtripping" as Hewitt defines it. — Carl (CBM · talk) 02:56, 5 January 2011 (UTC)

Unfortunately, you are mistaken about Hewitt's work. Abstraction does not assert the truth about anything. In the case of Gödel's theory:

1. Abstraction maps a Gödel number to the the corresponding sentence.
2. Reification maps a sentence to the the corresponding Gödel number.

Going back and forth is called Gödel number roundtripping, which is what is needed to prove the incompleteness theorem.66.92.0.185 (talk) 03:44, 5 January 2011 (UTC)

For example, $\llcorner 5\lrcorner$ is a formula that is true if and only if the formula that has Gödel number 5 is true. In this sense, abstraction is an operation that takes a term and asserts the truth of the formula whose Gödel number is that term. You could rephrase this as: abstraction is an operation which allows someone working in a theory, having constructed a Gödel number, to assert the truth of the formula corresponding to that number.

One noticeable aspect of the standard proofs of Gödel's theorem is that they do not have anything corresponding to this abstraction operation. For example, look at the proof of diagonal lemma here. There is a Gödel numbering operation, #, but there is no inverse of this operation in that proof. — Carl (CBM · talk) 03:55, 5 January 2011 (UTC)

Unfortunately, you still misunderstand Hewitt's work. If $n$ is the Gödel number of a sentence, then $\llcorner n\lrcorner$ is the corresponding sentence. There is no "truth" involved and no "truth" asserted. Because the proof in the Wikipedia article Incompleteness theorem is not a rigorous proof, it omits formally naming the inverse operation and uses English instead. Nevertheless, both abstraction and reification are required for the proof. The statement and proof of the Diagonal Lemma is much simpler in Hewitt's article than in the Wikipedia article. Hewitt's proof of the Diagonal Lemma shows explicitly where roundtripping is required. (And truth is not involved!) 63.249.108.250 (talk) 04:57, 5 January 2011 (UTC)

The point is that, as per Tarksi's indefinability theorem, no sufficiently strong consistent theory of arithmetic with a Gödel numbering #(.) can have a formula $T(z)$ such that for every formula φ the equivalence $\phi \leftrightarrow T(\#(\phi ))$ holds. Therefore no consistent theory can include a syntactic operation $\llcorner x\lrcorner$ such that $\llcorner \#(\phi )\lrcorner$ gives the formula φ, because every formula φ is certainly equivalent to itself. This argument does not assume $\phi \leftrightarrow T(\#(\phi ))$ is provable, only that it is true, which it is in Hewitt's system because of the way that the abstraction operator is defined.

One of the hypotheses of the incompleteness theorems is that the theory at hand is consistent – so the theory being proved incomplete will never include the abstraction operation.

In particular, Hewitt's proof does not work for proving the incompleteness of ordinary Peano arithmetic, which is a consistent first-order theory that does not include any abstraction operation. Hewitt's proof of the diagonal lemma also does not work for Peano arithmetic, for the same reason. On the other hand, the methods used in the standard proofs assume consistency, which Hewitt's system doesn't have. So the methods that Hewitt uses are orthogonal to the methods usually employed; they apply to different collections of theories. — Carl (CBM · talk) 05:30, 5 January 2011 (UTC)

Tarski's $T$ predicate is a giant red herring. In Gödel's theory, a sentence is a character string and therefore ⌈⌊s⌋⌉ = s which doesn't cause any problem with consistency because it can be done entirely within Peano arithmetic. The problem is that more than Peano arithmetic is needed to prove the incompleteness theorem, namely, roundtripping is required. The proof of the incompleteness theorem requires Peano+Roundtripping. However, Peano+Roundtripping is inconsistent. (Hewitt dealt only with provability and never spoke of truth in these proofs.) This was all explained in Gödel versus Wittgenstein. 171.66.86.197 (talk) 21:58, 7 January 2011 (UTC)

Note that Carl Hewitt himself acknowledges this point on page 16 of the current (54th) version of his arxiv post. Namely, he writes here that his "reification" is only similar to Goedel's numbering, implicitly acknowledging that he is working in a different system from Goedel's. Tkuvho (talk) 06:06, 5 January 2011 (UTC)

In the footnote to which you are referring, Hewitt should have been more specific and said that reification is a generalization of Gödel numbering.171.66.86.197 (talk) 21:58, 7 January 2011 (UTC)

Inaccurate description of work by Professor Hewitt

I noticed that someone deleted an editor's suggestion of a less inaccurate description of the work of Professor Hewitt that read as follows: "Carl Hewitt has proposed that a powerful inconsistency robust logic (which is inconconsistent becuse theories can prove their own incompleteness) has applications in software engineering and the Internet."

What is the motivation for Wikipedia having an inaccurate description of Hewitt' work? 71.198.220.76 (talk) 19:21, 5 December 2010 (UTC)

The description in the article is, "Carl Hewitt (2008) has proposed that (inconsistent) paraconsistent logics that prove their own Gödel sentences may have applications in software engineering.". Apart from differing adjectives, that's that same as the text you quoted. — Carl (CBM · talk) 23:11, 5 December 2010 (UTC)

User:CBM is being disenguous in trying to cover up controversies that he would prefer to censor.

• The first constroversy is between paraconsistency and and the much stronger criterion of inconsistency robustness. Paraconsistency merely means that not everything can be inferred from an inconsistency. (Thus a theory is paraconsistent even if a rule is added to the effect that an inconsistency infers that the moon is made of green chees.) Inconsistency robustness requires that nonsense cannot be inferred from just an inconsistency.
• A second way that User:CBM is being disengenous is by insulting Professor Hewitt's work by claiming it only "may" have applications to software engineering and omitting discussion of the Internet altogether
• Also, he is trying to censor mention of the published paper referenced above.

There will be a symposium about the subject this summer, see Robustness 2011 at Stanford.

70.137.154.215 (talk) 18:12, 6 December 2010 (UTC)

Accusing fellow editors of "covering up", "censoring", etc. is against wikipedia policy. As far as the specific point concerning applications, if your basis for this is an arxiv post you mentioned above, then such as claim is considered as unsourced by wiki standards and should be deleted altogether. Good luck with the stanford symposium and hopefully it will lead to publications in refereed journals that can be used here. Tkuvho (talk) 18:25, 6 December 2010 (UTC)

I see that the C. Hewitt paper is on its fifty-third version (!), but this does not make it "published", contrary to what you claim above. Tkuvho (talk) 18:28, 6 December 2010 (UTC)

Of course, it's published, and by a reputable publisher! Each of the published versions is immutable and we have the advantage that we can see the evolution of development in a place that is freely accessible as opposed to having to try to to trace development through references in journals and proceedings that are not freely accessible. Would you prefer that previous versions not necessarily be accessible as on Google Knol? 67.169.144.115 (talk) 19:34, 6 December 2010 (UTC)

Arxiv is not a publisher, but a preprint repository with pretty much zero content control. It is not subject to standard peer review, and as such it does not count as a reliable source according to Wikipedia standards.—Emil J. 19:40, 6 December 2010 (UTC)

It is more than zero: submissions can be removed from arXiv for being off-topic or for being substantially below scientific writing standards (e.g. having no references). And many papers on arXiv are also peer-reviewed in other venues. That said, I agree that being on arXiv by itself is not enough to qualify a paper as being reliably published, and that WP:SPS is the appropriate standard to use when judging whether such papers can still be used as sources. —David Eppstein (talk) 19:46, 6 December 2010 (UTC)

The article's critics have considerable science on their side whereas Wikipedia adminstrators have Wikilaw. Hewitt has published an excerpt from his ArXiv article on Knol as Incompleteness Theorems: The logical necessity of inconsistency. The account of imcompleteness there is quite different from the one in the Wikipedia article Incompleteness Theorems. The longer that Wikipedia censors the work, the worse for its reputation. ~~ —Preceding unsigned comment added by 171.66.107.146 (talk) 00:00, 9 December 2010 (UTC)

Maybe this will be the undoing of wikipedia, but those are the rules here. The Knol site seems like a blog page which does not meet the criteria for inclusion here. Personally I think that barring this kind of input is what gives wikipedia its vitality. Tkuvho (talk) 03:51, 9 December 2010 (UTC)

I doubt that this particular censorship will have much effect on Wikipedia. However, this kind of censorship discourages contributions to Wikipedia and causes users to have look eleswhere for information. Google is probably the largest beneficiary of the censorship.13.7.64.111 (talk) 01:43, 10 December 2010 (UTC)

Perhaps, but wikipedia is not a blog page, and most serious contributors here realize this. Tkuvho (talk) 03:47, 10 December 2010 (UTC)

No one is under the illusion that Wikipedia is a blog. However, Wikipedia is inconsistent on the issue of allowing links to ArXiv publications. Sometimes, as in the case of Perelman they are allowed. In other cases, such as this one, they have been banned. 67.169.144.115 (talk) 19:43, 10 December 2010 (UTC)

I'll support liking to Hewitt's arxiv paper, like Perelman's, as soon as Hewitt is awarded the Fields Medal for that paper, like Perelman was. As for Wikipedia's inconsistency, didn't Hewitt prove that it's logically necessary?

Wikipedia often includes references event to blogs, e.g., Arsenic in nucleic acids. So the removal of the reference to Hewitt's ArXiv article in favor of an inferior reference looks like personal animosity against Hewitt on the part of Wikipedia. 63.249.116.52 (talk) 21:40, 19 December 2010 (UTC)

Wikipedia articles often contain all kinds of inappropriate things, that's the nature of the beast, but that's no reason that this article should. Paul August ☎ 22:11, 19 December 2010 (UTC)

The contrast is quite amazing between the Wikipedia article Incompleteness theorems and the Hewitt article Incompleteness Theorems: the logical necessity of inconistency, which is a popularization of Common sense for concurrency and inconsistency robustness using Direct Logic(TM) and the Actor Model arXiv:0812.4852. It will be interesting to see how this controversy develops. 99.29.247.230 (talk) 21:39, 23 December 2010 (UTC)

Is there a Guinness world record for the largest number of versions for an arXiv post? I hereby propose Hewitt as a candidate. Someone should start Carl Hewitt in Guinness book of world records. Tkuvho (talk) 05:42, 24 December 2010 (UTC)

Many of the revisions concerned keeping the article consistent with Hewitt's other publications on ArXiv. Others made the article more readable and added motivation.

Also I wonder what the record is for the number of revisions to a Wikipedia article :-) 99.29.247.230 (talk) 20:46, 24 December 2010 (UTC)

What I find most puzzling about this whole tempest is that Hewitt's article has a simple rigorous proof of incompleteness whereas the Wikipedia article Proof sketch is complicated and hand-waving. What is it about Hewitt that has so ticked off User:Tkuvho? 64.134.223.51 (talk) 21:40, 24 December 2010 (UTC)

More accurately, my reaction could be described as "amuzed". I am not competent to comment on the merits of C.H.'s argument. My only point is that his admirers don't seem to have internalized yet that until C.H. publishes his work in refereed venues, coverage in wiki is inappropriate by wiki's rules, which apply to everyone including Perelman. Tkuvho (talk) 19:33, 25 December 2010 (UTC)

At a Stanford logic colloquium last summer, the results in Hewitt's article were presented to some of the most prestigious logicians in the world. There is a video available at Wittgenstein versus Gödel on the Foundations of Logic. This is a much more stringent test than simply appearing in a "refereed" rag.64.134.228.32 (talk) 19:13, 26 December 2010 (UTC)

At the colloquium, Solomon Feferman, Jeremy Forth, Grigori Mints, and Charles Petrie participated in the discussion. 67.169.144.115 (talk) 22:33, 1 January 2011 (UTC)

Well, actually, the proof in Wikipedia is approximately a conversion of Gödel's original proof into modern notation, while Hewitt's proof is a new(?) proof in his notation, which is an extention of modern notation. New notation can often make proofs easier. But it's not clear that Hewitt's theory is a conservative extension of modern mathematical logic; it could be something completely different.

We can argue about simplicity; but Hewitt's proof requires a proof within the system that reification and abstraction are inverse functions, a non-trivial assertion. — Arthur Rubin (talk) 17:46, 25 December 2010 (UTC)

It looks like the proof in Wikipedia says for every sentence s that s=⌊⌈s⌉_Gödel⌋_Gödel where ⌈s⌉_Gödel is the Gödel number of s and ⌊n⌋_Gödel is the sentence with Gödel number n. (This is called "Roundtripping" in Hewitt's article.) Otherwise, it looks like the incompleteness proof in Hewitt's article goes through just fine for the theory Peano+Roundtripping, which is what Hewitt calles Peano Arithmetic when Roundtripping is added. 19:33, 26 December 2010 (UTC) —Preceding unsigned comment added by 64.134.228.32 (talk)

Goedel's incompleteness theorem assumes as a hypothesis that it is given a consistent first-order theory with some additional properties. Because Hewitt's system is not consistent nor a theory in first-order logic, Hewitt's system is outside the scope of Goedel's theorem. So the theorem that Hewitt proves about his system is analogous to Goedel's theorem, certainly, but it isn't the same theorem. In particular, the sentences that Hewitt constructs on his knol page have the ⌊.⌋ and ⌈.⌉ symbols in them, so Hewitt's proof does not actually construct a sentence in the language of first-order Peano arithmetic, and thus does not prove Goedel's incompleteness theorem for first-order Peano arithmetic. — Carl (CBM · talk) 22:24, 26 December 2010 (UTC)

Since ⌊.⌋_Gödel and ⌈.⌉_Gödel are part of first-order arithemtic, the Hewitt article proved incompleteness of first-order arithmetic. However, the Hewitt proof used roundtripping, which is also used by the proof in the Wikipedia article. So Gödel fundamentally extended the theory of arithmetic by introducing the roundtripping principle. It takes Peano+Roundtripping to prove incompleteness. But Hewitt showed that Peano+Roundtripping also proves inconsistency. It seems quite evident that Peano arithmetic is consistent. It is not obvious that Peano+Roundtripping is consistent. 63.249.108.250 (talk) 22:47, 26 December 2010 (UTC)

(1) Tarski's indefinability theorem shows that it is not possible for a consistent-first order theory to have a ⌊.⌋ operation that allows one to assert in the object theory that the sentence encoded by a given number is true. The proof sketch in this article does not make use of these things, as it applies to consistent theories. (2) Hewitt has proved that his system is not consistent. This is what he means when he says "The Logical Necessity of Inconsistency". — Carl (CBM · talk) 23:47, 26 December 2010 (UTC)

The Wikipedia article proof of incompleteness does not have a formal proof unlike the Hewitt article that does have a formal proof. In what theory does the Wikipedia article purport to prove incompleteness?? 63.249.108.250 (talk) 22:17, 26 December 2010 (UTC)

This article does not prove the incompleteness theorem: it provides a proof sketch. The proof sketched here would apply to any first-order, consistent, effective theory that interprets Robinson arithmetic. — Carl (CBM · talk) 22:24, 26 December 2010 (UTC)

The problem is that the proof is not actually carried out in first-order arithmetic. 63.249.108.250 (talk) 22:52, 26 December 2010 (UTC)

The primary difficulties in presenting a rigorous proof here are the same as in a textbook: it takes a lot of work to verify all the details of the Goedel numbering. But this cannot be avoided if one wants to have a theorem that applies to ordinary first-order Peano arithmetic. Since so many textbooks have the full details, it's fine for this article to have a proof sketch. — Carl (CBM · talk) 23:50, 26 December 2010 (UTC)

As CBM points out, the proof sketch could be converted to a proof in first-order arithmetic. On the other hand, Hewitt's proof, as is his theory, is in an inconsistent variant of first order arithmetic plus reification and abstraction. The reification and abstraction operators cannot be proved to exist within first order arithmetic. The coding can be expressed, but the actual truth function can only be proved correct for a finite number of formulae. That would make Hewitt's proof simpler, but of a different theorem in a different logical system. (We can argue the merits of Hewitt's incompleteness theorems in a different forum.) — Arthur Rubin (talk) 18:10, 27 December 2010 (UTC)

In his article in the section Gödel versus Wittgenstein, Hewitt speaks only about provability and not about truth and consequently there is no "truth function." The problem is that incompleteness cannot be proved within Peano arithmetic because roundtripping is needed for the proof. But Hewitt proved that the theory Peano+Rountripping is inconsistent. 99.29.247.230 (talk) 19:18, 27 December 2010 (UTC)

That might make sense. It has nothing to do with the Gödel incompleteness theorems (which in turn, have nothing to do with "roundtripping"), but it might make sense.

Actually, thinking about it the problem with your interpretation is that the 1st incompleteness theorem requires the truth of the "Gödel formula" of a number being provable being determined from within the system, which requires ω-consistency. Hewitt's concept of "roundtripping" is a separate meta-axiom. — Arthur Rubin (talk) 05:49, 29 December 2010 (UTC)

I think that I get something of your drift. However, I am an having trouble understanding you statement:

truth of the "Gödel formula" of a number being provable being determined from within the system

Is this the same as ⊢s if and only if ⊢⌊ ⌈s⌉ ⌋ ? Happy New Year! 67.169.144.115 (talk) 22:24, 1 January 2011 (UTC)

Query about First Incompleteness Theorem

The appropriate domain here is the domain of ordinary mathematics SN (the set superstructure of the natural numbers). Since ordinary mathematics does not impose any funny restrictions on the induction axiom, it turns out that all the Tarski models of ordinary mathematics are isomorphic to SN. It seems quite likely that SN is consistent. However, in order to prove the incompleteness theorem in SN, Gödel introduced roundtripping. But the theory SN+Roundtripping is inconsistent (see the Google Knol Incompleteness Theorems). Inconsistency is OK for inconsistency robust logic but it is a disaster for classical logic.98.210.242.39 (talk) 20:16, 20 January 2011 (UTC)

More nonsense about roundtripping. As a regular contributor here, I'm not going to move it to /Arguments, but I think it should be moved. — Arthur Rubin (talk) 07:52, 21 January 2011 (UTC)

How do you know that roundtripping is "nonsense"? Computer scientists seem to have a very good technical grasp of the published literature on the incompleteness theorem. But classical logicians who edit here don't seem to have a similar grasp of computer science and where it is going. Calling the computer science "nonsense" is not going to make it go away.98.210.242.39 (talk) 17:59, 21 January 2011 (UTC)

I don't know that "roundtripping" is "nonsense". I know that what Gödel did, and the other standard proofs of the incompleteness theorem, are not roundtripping. The statement "Gödel introduced roundtripping" is nonsense. — Arthur Rubin (talk) 18:28, 21 January 2011 (UTC)

Computer scientists have very rigorous criteria and by their criteria Gödel's proof used roundtripping although Gödel did not publish a formal proof (see arXiv:0812.4852). All rigorous proofs have used roundtripping, e.g, the ones in the Google Knol mentioned above.98.210.242.39 (talk) 18:46, 21 January 2011 (UTC)

Dude, speak for yourself. Rigorous standards ≠ license to make stuff up out of thin air. —David Eppstein (talk) 18:52, 21 January 2011 (UTC)

Given that this is not his field of specialization, it is interesting that Professor Eppstein would want to go so far. Following the previous conventional wisdom often works. But sometimes it then goes spectacularly wrong. It could be possible for the classical logicians to salvage something from this. But they will have to be very precise about exactly which theory is being used to prove the incompleteness theorem. —Preceding unsigned comment added by 171.66.85.193 (talk) 01:19, 22 January 2011 (UTC)

It is known that the second incompleteness theorem is provable in very weak, consistent theories such as primitive recursive arithmetic; this is discussed in detail by Smorynski in his article in the Handbook of Mathematical Logic. Presumably that is precise enough. — Carl (CBM · talk) 01:23, 22 January 2011 (UTC)

I think that the dispute is about formalizing roundtripping. There is no doubt that some of the proof of incompleteness can be carried out in primitive recursive arithmetic. The question is whether the whole proof can be carried out in that theory.171.66.85.193 (talk) 01:30, 22 January 2011 (UTC)

Yes, it all can. This is explicitly stated by Smorynski in his article, Corollary 2.2.4 and the discussion on page 840. It's not as if the question of what theory is needed to prove the theorem has never occurred to anyone; it's well known and documented in the standard references. — Carl (CBM · talk) 01:47, 22 January 2011 (UTC)

Unfortunately, many classical logicians have an incredible blindness concerning what it takes to formally prove the incompleteness theorem. Gödel knew that in order to avoid inconsistency that the proof would have to be carried out in a "metatheory" that wasn't Principia Mathematica. Later he further retreated to carrying out part of the proof in primitive recursive arithmetic but didn't have anything further to say about the mysterious "metatheory."171.66.104.156 (talk) 01:56, 22 January 2011 (UTC)

There's that fantasy version of history again. --Trovatore (talk) 01:58, 22 January 2011 (UTC)

Regardless, I answered your question about what it takes to prove the second incompleteness theorem: it can be formally proved in primitive recursive arithmetic, period. Your response is just bluster. I'd recommend studying the actual incompleteness theorems, using Smorynski's article or some other reliable reference, before you take Hewitt's claims too seriously. I'm sure they have something in the library at Stanford, along with faculty who could explain the matter in person if you asked them. — Carl (CBM · talk) 02:05, 22 January 2011 (UTC)

You need to visit Stanford for a reality check. It seems that the only active professors that believe the User:CBM account are a couple of elderly logicians in Philosophy Department. Everyone else sides with Computer Science. See the video of the Stanford colloquium at How to Program the Many Cores for Inconsistency Robustness. In fact, there will be a Stanford symposium this summer that includes inconsistency robust logic in addition to covering how scientists address inconsistency more generally. See Inconsistency Robustness 2011 at Stanford.171.66.107.151 (talk) 05:00, 22 January 2011 (UTC)

The idea that there are "sides" is somewhat arealistic. There is no debate in the logic community about the provability of the incompleteness theorems. As is typical in mathematics, it's not an issue of "belief", since the result are proved completely rigorously and can be verified by anyone who takes the time to do so. I'd recommend starting with Smorynski's article, or maybe a graduate textbook, and working through it from the start. — Carl (CBM · talk) 14:35, 22 January 2011 (UTC)

Identification of Godel-statements as falsifiable-statements ?

              This may seem a bizarre suggestion, it occurred whilst puzzling over the status that 
               should be accorded 'Godel-statements'; by which is meant  the unprovable 
               statements, of  Kurt Godel's famous Incompleteness Theorem.           
              Interpreted as:   
                             "Every axiomatic system is either complete or consistent, but 
                             not both”. 
               Which implies that every consistent axiomatic system is incomplete; 
               which implies that Godel-statements must exist in every consistent axiomatic 
               system.

               Where by 'complete' axiomatic system is intended ,one in which:
              'all statements constructable within such a system, are provably true or false';  
               and 
               where by 'consistent' axiomatic system  is intended one, in which :
               'no two  provable statements, can be found to conflict' ; 
                                       
            Now another theorem of Godel, his Consistency Theorem established that consistency  
            itself was not provable; which implies that the statement :
            "This axiom set is consistent”  along with it's corollary ,
            “This axiom set is incomplete “
           are necessarily Godel-statements in any axiom system, which is not formally  
            inconsistent; ie. containing conflicting axioms.        

 My difficulty arises when trying to decide what exactly a Godel-statement,
that is an 'unprovable statement';  'is'..
Statements which seem true, but can't be proved , superficially  resemble the axioms themselves. 

In that axioms are statements which are necessarily true, since they define the particular axiom system, but necessarily can't be proved.; since if they could be proved using the other axioms; they would be unnecessary.

But if Godel-statements are considered to be additional axioms, and formally added to the set, one starts an escalating vicious cycle; because this new enhanced axiom set , will have it's own additional Godel-statements. etc.

If instead of considering some statements 'true and proved' and others merely 'true'; we consider all 'true' statements as falsifiable by: the 'mathematical observed facts' of the axiom system; we can then distinguish between the 'proved statements', that is the tautologies we call theorems, which are necessarily consistent with the 'mathematical observed facts' of the axiom system; and those which have merely been found to be consistent, to date. After all if we could be certain they would remain so, they would be 'provable' theorems.

To repeat in different words for clarity;

because this is a drastic and radical departure from the traditional notion of mathematical truth.

It is proposed that all theorems are considered as statements asserting explicitly or implicitly; 

one or more 'mathematical observable facts' of the relevant axiom systems. Conflict with the actual 'mathematical observable facts' of the axiom system, would make the statement false. We can then distinguish between the 'proved statements', that is the tautologies, we call theorems, which are necessarily consistent with the 'mathematical observed facts' of the axiom system; and those which have merely been found to be consistent, to date.

Now if we treat Godel-statements as falsifiable-statements, in this extended sense of falsifiability, that is, capable of being falsified by the 'mathematical observed facts' of the particular axiom system; then we have a place for Godel-statements, without having to add them as axioms , thus avoiding the above vicious cycle. . Corollary to Query (2) above:

                            If Goedel-statements can be considered to be falsifiable-statements in 
                             this extended mathematical sense,of 'unproved statements,
                             thus far found consistent with the facts of the axiom system , 
                             but possibly false by comparison with facts yet to be considered.'

Are Godel-statements , which are consistent with only a sub-set of the facts of the axiom system (a) possible ?; (b) necessary ?

Rhnmcl (talk) 02:16, 26 August 2011 (UTC)

Extra for "Note and for Pedagogics of the Article"

I also like to note that Gödel mentions "prime number" 5, five, times through his 23 pages paper, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I." — Preceding unsigned comment added by 109.189.88.76 (talk) 08:18, 6 December 2012 (UTC)