Talk:Gödel's incompleteness theorems

From Wikipedia, the free encyclopedia

You have new messages (last change).

This is the talk page for discussing changes to the Gödel's incompleteness theorems ARTICLE. Please place discussions on the underlying mathematical issues on the Arguments page. Non-editorial comments on this talk page may be removed by other editors.

Please sign your comments using four tildes (~~~~). Place comments that start a new topic at the bottom of the page and give them == A Descriptive Header ==. If you're new to Wikipedia, please see Welcome to Wikipedia and frequently asked questions.
WikiProject Mathematics
This article is within the scope of WikiProject Mathematics.
Mathematics grading: B+ Class High Importance  Field: Foundations, logic, and set theory

Needs proper introduction, and consider breaking up lengthy sections. Tompw 18:58, 7 October 2006 (UTC)
A Wikipedian removed Gödel's incompleteness theorems from the good article list. There are suggestions below for improving areas to satisfy the good article criteria. Once the objections are addressed, renominate the article as a good article. If you disagree with the objections, you can seek a review.
Removal date: 8 May 2006


Contents

[edit] Re: Gödel's Incompleteness Theorems - A Brief Introduction

Hey, User:Paul_August, I am curious what fault you found with the article at http://www.mind-crafts.com/godels_incompleteness_theorems.html that made you remove the link to it I put in External Links. I have to confess that IMHO it's the best non-technical introduction to Gödel's theorems on the Internet. 66.217.176.211 16:55, 16 November 2006 (UTC)

Paul, actually, I took a brief look and (at least at that level of scrutiny) it does look pretty good. We don't want to encourage link farming but this one really might be worthwhile. --Trovatore 03:52, 27 November 2006 (UTC)
OK, I restored the link - since no arguments were given against it. Will be happy to listen and discuss if anybody comes up with cogent args. 66.217.179.50 22:45, 3 December 2006 (UTC)

[edit] Removal of Godel's statement of theorem

I removed Godel's original statement of the theorem, but it's been reverted back. Godel's statement:

To every ω-consistent recursive class κ of formulae there correspond recursive class signs r, such that neither v Gen r nor Neg(v Gen r) belongs to Flg(κ) (where v is the free variable of r).

is only meaningful if you explain Godel's notation (e.g., class signs, Gen, Neg, and Flg), which we don't really need to do in this article. Perhaps for historical interest, we can have all this in its own section of the article, but it's not useful where it stands now and will just mystify most people. If there are no objections, I'll remove it again soon. -SpuriousQ 09:55, 27 November 2006 (UTC)

Obviously, I disagree or I would not have reverted you. You took out a section header which is inappropriate. And the formal statement of the theorem may be of interest to some people, such as those who have read the paper. If you think that it is too advanced a topic, the appropriate course is to move it to the end of the article and add more explanatory material. JRSpriggs 10:29, 27 November 2006 (UTC)
Thanks for the explanation, JRSpriggs. The section header was removed because it was introducing the deleted content and didn't make sense without it. As for the content itself, I don't think it's a matter of the topic being "too advanced"; it's that it's unreasonable for us to expect our audience to have read Godel's paper (with the German abbreviations intact, at that). As stated right now, I feel it does more harm than good, especially given the recent remarks about the article's accessibility. Like you suggest, a possible solution would be to move it to the end with more explanation, which I would be happy with and may attempt when I get a chance. -SpuriousQ 16:12, 27 November 2006 (UTC)
With respect to JR, I tend to agree with Spurious here. Gödel's proof was brilliant; his notation, like almost all version-1.0 notation, was less than ideal from the point of view of long-after-the-fact exposition. And even if the notation were nicer, we still should not want to get into the details of a specific coding scheme early in the article, as it's kind of beside the point. --Trovatore 16:27, 27 November 2006 (UTC)
Word. Ruakh 21:26, 27 November 2006 (UTC)

[edit] The bizarre proof sketch

How can you say that P(x) can be proved if x is the Gödel number of a provable statement explicitly explaining in the previous paragraph that the Gödel numbers encode single-parameter formulas, which are not statements and, therefore, cannot be proved or disproved? In other words, the concept of "provability" is inappropriate to F when we rewrite P(x) as P(G(F)). --Javalenok 02:17, 6 January 2007 (UTC)

A given Gödel number might encode a single-parameter formula, or any other formula, or a statement. I've made an edit that I think might clarify a bit; does it address the problem you see? If not, can you be more specific about what text you see the problem in? Thanks in advance! —RuakhTALK 06:49, 6 January 2007 (UTC)
At first, reading this article and the Gödel number, I have got the affirmation that a given Gödel number encodes a formula. The mapping one-to-one at that. Therefore, it seems that you are wrong when telling that a number (a means one in english) encodes a form or another form. It encodes only one form but not another. Secondly, since x is a natural number, a form generates an infinite number of statements. That is, infinitely many statements F(x) conform to a form F. Taking into account that the notion of proof does not apply to the forms, we are precluded from defining the decider P(G(F)). The decider must be provided with a statement; i.e., both the number of F and x. --Javalenok 13:15, 6 January 2007 (UTC)
Sorry, you misunderstood me. I didn't mean that a Gödel number might simultaneously encode all of those things; I meant that a given Gödel number could be a Gödel number that encodes a single-parameter formula, or a Gödel number that encodes a formula of some other type, or a Gödel number that encodes a statement.
Also, the article does not use the term decider and does not make reference to P(G(F)), so I don't know what you're referring to. Can you quote a specific sentence from the article so I can see what you're objecting to?
—RuakhTALK 19:41, 6 January 2007 (UTC)
To Javalenok: Please do not remove the messages of other editors (unless they are vandalism, libel, obscenity, etc.). Also do not remove your own prior messages if they provide context to another user's messages. If you like, you may strike-out the parts of your messages with which you no longer agree using <s> and </s> (having this effect and ). Consequently, I have restored the messages by Ruakh and yours which provide context. JRSpriggs 07:35, 9 January 2007 (UTC)

Sorry my fussiness, I have overlooked in the beginning that statements can also have Gödel numbers. Before this discussion will be deleted, please explain why do you substitute the Godel number x by formula F(G(F)) in P(x)? The formula is not a number. The grammatically correct statement would be P(G(F(G(F)))). Furthermore, the substitution of variable x in P('x') by the number of statement p turns the form into statement and its number changes accordingly. But the resulting statement is p, so its number 1)must be fixed; and 2) known in advance!!! Where do we get the number from? --Javalenok 20:33, 11 January 2007 (UTC)

Also, I suggest to incorporate the the '#' notation for 'G()' as in [1] so that P(#F(#F)) looks better than P(G(F(G(F)))). --Javalenok 16:10, 8 January 2007 (UTC)

In addition, let me note that the formalism p = SU(#SU) corresponds to the sentence 'p is equal to "this statement is not provable"' rather than the 'desired' "p cannot be proved". Peahaps, the difference between two sentences of lair paradox does not really matter. Nevertheless, the neccessety for the redundant 'p' confuses me. --Javalenok 23:02, 8 January 2007 (UTC)

[edit] What is the need for self-unprovable formulas?

Let me give a shorter sketch. I see no need to define SU. The statement p equivalent to "p cannot be proven" can be easily formalized as p = ~P(p). Now, if p is provable true then the argument p would be not provable (a contradiction). Alternatively, if p is false (that is, not provable true) then P(p) would be true meaning the argument p is provable true (again contradiction). --Javalenok 13:44, 10 January 2007 (UTC)

You said "...if p is false (that is, not provable true)...". Falsity is the same as not BEING true. That is different from not PROVABLE. This distinction is essential to understanding Gödel's theorem. There is no inconsistency in the existence of a sentence p which is simultaneously true and not provable. Gödel never proved p, i.e. that p cannot be proved. What he proved was ω-con→p, i.e. that IF arithmetic is ω-consistent, THEN p cannot be proved. JRSpriggs 06:39, 11 January 2007 (UTC)
OK, may be I should tell: IF p = false THEN P(p) = true HENCE p is provable true HENCE contradiction (p and ~p) = true. The purpose of the incompleteness theorem is to show that a consistent theory cannot be complete. I'm showing that it is possible to do without introducing the self-unprovable forms. Any objections? --Javalenok 08:47, 11 January 2007 (UTC)
Your first step, going from Neg(p) to P(p), is changing context which is logically invalid. You are going from an arithmetic statement to a meta-arithmetic statement. Although Gödel showed that some meta-arithmetic statements can be pushed down into arithmetic, it does NOT go the other way (as you would have it). Also you say "I'm showing that it is possible to do without introducing the self-unprovable forms.". I do not see what you are getting at here. You are still using p in your argument, and p is the "self-unprovable form" to which you object, is it not? JRSpriggs 08:36, 12 January 2007 (UTC)
Look, SU(#F) is defined as ~P(#F(#F)), so SU(#SU) = ~P(#SU(#SU)). Given SU(#SU) = p, we can rewrite the equality as p = ~P(#p). This equality states self-unprovability explicitly and, furthermore, eliminates the needles self-unprovable form SU(#F). The Neg(p) is ~~P(#p). But you deny the logical conclusion ~~P(#p) => P(#p). Instead, you prefer to go to english language. But stating that some self-unprovable can be proved is an outright nonsense. The [2] dares to state: "Suppose that ~(~P(p)) is a theorem. Hence P(p) is a theorem." --Javalenok 23:32, 13 January 2007 (UTC)
You have completely misunderstood my last message. There is no meaningful difference between "P(p)" and "~~P(p)"; and I did not say otherwise. The vital distinction which you are ignoring is between statements in English about arithmetic and statements in the language of arithmetic which might be regarded as (in some sense) encoding the English statements. Although the encoding is chosen with the intention of making them equivalent, they are not (known to be) PROVABLY equivalent either from the axioms of arithmetic or from meta-arithmetic considerations. JRSpriggs 09:24, 17 January 2007 (UTC)

[edit] How About

We split out the philosophical ruminations into a separate article and make *this* article as clear and concise a description of the theorem(s) and their context in mathematics and metamathematics (no easy feat, I'm sure). If nothing else this article is becoming very long and I think it'd benefit.

That said, I confess I'm not sure how this would be done -- do we need to have a discussion/vote? should one be bold and just start the other article? Thoughts? Zero sharp 21:31, 10 January 2007 (UTC)

Let's talk about it first. The ruminations here are quite short, which seems like the ideal situation to me. Are you saying that you would like to expand them?
If you have time and would like to improve this article, you might start by going through and changing the tone so that it is more encyclopedic, without the "we" statements. CMummert · talk 12:22, 11 January 2007 (UTC)
Well, the Minds and machines section may be better fit in its own article, or merged over to Mechanism (philosophy). Actually, there are a bunch of disparate treatments of this scattered over Wikipedia, e.g., here, in Mechanism (philosophy)#Anthropic_mechanism, John Lucas (philosopher), and Minds, Machines and Gödel. We should pick a primary place for the content to go and the rest can link to it. -SpuriousQ 12:27, 12 January 2007 (UTC)
I am all in favor of reducing redundancy. I am fearful about a separate article because I am not a philosopher. I am afraid it might grow into a giant mess of speculation, OR, and non-notable opinions, and it would be hard to fix. But I wouldn't revert the move if it happened. You might leave a one-paragraph summary here, and point to the main article with the {{main}} template. CMummert · talk 14:23, 12 January 2007 (UTC)

I think we need to distinguish between two sorts of philosophical issue. At least something ought to be said in this article about implications for philosopy of mathematics -- particularly, the difficulties that Gödel's results have presented for the formalist and logicist programs. That's part of the historical background in which the results were announced.

The stuff about philosophy of mind, on the other hand, should not be here in my opinion, with the exception of a link somewhere and a very brief summary. This is a mathematics article. --Trovatore 20:59, 12 January 2007 (UTC)

OK, I merged the "Minds and Machines" section over to Mechanism (philosophy). -SpuriousQ 01:14, 17 January 2007 (UTC)

[edit] Gödel sentence is an objection to AI. Is it true?

Moved to Talk:Gödel's incompleteness theorems/Arguments.

This question is not an "argument over the validity of the incompeteness theorem". Why was it moved there? --Javalenok 20:36, 11 January 2007 (UTC)
It's not directly related to improving the article. --Trovatore 21:24, 11 January 2007 (UTC)


[edit] Is the incompleteness theorem complete???

Moved to Talk:Gödel's incompleteness theorems/Arguments.

[edit] "Publication" cat

There's been a bit of reverting going on over the category Category:Important publication in mathematics. My take: first of all, the cat itself should be renamed (categories of this sort take plural names). Second, no, this article doesn't belong in that category, though a category an article named after Gödel's famous paper, "On Formally Undecidable Propositions...", would belong in the category. This article is not (primarily) about that paper, and therefore doesn't. --Trovatore 20:43, 17 January 2007 (UTC)

I strongly agree that the category should be pluralized, and weakly agree that it isn't suitable here. —RuakhTALK 22:44, 17 January 2007 (UTC)

The category tag seems to be added and removed over and over again. I think Trovatore's contention is that this article is about the theorems, not the publication. I agree. How about I create a short article on the actual publication, which is certainly notable because it introduced these theorems. Then that page can get added to the category, and everyone wins. CMummert · talk 18:55, 24 January 2007 (UTC)

Yes, please! And if the article is out of copyright, we can put its full text on Wikisource and both articles can link to it. :-D —RuakhTALK 19:17, 24 January 2007 (UTC)
The article itself was originally published in German in 1931; I have no idea what its copyright status is. The later English translations are almost certainly still under copyright in the United States. CMummert · talk 19:27, 24 January 2007 (UTC)
Done: On Formally Undecidable Propositions of Principia Mathematica and Related Systems. CMummert · talk 02:02, 25 January 2007 (UTC)
Nice work, Carl. I might quibble on the link to the problematic article Gödel numbering, which I think should probably be deleted or redirected somewhere. But it looks very good, and you finished it quickly! --Trovatore 02:51, 25 January 2007 (UTC)
My general philosophy is that a link should be provided if it theoretically helps the linking article. Otherwise, when the destination article is improved, how will anyone know which articles should link to it? I have the same belief about red links. CMummert · talk 03:29, 25 January 2007 (UTC)
Well, that makes sense, if there ought to be an article called "Gödel numbering". Should there? I'm not convinced. A redirect for sure, but an article? And the argument doesn't strike me as being quite as strong when talking about redirects. --Trovatore 03:52, 25 January 2007 (UTC)
The concept of Godel numbering the sentences of a first-order theory deserves some article. When the current article on Godel numbering is fixed, at least "what links here" will be accurate. The person making the redirect, or a bot in some cases, should resolve the link in the original article to bypass the redirect.
My thought about the Godel numbering article is that it should be an article, but it should just give a catalog of the various senses of the phrase, possibly with links to larger articles on each of these senses. CMummert · talk 04:12, 25 January 2007 (UTC)

[edit] Recent anon edits

While I generally feel that anyone wanting to make such extensive revisions to a high-profile article ought to log in, I think the recent spate of edits by 132.181.160.42 have generally been of high quality. However I can't agree with a couple of the changes to the intro. Explaining myself here. The anon wrote:

These theorems show that no consistent formal system can completely describe Peano arithmetic (addition and multiplication over the natural numbers), and that no system capable of representing that arithmetic can prove its own consistency.

This statement is insufficiently precise to be either right or wrong, but it has reasonable readings that are just wrong. Peano arithmetic, for example, is a syntactic rather than semantic construct (as opposed to the structure of the naturals, which is semantic); it's certainly possible for a consistent formal system to completely describe the syntactic manipulations of Peano arithmetic. Moreover there needs to be something said about what sort of formal system (say, that its axioms are computable), otherwise no such conclusion is possible. The anon also says:

The theorems also have extensive implications for philosophy and cognitive science.

A great deal of bad philosophy and cognitive science has been based on the theorems (so say I, a hardcore metaphysical libertarian and substance dualist who likes the conclusion of the Lucas arguments, just not the arguments themselves). In general any claimed philosophical implications outside of mathematics should be viewed with suspicion; it's not ruled out a priori that no such implications can be drawn, but I have never seen one that worked. I think there's a good bit of possibly accurate stuff that's suggested by the theorems, by analogy as it were, and these may even be a reasonable heuristic guide to truth. But the word "implication" is too strong. These are theorems of mathematics, and we should keep the focus firmly there. --Trovatore 07:34, 26 January 2007 (UTC)

I agree that Peano arithmetic is a formal system that adequately formalizes Peano arithmetic. I added a caveat to the lead - the well known decidable formal systems for geometry and the real numbers are simple, but not "trivial". CMummert · talk 13:36, 26 January 2007 (UTC)


[edit] Commercial links

The link to "Askanas, Malgosia, 2006, "Gödel Incompleteness Theorems - A Brief Introduction." A lucid and enjoyable exposition of both theorems in the spirit of Gödel's original proof. "is not a bad site for explaining this theorem--well above the high school student's level though--but its "lucid and enjoyable" presents a value judgement which is not at all consistent with the purpose of the article and Wikipedia. It is a commercial site selling services in math education. It should be retained, in my view, it does a fairly good job of explaining the concepts, but the evaluation needs to be reconsidered. Malangthon 03:31, 27 January 2007 (UTC)

I removed the annotation. You could (and, I would suggest, should) have moved it here along with your comment. In cases where a phrase is clearly not neutral POV, seems to advertise for a commercial service, or both, there is no reason to leave the statement while inquiring about it. CMummert · talk 03:54, 27 January 2007 (UTC)

[edit] is the incompleteness theorem complete?

This section discussed the underlying mathematics issues rather than the article. It has been moved to the arguments page and can be found here. CMummert · talk 02:16, 29 January 2007 (UTC)

[edit] Could we shorten the article.....considerably?

There are previously complaints about this not being accesible to laymen to understand the main points of Godel's Incompletness theorems.

Perhaps majorly shortening the article would help? Just throwing out a suggestion. Fephisto 22:45, 4 March 2007 (UTC)

Shortening it, by itself, will not make it more accessible. Moreover, I would not be in favor of removing material just because it requires a technical background to understand it. Ideally, that material should appear later in the article, with the more understandable material up front, but that's a matter of reorganizing, not shortening.
However it is true that the article is a bit long. It's difficult to maintain focus in articles this long, because people edit in the middle without considering the overall flow. I think the sections on the first and second theorems should be split out to their own separate articles; that would help a bit. That's one of those things I may get around to one day if no one else does it first. --Trovatore 00:59, 5 March 2007 (UTC)

[edit] A non-mathematical analogy?

Is the incompleteness theorem *very roughly* analogous to a logical aporia? An aporia is an irresolvable internal contradiction or logical disjunction in a text, argument, or theory. For example, if a Cretan declares all Cretans to be liars, there is an irresolvable contradition between the subject and the predicate. Another example would be: "Language cannot communicate truth", which, if true, is inherently untrue, and therefore true, and so on to infinity.

I am asking purely out of curiosity and am not suggesting this have any bearing on the article.

Thanks. —The preceding unsigned comment was added by Ulrich kinbote (talk • contribs) 07:58, 5 March 2007 (UTC)

Yes, there's a rough analogy there; that's a good way to put it (except the term I knew for it was "antinomy"; is there a distinction between "aporia" and "antinomy"?). Unfortunately a lot of people try to take it as too strict an analogy, and a small but noticeable percentage of these decide that they've "solved the problem" and rant on about some "subtle error" that they think Gödel made. --Trovatore 08:10, 5 March 2007 (UTC)
The problem is that while these theorems are given press coverage, they are intrinsically very difficult to understand. There is no "royal road", no analogy, no easy way to understand them. The layman will NEVER understand them. Only a person who has spent years studying mathematical logic has any hope of understanding them. However, they do not cause the crisis that some popularizers try to say that they cause. They just show that mathematics is infinitely ramified, i.e. there is always more to learn about it. JRSpriggs 10:34, 5 March 2007 (UTC)
Well, that might be a little overstating the case. An undergrad math major in a one-semester course in math logic should be able to get the basic idea pretty well. He might not bother to work through all the gory details of arithmetization of syntax, but those aren't very important anyway.
As to the "crisis" -- I think it was a crisis for the foundational schools that were fashionable at the time, such as Hilbert-style formalism. I think the theorems were the main cause of the latter-20th-century rehabilitation of realism/Platonism to a position of respect, not because they made the problems of realism any lighter, but because they heaped heavy difficulties on realism's leading competitors (while leaving realism itself more or less untouched). --Trovatore 07:07, 6 March 2007 (UTC)

[edit] Request for untruth

Can I convince people here to remove the word "true" and "truths" from the statements of the incompleteness theorems? There are two reasons for this. One is that these theorems are formal results about formal systems, and have nothing to do with truth except in certain philosophical interpretations. The interpretations should be in their own section, and not be mixed in with the formal statements of the theorems. The other reason is pedagogical. Despite having a pretty strong mathematical background, I was confused for years about the exact nature of Godel's theorems, precisely because I didn't understand what it meant to be "true but unprovable". It took a very long time for me to realize that the theorems are simply about provability of a sentence and its negation, and once I realized that I immediately understood them. In retrospect I feel that I was misled by nearly every description of the theorems into thinking they were more mysterious than they are, and wasted a lot of time in confusion as a result.

I would state the first incompleteness theorem something like this:

Every [formal system meeting certain criteria] contains a statement which either cannot be proven or disproven from the axioms (making the system incomplete) or which can be proven and disproven from the axioms (making the system inconsistent).

where the bracketed portion is either a placeholder for the actual criteria, or else those exact words with the definition occurring out of line. Probably the latter is better.

I think that the phrasing "every system is inconsistent or incomplete" is much clearer than the phrasing "every consistent system is incomplete". The latter suggests that consistency is just another technical requirement like recursive enumerability, which it certainly is not! -- BenRG 17:25, 23 March 2007 (UTC)

I would support a change like that, provided that the important interpretation of Godel sentences as "true but unprovable" is discussed somewhere else. I have thought for a while that this use of "truth" so early in the article is above the level of the intended reader (they will misunderstand what it means), and the footnote is too terse to help them understand the subtlety of the concept. Several other people watch this page, so I have no plans to rush any changes here. CMummert · talk 17:53, 23 March 2007 (UTC)
I'm not really in favor of such a change. Saying that T does not prove GT is precisely the same as saying that GT is true, and that's what we need to get across. It's possible to doubt that GT has a determinate truth value, but then you are also required to doubt that the proposition "T does not prove GT" has a determinate truth value. Or at least it's not obvious how you'll avoid it. --Trovatore 18:40, 23 March 2007 (UTC)
They are not the same, because you cannot say that GT asserts its own unprovability unless you interpret it as a statement about natural numbers. This is not a mere technicality, because it follows from the completeness theorem that if T is provably consistent in some system T', then there exist models of T in T' under which GT does not hold (i.e. the interpretation of ~GT is a theorem of T'). I'm not sure I got that exactly right, but I assure you that there is no way to talk about the truth of GT without making interpretational assumptions that can't be formally justified. -- BenRG 20:19, 23 March 2007 (UTC)
What I said was that if you doubt the existence of a determinate truth value for GT, you also have to doubt it for the proposition "T does not prove GT". The latter statement asserts the nonexistence of a finite string of sentences starting with the axioms following the rules of inference yada yada yada. If "natural number" (sempliciter, not relativized to any model) is problematic, then so is "finite string of sentences". If you don't think so, then please explain your semantics for interpreting "T does not prove GT", and explain why you don't have to relativize *those* semantics to a model. --Trovatore 20:41, 23 March 2007 (UTC)
Natural numbers are not problematic, just not unique. Let's assume Platonism, since presumably non-Platonists will have no objection to my original proposal. Without getting bogged down in issues of philosophy of language and levels of English quotation and whatnot, "T does not prove GT" is a statement about the Platonic realm, saying yada yada yada. But even to a Platonist, GT is not such a statement. T is a formal system by assumption, and so GT is a string of symbols by definition. Unlike real propositions and theorems, the so-called propositions and theorems of a formal system are just strings of symbols, and a Platonist is not obliged to interpret them in any particular way. The only important thing is that the interpretation be consistent, i.e. that all of the axioms and rules of inference be valid under the interpretation. The Platonic version of the result about T' is: "if T is provably consistent then there exists a consistent interpretation of T under which GT is false". The quoted statement is true if the completeness theorem is true, which I think any Platonist would accept.
Different consistent interpretations of T give you different theorems, all of which are true. In one interpretation GT, though not a theorem of T, happens to encode a true statement about natural numbers that's equivalent to an assertion of GT's unprovability in T. In other interpretations GT might encode other true statements. In at least one interpretation GT encodes a false statement, but ~GT, which is also not a theorem of T, encodes a true statement.
The point is that GT isn't a statement about natural numbers, and never was. The only reason people talk about natural numbers in the context of Gödel's proof is that it's a convenient informal way of describing the Gödelization process. All that's really necessary for the proof is a certain formal structure within the system, which can be provided by natural numbers but also by other things that aren't the same as natural numbers. They all suffice to construct the Gödelization of the system, but they differ in whether it's a true-but-unprovable statement or a false-but-undisprovable statement. -- BenRG 22:10, 23 March 2007 (UTC)
Let's stick to the naturals, please; it'll save us a lot of confusion. Sure, the objects of discourse of T may not literally be natural numbers (e.g., they might be sets, if T is for example ZFC). But the relevant objects of discourse of T are the ones that play the role of the natural numbers in the assumed relative interpretation of PA into T. These are the only ones for which we need provide an interpretation in order to interpret GT. So they might as well be the natural numbers.
Yes, if T is consistent then there is a model of T in which GT is false. But that model will (necessarily) have nonstandard natural numbers. Interpreted in the standard natural numbers (which are unique, up to a unique isomorphism) GT is true. Again, this is no more problematic than the claim that the statment "T does not prove GT" is true. --Trovatore 22:28, 23 March 2007 (UTC)
I disagree that sticking to the naturals saves confusion; I think it creates confusion. As I said before, it certainly did for me. Despite your use of "again", this is the first time you've said that GT interpreted in a particular way is true, rather than implying that GT itself is true. Personally I interpret the (first) incompleteness theorem in a completely different way. In light of the completeness theorem, it seems clear that it's not about the inability of axiomatic systems to capture truth. They can prove exactly what they ought to be able to prove (everything that's true in all models). What it's really about is the inability of axiomatic systems to fix the objects of discourse. To me this is a much more interesting result. It's a reasonable interpretation of what Gödel actually proved, but not a reasonable interpretation of the pre-interpreted version that implies that GT is really true. Of course I'm not saying that this objects-of-discourse thing should be in the theorem statement; it should be in a later section, after a theorem statement accurate enough to accommodate all interpretations.
If this doesn't change your mind then we may be at an impasse. I hope a few other people will weigh in on this. -- BenRG 14:28, 24 March 2007 (UTC)
You don't actually need the incompleteness theorems to show that (first-order) axiomatic systems can't "fix the objects of discourse". Löwenheim–Skolem is sufficient for that (and more directly on-point).
But it does seem that we're not arguing about what I thought we were; it may be more a difference of terminology. The way I think of it, GT, taken literally, is directly a statement about the natural numbers. It's written in the language of arithmetic. If T is not in the language of arithmetic, then the sentence that T literally fails to prove or disprove is not GT itself, but what we might call Translate(GT), where the Translate() function is the thing assumed to exist by the hypothesis that says PA is relatively interpretable in T. What GT asserts is not "T cannot prove me" but rather "T cannot prove my translation". Then I ordinarily suppress mention of translations from casual descriptions, because they really are a technical detail, and speak of T proving or not proving sentences of arithmetic, when literally speaking I really mean proving or not proving their translations.
Using this terminology, where GT is directly and literally a statement about the naturals, do you agree that if T is consistent, then GT is true? --Trovatore 18:15, 24 March 2007 (UTC)
There is a second translation: from the statement GT, which is just some Pi^0_1 sentence, to a statement at the meta level about provability. We recognize, at the meta level, that any actual proof could be coded as a standard natural number. It is because of this second translation that I think it would be worthwhile to have a whole paragraph in the article rather than just a footnote. This translation is already lightly covered one or two places, including the proof, but not as explicitly as it could be. CMummert · talk 19:24, 24 March 2007 (UTC)
Carl, of course you're right about this other level of translation, but it doesn't seem to be in dispute at the moment, especially in relation to the use of the word "true". I seem to have understood wrongly, at first, what BenRG's actual complaint was; it doesn't seem to be about theories of truth, but more about whether the Gödel sentence should be thought of as arithmetical. (For some reason BenRG didn't complain about the word "arithmetical" in the statement he was referring to.) Ben, do you see where I'm coming from on that now, and do you agree that the arithmetical version of GT is properly described as "true" if T is consistent? --Trovatore 01:52, 25 March 2007 (UTC)
Retrieved from "http://en.wikipedia.org../../../g/%C3%B6/d/Talk%7EG%C3%B6del%27s_incompleteness_theorems_d448.html"