Talk:Gödel's incompleteness theorems/Archive 4

Archive 1

Archive 2

Archive 3

Archive 4

Archive 5

Archive 6

→

Archive 10

complete and consistent

Double check the following sentence:

• Furthermore if the system can prove that it is consistent, then it is inconsistent.

Shouldn't that be

• Furthermore if the system can prove that it is complete, then it is inconsistent. —Preceding unsigned comment added by 131.111.16.20 (talk) 14:01, 13 December 2007 (UTC)

You are right that if the system proved itself complete, it would be inconsistent. Goedel's second incompleteness theorem establishes that a particular sentence expressing the consistency of the theory cannot be proven in the theory itself, if the theory is consistent and meets the other hypotheses of the incompleteness theorem. That is what the first bullet above is referring to. — Carl (CBM · talk) 14:44, 13 December 2007 (UTC)

Hmm? An inconsistent theory is "complete" by most definitions (not only does it prove every sentence or its negation; it proves every sentence and its negation), and it's certainly possible for a consistent theory to prove itself inconsistent. So for example PA+¬Con(PA) is consistent, but proves that it's inconsistent, and therefore complete. --Trovatore (talk) 18:11, 13 December 2007 (UTC)

My comment that a theory that proves itself complete is inconsistent is only correct for theories satisfied by the standard model. — Carl (CBM · talk) 18:16, 13 December 2007 (UTC)

Which are the inconsistent theories satisfied by the standard model:-) ? --Trovatore (talk) 18:17, 13 December 2007 (UTC)

Indeed; it seems there isn't much content there. But hopefully you can see the argument I had in mind. — Carl (CBM · talk) 18:19, 13 December 2007 (UTC)

A less content-free way of saying it would be: a theory that proves itself complete will be ω-inconsistent. — Carl (CBM · talk) 18:21, 13 December 2007 (UTC)

What's the "standard model"? Wiki's standard model has to do with physics and particles. Bill Wvbailey (talk) 23:08, 13 December 2007 (UTC)

I think we're discussing theories of arithmetic here, so the standard model would be the genuine natural numbers with addition and multiplication. A "nonstandard model" would be one that satisfied many (or even all) of the same first-order sentences as the genuine naturals, but which contained fake natural numbers that can't be matched up with any of the true ones. --Trovatore (talk) —Preceding comment was added at 23:15, 13 December 2007 (UTC)

So it's more or less what Enderton calls "first order logic" (i.e. more or less Goedel's system: propositional logic, PA, predicate logic's ∀, identity =, enough recursion theory to form + and * )? Is this a "common phrase in the industry"? Should this phrase be disambiguated? Thanks. Bill Wvbailey (talk) 23:46, 13 December 2007 (UTC)

(←) The standard model is a structure, not a logical system. It's the intended model of the Peano axioms: {0,1,2,3,...}. We don't need the phrase in our articles, which is why I think it has no article. — Carl (CBM · talk) 23:50, 13 December 2007 (UTC)

JR Lucas is Inconsistent

The argument given by Russell and Norvig (Artificial Intelligence: A Modern Approach) is an excellent refutation of J. R. Lucas' supposition that because computers are essentially limited Turing machines, which being formal systems 'stronger' than arithmetic, and are thus limited by their own 'Godelian statement' - J. R. Lucas further draws the conclusion that this limitation precludes 'machine intelligence'.

The refutation Russell and Norvig use states thus:

p = J.R. Lucas cannot consistently assert that this statement is true.

Thus demonstrating that J. R. Lucas is himself limited by his own 'Godelian Statement' and by his own definition, he has rendered himself as lacking intelligence (Chapter 26 - Philosophical Foundations - AIMA by Stuart Russell and Peter Norvig.)

Shouldn't we include this?

-- 86.129.93.182 (talk) 01:56, 12 January 2008 (UTC)

No need for photo of Goedel

I see no need for a photo of Goedel at the top of the article. I generally feel images should be used only when they deepen the reader's understanding of the topic. This is particularly true of non-free images, which according to WP:NFCC#3 may be used only when "necessary"; in this case, I believe the photo of Goedel is not permitted by our nonfree image policy. But even if it were a free image of Goedel, I don't see how it contributes to the reader's understanding of the topic, and wouldn't support it without seeing a convincing reason. — Carl (CBM · talk) 18:56, 12 January 2008 (UTC)

Goedel deduced the Goedel Incompleteness Theorems. That's probably why there should be a picture of him. Plus, he's kinda funny looking, and that helps to support my theory that most mathematicians are funny looking people. Niubrad (talk) 01:12, 6 February 2008 (UTC)

Confusing to laymen/laywomen

Any way the writers/editors could make this article comprehensible to the average reader who does not have a degree in mathematics or physics? I'm not talking about "dumbing it down" just not assuming a lot of knowledge on the part of the reader which one could only get in upper division university classes.

This is a matter of communication more than anything else. I believe the information in this entry can be accurate but also made more understandable to the average user (which I think is the goal of Wikipedia). This is not Encyclopedia Mathematica, this is a reference source used by the general public. I don't mean these comments as a slight to the writers of this entry, more of a challenge to write copy that is both informative and basic to understanding this work.Nwjerseyliz (talk) 21:01, 12 January 2008 (UTC)

There is a complete lay-comprehensible proof on the talk page of this spin-off article. It's in section 8, under the title "Proof of Godel's Theorem". That proof used to be on this page, but it was considered inappropriately written. It was too short and too comprehensible. If you like it, feel free to cut and paste it into the body of the article. I have gone through too much censure to do it again.Likebox (talk) 22:39, 12 January 2008 (UTC)

This is a willful misrepresentation on the part of one aggrieved editor regarding the alternative 'proof' (so-called). Please review the talk page archives for a the full, complete, correct record of the discussion, and the outcome. While the article as it is certainly could be improved, made more accessible, can we please _not_ reignite that particular bonfire? —Preceding unsigned comment added by 65.46.253.42 (talk) 22:52, 30 January 2008 (UTC)

I am not going away. I'm just waiting for the other people here to come to their senses. The only reason I am responding at all is because of the "so called" parenthetical. The proof is complete and correct, and it is equivalent to Kleene's in its logic, but some people here had a hard time following it at first. It's very easy.Likebox (talk) 18:24, 31 January 2008 (UTC)

A rather difficutl question

I have always been quite put off by Godel's theorem. In the system that I normally use, I used Godel's formulation to find a statement that it could not prove, loaded its inverse as an assumption, and found the inverse could be quickly reduced to a contradiction. Is Godel's theorem sufficiently weak that it only requires that statement to not be reachable from the ruleset (it was not as it contained a reference to itself and would have had infinite length in my notation) or am I completely missing the point here? 75.42.82.54 (talk) 04:21, 15 February 2008 (UTC) JH

Given some adequate formal system T, the statement in Goedel's theorem will not be disprovable in T. If you believe you have done so, there is an error of some sort in your analysis. The statement also will not be infinite; it will be an ordinary, finite formula. — Carl (CBM · talk) 13:36, 17 February 2008 (UTC)

Your difficulties are the usual ones for those who try to understand Godel's theorem. The infinite length of your statement comes from the fact that when you say "P is unprovable" you are unpacking it into "'P is unprovable' is unprovable" etc, etc, which leads to an infinite length statement which is not allowed. This is the central technical difficulty in Godel's proof, how do you construct a sentence of finite length that can talk about itself?

To get around it, you need a finite way of saying "The statement composed of these symbols blah blah blah, copied and manipulated in this way blah blah blah is unprovable", where all the stuff in the sentence is just a tricky way of constructing the same sentence again. In Godel's proof this requires some contortions.

There is a modern shortcut. You can redefine the statements to be about computer programs, so that they are of the form "Program X doesn't halt". Then to get a statement which asserts that it is unprovable, you just move the self-reference into the computer program. If you know how to program a computer, it is pretty obvious that X can construct the sentence "Program X doesn't halt" by printing out it's own code into X and then adding the fluff around that.

X can then look at all the deductions of the axiom system looking for the theorem "Program X doesn't halt", and halt if it finds this theorem. Now the statement "Program X doesn't halt" is asserting its own unprovability.

The reason you came to a quick contradiction from assuming the negation of P is because you are automatically assuming that your axiom systems are consistent (and omega consistent) without hesitation. These assumptions are independent of the axioms you start with, if you are careful to write out everything precisely, as in a computer program. If you are informal about the mathematics, then Godel's statement is obviously true (although unprovable in the original axioms), as Godel pointed out.Likebox (talk) 19:45, 17 February 2008 (UTC)

And here's the answer. My system does in fact allow infinite statements of finite Kolmogorov_complexity. Godel's theorem, however, depends on ZF, while I cannot yet prove that my axiom set is ZF. The fact that the Axiom of Choice should be true but any attempt to use the Banach–Tarski_paradox doesn't work suggests that it isn't. However, I cannot eliminate an error in the proof of that paradox.

Also, allowing infinite statements certainly means that my system is not recursively enumerable. Furthermore, there are unprovable statements; the problem is merely that Godel's construction didn't find one. Thanks for your time. 75.42.82.54 (talk) 22:42, 17 February 2008 (UTC)JH

Goedel's theorem does not require ZF or the axiom of choice; it applies to very weak subsystems of Peano arithmetic. But if your system isn't effective, then there is no reason to expect Goedel's theorem to apply in the first place. — Carl (CBM · talk) 00:20, 18 February 2008 (UTC)

How sure are you that your system is consistent? If it allows infinite statements, how does it avoid Curry's paradox? -- BenRG (talk) 03:12, 18 February 2008 (UTC)

Trying to falsify Godel

I changed an entry to Godel as it was blatantly trying to hide the facts about Godels proof. The entry said Godels system P was Peano arithmetic this is a blatant falsification. System P is according to godel "By and large, P is the system that you get by building the logic of PM on top the Peano axioms On formally undecidable propositions —Preceding unsigned comment added by Xamce (talk • contribs)

That is not a quote from Goedel, but rather from a translation, as the original is in German. The translation by van Heijenoort is somewhat superior, but I don't think a direct quote is needed anyway, simply the fact that P is obtained by adding the Peano axioms to the logical system of Principia Mathematica. — Carl (CBM · talk) 16:29, 29 February 2008 (UTC)

I made Carl's proposed change. I do want to keep the van Heijenoort quote, however. When I first confronted this topic (and this article) I was very confused about the "first" and "second" incompleteness theorems -- I went searching for them in the translations and couldn't find them. Only after careful reading of the translations was I able to make the connection. The quote also makes it clear that this isn't trivial stuff. Bill Wvbailey (talk) 17:06, 29 February 2008 (UTC)

I meant the quote from Hirzel's translation, sorry. I have never really liked having the original statement of the theorem but I won't argue strongly against it. — Carl (CBM · talk) 17:23, 29 February 2008 (UTC)

second incompleteness theorem

There is obviously an error in the following. Can someone spot it?

1. An inconsistent system is one that proves a false contradictory statement, like 1=0. (definition). A contradictory statement S is one where both S and not-S are provable.
2. If you can prove a false contradictory statement you can prove any statement. (Principle of explosion).
3. Therefore, in an inconsistent system, all statements are provable. Any system with an unprovable statement (whether true or false) must be consistent. (The converse is not necessarily true, for example the empty theory).
4. The first incompleteness theorem proves that a sufficiently powerful, consistent system contains an unprovable statement, which we'll call G.
5. Further (let's assume for concreteness that the system is PA) the proof that G is unprovable in PA can itself be carried out in PA. (Showing this is the main technical content of the second theorem). (Question: is the proof of the first theorem finitistic in the Hilbert sense?)
6. Thus, PA proves that PA contains a statement G which is unprovable in PA, and therefore (from point 3 above) PA proves its own consistency, the opposite of what the second theorem says.

Is the problem that the principle of explosion can't be proved in PA? That would surprise me since it goes back to ancient Greece. More likely I've missed something different and obvious. Thanks. (Added: the remarkable thing about the first theorem is it shows a statement that is unprovable but true. The above consistency argument would be satisfied by exhibiting a statement that is provably unprovable even if it's false. I'd expect that to be easier--is it?)

Hello. The main mistake is that PA can just prove (an arithmetical statement that is interpretable as) "if PA is consistent then PA cannot prove G". Incidentally also your way to express the principle of explosion is incorrect: they are not "false" statement that imply everything, just contradictions do that.--Pokipsy76 (talk) 12:36, 5 January 2008 (UTC)

Thanks, I fixed "false", I think maybe the article is a bit unclear about G. I'll have to look at it more closely.

Theorem #1

Wouldn't it be easier to understand (and equivalent to say) that for any theory there exists a statement which is not provable except by using a proof by contradiction?--Loodog (talk) 15:28, 9 April 2008 (UTC)

No, that's not equivalent in any meaningful sense. --Trovatore (talk) 16:56, 9 April 2008 (UTC)

Then I'm misreading this article. I thought it was saying: A statement exists such that either the statement is true or it contradicts the system.--Loodog (talk) 17:21, 9 April 2008 (UTC)

Not exactly. It's more like, either the statement is true, or the system contains a contradiction. The second part is not the same thing as the statement itself contradicting the system. --Trovatore (talk) 17:53, 9 April 2008 (UTC)

Footnote 1

The content of footnote 1 seem to me completely irrelevant. I would consider replacing it with a totally different text: Some theories have a standard model, for example natural numbers are the standard model of Peanno Arithmetics, although this theory has many different (non-isomorphic) models. We say that a statement is true in the theory if the standard model satisfies it. Provable statements are always true, but not vice versa. What do you think? --Pavel Jelinek (talk) 17:53, 18 June 2008 (UTC)

Hmm, well, I wrote that footnote, so I'm not unbiased, but certainly I can accept that it might be improved. (I certainly do not agree that it's "irrelevant". :-) But I don't know if it's useful to bring in models, and especially standard models. The "disquotational" version correctly explains the situation to a reader that does not accept the existence of a completed set of natural numbers, provided that reader accepts that first-order statements whose variables are restricted to the naturals are meaningful. --Trovatore (talk) 00:55, 19 June 2008 (UTC)

Following up on that, it's said that Goedel originally considered phrasing his results semantically, but decided they would be more compelling if presented purely syntactically, since that removes any possible objections related to semantic truth in the natural numbers (see [1] for example). Maybe a sentence could be added to the footnote explaining that it is also possible to read "true" as "true in the standard model of the natural numbers", but the disquotational interpretation doesn't invoke the standard model at all. — Carl (CBM · talk) 01:07, 19 June 2008 (UTC)

I am sorry, I do not understand what it is completed set of natural numbers. Secondly, I found no definition what it means that arithmetical statement is true. I have always thought that true means satisfied in the standard model. If I am wrong, please tell the correct definition. If I am right here, then it seems to me imposible to leave out standard models from the explanation in the article.

I read the article at stanford.edu (cited by Carl) and it seems as if "satisfies" there means the same as "is true" here, and the author uses this term again without definition. Im convinced that our article should contain the definition of true statement (or at least a very clear link to the definition).

I am convinced that the statement "arithmetical statement S is true" is a statement in meta-theory while S is a formula in Peano arithmetics. It is impossible to claim equivalence between a (metamathematical) statement about a theory and a formula in that theory. Therefore I still cannot see any connection between the topic of our article and disquotationalism. I would fully accept this connection if we said "M is true" about a meta-mathematical statement M. --Pavel Jelinek (talk) 19:27, 21 June 2008 (UTC)

You're correct that a statement of arithmetic is true simpliciter if and only if it's true in the standard model. But the point is that you don't have to believe in the standard model (or any model of PA) to make sense of a statement of arithmetic being true. Suppose you believe that there are things that are natural numbers, and things that aren't, but that there is no set containing all the natural numbers. Then you don't believe in the standard model. But you can still believe that every natural number is the sum of the squares of four natural numbers; that's still a meaningful statement. And then you can believe the claim the statement "every natural number is the sum of the squares of four natural numbers" is true, just by removing the quotation marks and the redundant verbiage around them. --Trovatore (talk) 19:19, 21 June 2008 (UTC)

Responding to your last paragraph, which you apparently added after my first response: An equivalence between the claim "S is true" and the claim S is precisely what disquotationalism gives you, and that's exactly why it's relevant. But the reason for mentioning it is simply to avoid difficulties with the word "true", not to say anything deep about the underlying content.

Here's the point: Suppose I don't believe in infinite sets, but I do believe that a certain formal theory T is consistent. Must I believe G_T, even though G_T is not provable from T? Yes, I must. That's the motivation for saying that G_T is true, though unprovable in T. But people were quibbling on the word "true", so I added the footnote explaining it. --Trovatore (talk) 20:32, 21 June 2008 (UTC)

Oh, here's a possible place we might be talking past each other: When I talk about G_T, I'm talking about a statement of arithmetic, no matter what T is. The objects of discourse of T might be natural numbers, but they might also be real numbers, or sets, or fictional French kings from possible science fiction novels that may or may not have been written. The objects of discourse of G_T are always natural numbers, and when we say that T does not prove G_T, what we really mean is that T does not prove the translation of G_T into the language of T. (That such a translation exists is one of the hypotheses of the theorem -- the "relative interpretability" one.)

So when I say I am forced to accept G_T if I accept that T is consistent, I mean that I am forced to accept it as a claim about the natural numbers. I am not necessarily forced to accept it as a claim about the intended model objects of discourse (if any) of T. Does that clear things up? --Trovatore (talk) 23:49, 22 June 2008 (UTC)

I will answer you after I think about it, but I want to say another thing. If we want to make an exact mathematics, then we may only work with exactly defined terms. What exact definition of "true" do you propose? Btw. if my formatting of my contributions here is wrong, I do not mind anyone to correct it. (If I formatted is as usual, we would soon get to 15 indents (:::::::::::::::) and I am not sure if this is the best way. Pavel Jelínek, 12:40, 23 June 2008 (UTC)

Well, I already told you what I mean by G_T is true--it means just the same thing as G_T; that's the use of disquotationalism. So are you asking what it means to accept G_T? Well, G_T asserts that there is no natural number with a certain property (the property can be coded into a computer program that is guaranteed to halt). When I say I accept G_T, I mean I accept that there is no such natural number. And I must accept that, if I accept that T is consistent, because if there were a natural number having that property, I could recover from it, in a completely effective manner, a formal contradiction in T. --Trovatore (talk) 16:55, 23 June 2008 (UTC)

Inconsistency as a Consequence of Gödel's Argument

An anon added a section entitled Inconsistency as a Consequence of Gödel's Argument. It was full of references, but I could not work out what its claim was supposed to be. Thus I have removed it for now. There may well be material in it worthy of appearing in the article, but if so it needs to be explained more clearly. I would encourage the anonymous poster to register an account if he/she is interested in having this material incorporated, as it is very difficult to have a productive discussion with an IP address. --Trovatore (talk) 23:20, 22 June 2008 (UTC)

The section makes sense according to the published references although it could be explained more clearly. I have included it below so that editors can discuss.--67.169.49.125 (talk) 17:21, 23 June 2008 (UTC)

Proposed section on Inconsistency as a Consequence of Gödel's Argument

Mathematical logicians almost unanimously followed Gödel in adopting the assumption of hierarchical meta-theories. The standard justification of the assumption of hierarchical meta-theories was exactly that it avoided inconsistencies. Tarski and his successors adopted the assumption and made into a framework that became the bases of model theory. But Feferman has pointed out that “…natural language abounds with directly or indirectly self-referential yet apparently harmless expressions—all of which are excluded from the Tarskian framework.” Thus there are substantial reasons to avoid adopting the assumption of hierarchical meta-theories.

Much earlier, Wittgenstein disputed Gödel's assumption of hierarchical meta-theories. Consequently he argued that Gödel's argument led to an actual inconsistency because without the assumption of hierarchical meta-theories, it is easy to show that the paradoxical sentence p is provable (and this proof can even be done paraconsistently). And Gödel showed that p is provable leads to inconsistency. Thus Wittgenstein maintained that Gödel's argument led to inconsistency, a consequence that was totally unacceptable to mathematical logicians at that time.

It is worth noting in this regard that according to Graham Priest in 1930 Wittgenstein remarked "Indeed, even at this stage, I predict a time when there will be mathematical investigations of calculi containing contradictions, and people will actually be proud of having emancipated themselves from consistency." Subsequently paraconsistent logic has been developed which provides exactly this kind of emancipation from consistency. Thus, using paraconsistent logic, it is possible to concur with Wittgenstein in maintaining inconsistency as a consequence of Gödel's argument without being able to prove everything.

Gödel was aware of Wittgenstein's views and disliked them intensely. According to Rebecca Goldstein,

"Gödel had harsh things to say about Wittgenstein later in his life. Never, of course, face to face, usually not even to other people, but in letters. Most of them he never sent, and I came upon them in Firestone among the literary remains, the Nachlass, of Gödel. Wittgenstein never accepted Gödel's result; he said in The Foundations of Mathematics, posthumously published, that his task is not to discuss Gödel, but rather to bypass Gödel. He also called Gödel's results the tricks of a logical conjurer, logical artifices. Kunststücken. Someone told Gödel about this and it was then that he let vent some of his annoyance about Wittgenstein, annoyance that was, if my psychological speculations are right, decades old, hatched long ago while Gödel listened to the positivists extolling Wittgenstein's views, understanding him to vindicate their condemnation of all metaphysical views, including Platonism."

Discussion of "inconsistency" section

OK, I don't have time to say much, but very quickly here are my most obvious questions:

1. The section is entitled "Inconsistency as a Consequence of Gödel's Argument". Inconsistency of what, exactly? Of the theory T, assuming that T proves G_T?
2. Who says that Gödel "assumed hierarchical metatheories"? I haven't read his original paper, but certainly there is no need to use a hierarchy of metatheories to discuss the result--you work in a single metatheory, which is strong enough to encode the provability predicate for the object theory T. Certainly, if you like, you can describe your meta-theory proofs in some meta-meta-theory, but there is no obvious advantage in doing so (especially since the meta-meta-theory would just be PA or some fragment of it again, same as the meta-theory).
3. Who says that hierarchical metatheories led to model theory? It's not impossible that this is the case historically (history is not really my strong suit) but I personally don't see much of a connection, especially for the sort of metatheories we're discussing here, which exist only to prove syntactic results, not semantic ones.
4. How is dropping "the assumption of hierarchical metatheories" supposed to allow you to prove the Gödel sentence for a consistent theory T, if you couldn't prove it with that assumption? Generally, dropping assumptions allows you to prove fewer things, not more. Surely, some extra assumption or rule of inference must also have been added?

This is just a start, but if you can explain what you're getting at with regard to these four points, we should be moving towards clarity. --Trovatore (talk) 23:45, 23 June 2008 (UTC)

The second paragraph appears to confuse the issue of which logic is being used. Ordinary PA in first-order logic has been proven consistent, but I'm sure there are other, nonstandard logics that include reflection principles such that the axioms of PA are not consistent in these nonstandard logics. This in no way affects Goedel's theorem.

This confusion about which logic is being used also seems to affect the third paragraph. This paragraph doesn't seem to be about Goedel's theorem at all, only about paraconsistent logic. I don't know what "maintaining inconsistency as a consequence of Gödel's argument " means there - which inconsistency? This is particularly confusing because the theory to which Goedel's theorem is most often applied is the consistent theory of first-order PA. — Carl (CBM · talk) 02:48, 24 June 2008 (UTC)

(The following are replies to Trovatore's questions, moved down so they aren't interspersed with the original comments. The numbers match. — Carl (CBM · talk) 03:00, 24 June 2008 (UTC))

1. The inconsistency is that T proves that G_T is provable in T and also that T proves that G_T is not provable in T.--67.169.145.42 (talk) 02:55, 24 June 2008 (UTC)
2. Once is assumed that each theory has a hierarchical metatheory, there is a whole hierarchy.--67.169.145.42 (talk) 02:55, 24 June 2008 (UTC)
3. Without the assumption of hierarchical metatheories, every sufficiently powerful theory is inconsistent and consequently has no models.--67.169.145.42 (talk) 02:55, 24 June 2008 (UTC)
4. Imposing the assumption of hierarchical metatheories, allows consistency to be proved (see Gentzen's consistency proof)).--67.169.145.42 (talk) 02:55, 24 June 2008 (UTC)

I don't follow what you are saying in #1. Let's take the specific case where T is first-order Peano Arithmetic. In this case, T will not prove G_T (this is the first incompleteness theorem), nor will T prove that G_T is provable (because if PA proves that an arithmetical statement is provable in PA, then the statement really is provable in PA).

I don't think your answers to #3 and #4 actually address the questions being asked. — Carl (CBM · talk) 03:07, 24 June 2008 (UTC)

If T is Peano Arithmetic with reification reflection, then T proves both of the following:

• G_T is provable in T
• G_T is not provable in T.

You are correct that the following are equivalent:

• T proves that G_T is provable in T
• T proves G_T

--67.169.145.42 (talk) 05:45, 24 June 2008 (UTC)

The example I chose was the ordinary first-order theory of PA, not PA with reification reflection. It seems, like I said, that you are not looking at the first-order theories to which Goedel's theorem is typically applied. It may be possible to clarify the proposed text; one necessary clarification will be to explain exactly which logic you are working with, since it isn't the logic that is typically employed. — Carl (CBM · talk) 13:11, 24 June 2008 (UTC)

Of course, Gödel's incompleteness theorems do not apply to first-order theories since they are complete.

Incompleteness can be proved for arithmetic (with induction) that includes some kind of reificaton reflection principle. Now it just so happens that Gödel used a certain kind of reification reflection that involved using Gödel numbers for reification. However, character strings or even XML could be used instead.

A paraconsistent logic in which the proof of inconsistency is carried out was published in reference 3 in the proposed section above.--67.169.9.185 (talk) 15:14, 24 June 2008 (UTC)

First-order Peano Arithmetic is not complete - that's the immediate consequence of Goedel's theorem, which certainly does apply to first-order PA. I'm having trouble understanding the argument you are making, which is why I want to start by figuring out how what you are saying applies to the familiar setting of PA in first-order logic. As far as I can tell, the "inconsistency" the proposed text is referring to is inconsistency only in theories under paraconsistent logic, not inconsistency in theories under first-order logic. Do we agree enough about terminology to agree that first-order PA is consistent and incomplete? — Carl (CBM · talk) 15:40, 24 June 2008 (UTC)

I'm going to try to rephrase what I think the anon may be getting at into more standard language. Anon, correct me if I get it wrong.

What the Goedel theorems don't seem to rule out in any obvious way is the following: There might be a collection of axioms T such that when T is closed under provability in some paraconsistent logic, T proves G_T, and nevertheless T does not prove all sentences in the language of arithmetic (using the stipulated logic). Then it is conceivable that T might be negation-complete -- it would prove every statement in the language of arithmetic or its negation, and in some (but not every) case would prove both the statement and its negation. Then a dialetheist (spelling?) could take arithmetic truth to equal provability in T, accepting that some statements are both true and false. Is that the idea? --Trovatore (talk) 03:20, 24 June 2008 (UTC)

T paraconsistently proves that G_T is provable in T and also T paraconsistently proves that G_T is not provable in T. So the inconsistency follows even for paraconsitent theories. If T happens to also be a classical theory then T can prove everything because of the inconsistency.--67.169.145.42 (talk) 05:45, 24 June 2008 (UTC)

What is T? Can you give us an outline of a proof of G_T, formalizable in T using some paraconsistent logic? (Please also specify the paraconsistent logic you have in mind.) --Trovatore (talk) 07:23, 24 June 2008 (UTC)

Reference 3 in the proposed scection above has axioms for a paraconsistent logic that are sufficient to show that T proves G_T.--67.169.9.185 (talk) 15:14, 24 June 2008 (UTC)

Could you directly answer the question of what the theory T is? That would help me greatly in understanding your argument. I downloaded the paper in reference 3, so you can use page numbers from that paper if it helps. I am simply looking for a precise definition of what you mean by the theory T. — Carl (CBM · talk) 15:41, 24 June 2008 (UTC)

In reference 3, properties of strongly paraconsistent theories are automatized in a way similar to the way that properties of numbers are often automatized. What else do you want?--67.180.94.244 (talk) 15:47, 24 June 2008 (UTC)

It just occurred to me that there is another interpretation of your question. Since the proof of inconsistency can be carried out for any (sufficiently strong) paraconsistent theory T, it can be carried out in ⊥ (the empty strongly paraconsistent theory with no domain axioms).--67.180.94.244 (talk) 16:06, 24 June 2008 (UTC)

You're not answering the question. For example, the theory must have some nonlogical symbols in order to have formulas at all - what is the signature of a particular theory T that you are interested in? If it has no axioms, how is is that the hypotheses of Goedel's theorem apply? (These require, essentially, that the theory is able to represent several computable functions. We know that these are not representable in sufficiently weak theories of arithmetic, and so are not representable in the first-order theory in the language of PA with no axioms.)

These questions are not at all addressed in reference 3 in the text above (available at SpringlerLink [2]). That paper doesn't appear to precisely define anything, nor to actually give the proof that its abstract claims. If I have somehow overlooked these, please let me know the page numbers so I can look at the paper in more detail. I also downloaded "Common sense for concurrency and strong paraconsistency using unstratified inference and reflection", so you can give page numbers from that if you wish. — Carl (CBM · talk) 17:20, 24

The paper deals with theories for software engineering, so standard theories of mathematics (e.g., lambda calculus, functions, arithmetic, etc.) are built in. The domain axioms are for the particular area of software (e.g. operating systems, web pages, data bases, etc.). Consequently even the empty theory ⊥ with no domain axioms is sufficient to prove inconsistency.--67.180.94.244 (talk) 17:41, 24 June 2008 (UTC) June 2008 (UTC)

Since there is insufficient space available for the proofs, the published paper references the other paper that you downloaded ("Common sense for concurrency and strong paraconsistency using unstratified inference and reflection") where the proof of inconsistency is on page 12.--67.180.94.244 (talk) 17:41, 24 June 2008 (UTC)

Which "standard theories of mathematics" do you mean are built in? Where is the precise theory T defined? I think one issue here is that Trovatore and I are expecting a more rigorous style of conversation, in which everyone is willing to precisely define all terms used. Both Trovatore and I have strong backgrounds in mathematical logic, so we are accustomed to that style of discussion.

Let's start with my question from above, just to get the terminology straight. Do we agree enough about terminology to agree that first-order PA is consistent and incomplete? — Carl (CBM · talk) 17:47, 24 June 2008 (UTC)

Software engineers make use of a variety of standard mathematical theories, e.g., lambda calculus, arithmetic with induction, etc. None of this should be problematical. If you want to be very concrete, you could just take the ones defined in "Common sense for concurrency and strong paraconsistency using unstratified inference and reflection"--67.180.94.244 (talk) 18:21, 24 June 2008 (UTC)

Of course, as Gödel proved, all first-order theories are complete. So Gödel proved that arithmetic with induction (which is of course not a first-order theory) is incomplete. The question of consistency turns on two questions:

1. What kind of reification reflection is used: Gödel assumed that every proposition can be reified as a number.
2. The hierarchical nature of metatheories: Gödel made the assumption of hierarchical metatheories. This assumption was denied by Wittgenstein and later questioned by Feferman.

--67.180.94.244 (talk) 18:21, 24 June 2008 (UTC)

All first-order theories are complete? I really hope this is a joke. In the unlikely event that it is not, have a look at Gödel's completeness theorem. (Fourth paragraph.) --Hans Adler (talk) 18:28, 24 June 2008 (UTC)

First-order theories are complete in the sense that a proposition is valid (true in all models) if and only if it is provable.--67.180.94.244 (talk) 18:47, 24 June 2008 (UTC)

It's an unfortunate fact that we are using the same adjective to refer to two completely different things. The standard practice is to keep them apart by never using them to refer to the same kind of thing: "The logic L is complete" always refers to the adjective from the completeness theorem, and "The theory T is complete" always refers to the adjective from the incompleteness theorems. I hope you can understand why my woolly thinking alarm went off violently when you got this elementary point wrong in this particular situation. --Hans Adler (talk) 19:06, 24 June 2008 (UTC)

I do not believe the "common sense" paper actually defines the theory T in any way. Could you give a page number for that definition, in case I missed it? The question is: exactly what theories can be used for the T. I am not looking for a vague assertion, just an actual precise mathematical definition. "The ones used in practice" is not precise in any way."

By the way, please stop inserting comments in the middle of other people's comments; doing so makes it hard to follow the conversation in order. — Carl (CBM · talk) 18:39, 24 June 2008 (UTC)

Software engineering has to deal with a variety of theories. In particular it must deal with theories that are open-ended schematic axiomatic systems (Feferman 2007b Gödel, Nagel, minds and machines). The language of a theory can include any vocabulary in which its axioms may be applied, 'i.e.', it is not restricted to a specific vocabulary fixed in advance (or at any other time).

That said. There is a particular concrete theory, namely ⊥, on which you can focus your attention. The theory ⊥ consists of the theories automatized in the first appendix of "Common sense for concurrency and strong paraconsistency using unstratified inference and reflection" pages 25-28.--67.180.94.244 (talk) 19:03, 24 June 2008 (UTC)

(←) Let's start at the beginning: what is the signature of this theory ⊥? Per my terminology key below, I am using the term theory to indicate a signature and a set of formulas in the signature. Pages 25 to 28 of the paper describe a proof system, but not any theory. Indeed, page 25 begins by assuming that the reader knows what a "paraconsistent reflective theory for large software systems" is; the term doesn't seem to be defined. — Carl (CBM · talk) 19:14, 24 June 2008 (UTC)

The appendix presents axioms that apply for every T which is a paraconsistent reflective theory. The theory ⊥ is a particular such T that picks up its signature from the sections that follow on the lambda calculus, XML, and elementary set theory.--67.180.94.244 (talk) 19:25, 24 June 2008 (UTC)

I see no mention of λ calculus or elementary set theory at all in the paper (apart from the statement that direct logic uses higher order logic - maybe that's what you mean). Given that XML is an abbreviation for "Extensible Markup Langauge", formulas like "P ⊆ XML" don't make sense, any more than "P ⊆ HTML" would make sense. Can't you just come out and say what the signature of your theory ⊥ is? Equally good, you could give a definition of a well-formed formula in the language of the theory. — Carl (CBM · talk) 19:47, 24 June 2008 (UTC)

The λ calculus is automatized on page 26 and the comprehension axiom for sets derived from XML is on page 27. The expressionn "P ⊆ XML" means that P is a subset of the set of valid XML.--67.180.94.244 (talk) 20:15, 24 June 2008 (UTC)

Ignoring for the moment whether those are axiomatizations: can you directly answer the question: what is the signature of your theory ⊥? Even better, can you give a precise definition of a well-formed formula in the language of the theory? — Carl (CBM · talk) 20:37, 24 June 2008 (UTC)

(←) OK, we do have some terminology issues. Here is the terminology I would like to use; it is the standard terminology in mathematical logic.

• Goedel proved that first order logic is complete, in the sense that a formula is provable from a set of axioms if and only if the formula is satisfied by every structure that satisfies the axioms. This is Goedel's completeness theorem.
• A first-order theory consists of a signature and a set of formulas in that signature, known as the axioms. A first-order theory is consistent if and only if there is at least one formula that is not provable from the axioms. A first-order theory is complete if for every formula in its signature, either that formula or the negation of that formula is provable from the axioms.
• Goedel proved that no effective first-order theory that includes a sufficient fragment of arithmetic is both consistent and complete. This is the content of the incompleteness theorems. The sense of the word complete is different between completeness theorem and incompleteness theorem.
• As a particular example, Peano Arithmetic is a first-order theory that is both consistent (as proved by Gentzen, Goedel, and others) and incomplete (as a consequence of Goedel's incompleteness theorem and the consistency proofs).

I hope that will clear up some of the issues here. In particular, I am confused about the phrase "Inconsistency as a Consequence of Gödel's Argument" because it is the incompleteness of PA, not the inconsistency of PA, that the incompleteness theorems establish. — Carl (CBM · talk) 18:36, 24 June 2008 (UTC)

This is exactly the point: Using what some authors have considered to be very reasonable assumptions, a slight extenstion of Gödel's argument leads all the way to inconsistency, not just incompleteness. Making sense of this is where Wittgenstein and paraconsistency come in. —Preceding unsigned comment added by 67.180.94.244 (talk) 19:15, 24 June 2008 (UTC)

I take it that what you mean is that "a slight extension of Gödel's argument" shows that the PA axioms supplied with the rules of inference of a particular paraconsistent logic give an inconsistent theory. Is that indeed what you mean? --Trovatore (talk) 19:30, 24 June 2008 (UTC)

It's formally proved that Arithmetic+Induction+Reflection+NonhierarchicalMetatheories+λ-calculus lead to inconsistency (even for paraconsistent theories). Gödel used Arithmetic+Induction+Reflection+HierarchicalMetatheories+ClassicalLogic to prove incompleteness (using the λ-calculus just makes it easier and clearer).

Of course, the rules of paraconsistent logic are a 'subset' of the rules of classical logic.

Wittgenstein seems to have been the first to weigh in on extending Gödel's argument. Gödel intensely disliked Wittgenstein views and resented his influence.

--67.180.94.244 (talk) 20:06, 24 June 2008 (UTC)

Your invocation of the phrase "nonhierarchical metatheories" is, I fear, concealing something, even if that is not your intent. Do you agree that no contradiction follows (or at least none has been discovered to follow) from the PA axioms, using the ordinary rules of inference from first-order logic? There is no need to discuss metatheories in responding to that question; it's a simple question of fact. --Trovatore (talk) 20:17, 24 June 2008 (UTC)

I agree that we have found no contradiction from Arithmetic+Induction. On the other hand, it is unclear how to formally state and prove the incompleteness theorems within Arithmetic+Induction.--67.180.94.244 (talk) 20:24, 24 June 2008 (UTC)

No, it isn't. --Trovatore (talk) 20:25, 24 June 2008 (UTC)

67.180.94.244 : I think you're confusing an issue here. You have claimed several times that PA has a reflection principle, which it does not in the sense I think you mean. The rest of this comment assumes we have fixed PA as our theory. The Goedel sentence φ is provably (in PA) equivalent to NotPvbl(#φ), and Goedel showed that φ is not provable in PA. This does not mean that ψ = NotPvbl(#φ) is provable in PA (indeed, ψ is not provable in PA, because there are nonstandard models of PA satisfying Pvbl(#φ)). So there is no reflection principle that says that if an arbitrary formula φ is not provable in PA, then NotPvbl(#φ) is provable in PA. However, I believe that the source of inconsistency in your paraconsistent system is not the paraconsistent logic, but the addition of additional inconsistent reflection principles. It appears to me that this happens in the 'admissibility' criterion on p. 10 of the "common sense" paper, which is then used in the proof on p. 11. — Carl (CBM · talk) 20:29, 24 June 2008 (UTC)

It is important to note that 'admissibility' serves only to restrict the use of reflection. Thus it cannot possibly be the source of inconsistency. Also, your statement as follows is correct:

"So there is no reflection principle that says that if an arbitrary formula φ is not provable in PA, then NotPvbl(#φ) is provable in PA."

However, the paper does not assume any such reflection principle.

The statement that "φ is provably (in PA) equivalent to NotPvbl(#φ)" embodies a reflection principle.

--67.180.94.244 (talk) 20:48, 24 June 2008 (UTC)

It appears to me that the inconsistency is because of the reflection used at the top of the right hand column on p. 11. Another possibility is that the paper has rediscovered a variation of the Kleene-Rosser paradox. But we are starting to dwell on the paper instead of the article. What do you think about the proposal below? — Carl (CBM · talk) 21:21, 24 June 2008 (UTC)

The inconsistency is not due to the Kleene-Rosser paradox as pointed in the footnote on page 11.

Furthermore, the inconsistency is not due to the use of reflection at the top of the right hand column on pg. 11 because that only proves the diagonal lemma (see Gödel's_incompleteness_theorems#Diagonalization).

--67.180.94.244 (talk) 21:58, 24 June 2008 (UTC)

I realized that a little after I wrote the last comment, looked further, and found something more interesting. The argument on page 11 uses a "Right meta direct indirect inference" rule, a different sort of reflection principle from p. 6. This rule says

|- ([ψ |-_T (|-_T ~ ψ)] → |-_T ~ψ)

or, equivalently, and changing the inner |-_T to Pvbl as required:

(*) If T proves ψ → Pvbl(#(~ψ)) then T proves ~ψ

This is interesting because it is classically false. Let ψ be the sentence Pvbl(#(0=1)). Then ψ is consistent with PA, and moreover PA proves (ψ → Pvbl(#φ)) for every formula φ, because any model of ψ has a nonstandard "proof" of every formula. Thus PA does prove that ψ → Pvbl(#(~ψ)). But the principle (*) then says PA proves ~ψ, which means PA proves ~Pvbl(#(0=1)), which PA does not prove by the second incompleteness theorem. Perhaps this is the actual source of the inconsistency results in the paper. — Carl (CBM · talk) 21:55, 24 June 2008 (UTC)

Note that PA proves that ψ→Pvbl(#(~ψ)) only because PA is classical and 0=1 is an inconsistency.

For the system in the paper, in order to use "Right meta direct indirect inference" rule to prove |-_PA' ~ψ, you would have to show

ψ |-_PA' (|-_PA' ~ ψ)

where PA' is Arithmetic+Induction+ParaconsistentLogic.

The above example illustrates that in some ways it can be more difficult to prove inconsistencies in paraconsistent logic.

---67.180.94.244 (talk) 23:10, 24 June 2008 (UTC)

this points out, the inference rules in most paraconsistent logics are a strict subset of the inference rules of classical logic. A theory that was already consistent classically cannot become inconsistent simply through the removal of inference rules. But anyway, what do you think of my proposal below? — Carl (CBM · talk) 19:55, 24 June 2008 (UTC)

Although the logical rules regarding the Boolean connectives are weaker for paraconsistent logic, the rules for reflection and nonhierachical metatheories can be stronger stronger.--67.180.94.244 (talk) 23:12, 24 June 2008 (UTC)

Abridged version

My current impression of the material is that it is excessively focused on paraconsistent logic, which is not really the subject matter of Goedel's theorems as they are understood in the literature. I think it is out of place to include such a long discussion about paraconsistent logic here. I would be willing to add something brief to the article, such as:

Although Gödel's theorems are usually studied in the context of first-order logic, recent work by Carl Hewitt has demonstrated consequences of the theorems for paraconsistent logic.

This could be accompanied by a single reference to a paper by Hewitt your choice. As Hewitt's work is too new to have been properly accepted by the logic community, I don't immediately see a need to go into depth about it here. — Carl (CBM · talk) 17:47, 24 June 2008 (UTC)

I think that there is a lot of merit in this suggestion. However, I do have a couple of questions/suggestions.

1. Does Wittgenstein's contention that Gödel's argument can be extended to inconsistency deserve mention?
2. Perhaps the wording above could be improved as follows:

In the more general framework of nonhierachical metatheories (see Feferman ) , recent work by Carl Hewitt shows how Gödel's argument can be extended to inconsistency in the context of paraconsistent logic (see ).

This could probably be further improved.--67.180.94.244 (talk) 22:14, 24 June 2008 (UTC)

I think any mention of Wittgenstein should be kept brief. He was not a mathematician, and my sense is that he is not taken particularly seriously by philosophers of mathematics, at least as regards philosophy of mathematics.

On point (2), I would say no, at least not with that wording. The change you require to derive an inconsistency is not simply metatheoretic as most of us are likely to understand the term -- it goes down into the object theory, making it a different theory. Also the vague use of the mass noun "inconsistency", as one might use "stormy weather", is one of the first things I objected to. --Trovatore (talk) 22:29, 24 June 2008 (UTC)

OK, how about the following wording:

In a more general context of self-referential statements that lies outside Gödel's framework (see Feferman ) , recent work by Carl Hewitt shows how Gödel's argument can be extended to prove Gödel's paradoxical statement (and thus produce an inconsistency in the theory) using paraconsistent logic (see ).

--67.180.94.244 (talk) 23:04, 24 June 2008 (UTC)

Actually, that's not bad. --Trovatore (talk) 23:51, 24 June 2008 (UTC)

Thanks, would you like to make the edit?--67.180.94.244 (talk) 00:45, 25 June 2008 (UTC)

I would prefer something like

Recent work by Carl Hewitt extends Gödel's argument to show that, in a particular paraconsistent logic permitting more self-reference and indirect inference than first-order logic (see Feferman ), sufficiently strong theories are able to prove their own Gödel sentences, and are thus thus inconsistent..

I think order is somewhat more clear, and I think it's important to remember this is just one particular paraconsistent logic. I don't believe Hewitt has shown that his results apply to paraconsistent logics whose inference rules are a subset of the inference rules of classical logic.

Yes, that's better. Except that it does appear to attribute the particular logic to Feferman. Is that accurate? --Trovatore (talk) 17:48, 25 June 2008 (UTC)

Good point, Trovatore. Paraconsistent logic should not be attributed to Feferman.

So how about the following suggested improvement?

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 theories are able to prove their own Gödel sentences, and are thus inconsistent.

--169.230.124.110 (talk) 20:37, 25 June 2008 (UTC)

The Extensions of Gödel's original result section seems like a natural place. I copied the text there. I changed the Fererman reference to match the information given by the JStor link that was already there (was the paper published twice?!?). — Carl (CBM · talk) 00:09, 26 June 2008 (UTC)

External links cleaning

I propose cleaning up this section; there's a lot of personal waxing philosophic, pages that sell products, link collections on goedel, and simply sloppy pages. I propose keeping just:

• Stanford's page
• MacTutor pages
• Dale Myers page (this seems like the least bad of these sorts of offerings on display)

should there be no objections before 5pm GMT-4 today, 21.july.2008, i'll make the change. Quaeler (talk) 15:21, 21 July 2008 (UTC)

Arbitrary inclusion and deletion of links and references

I inserted an additional reference to a book, and an external link. A contributor named Quaeler deems that this is promotional and deleted these references. I most definitely am not promoting material, and what I will say here should confirm that. If there is to be material presented in Wiki, I want to see a fair representation of material.

Book references

If there is a list of books that explain and/or discuss Gödel’s theorem, there should be no self-styled arbiter of which books are included and which are not. To include some and not others is a completely subjective decision. For example, Quaeler allows the Wiki article to reference Douglas Hofstadter’s “Gödel, Escher, Bach”, a book which includes fictional characters and storylines as well as an explanation of Gödel’s proof. I included a reference to a recently published book, James R Meyer’s “The Shackles of Conviction”, which also has fictional characters and storyline as well as an explanation of Gödel’s proof. Quaeler instantly deleted it from the list.

So where’s the logic in including one and not the other? By deleting a reference, you ARE, ipso facto, promoting those that are left, and giving a spurious implication that those that are left in Wiki are the only ones that contain any useful information for the reader.

Among the books referenced is: Stanley Jaki, The drama of the quantities, with a link to http://www.realviewbooks.com/ a site unashamedly promotional, devoted to selling its books. I can find no information at all about this book . It doesn’t even seem to be in print – why is this in the list?

And if anyone thinks that a link to James R Meyer’s book is promotional, what on earth is Peter Smith’s An Introduction to Gödel's Theorems doing in the list? The given link is http://www.godelbook.net, a site that is devoted only to the promotion of the book.

And there is Rudy Rucker, Infinity and the Mind, a book where only a minor part of the book is about Gödel theorem – why is this included? And Hao Wang’s A Logical Journey: From Gödel to Philosophy covers much material, but gives very little concrete information about Gödel’s Incompleteness theorems and I see no reason why it should be in the list. Similarly, Raymond Smullyan’s Diagonalization and Self-Reference is not a book about Gödel’s theorem, covering a range of other subjects. There is no reason to include it in the list.

In view of the above, I propose to delete all book references, and the miscellaneous references (since these are actually book references).

External links

If there is a list of links that explain/discuss Gödel’s theorem, who is to decide which links are included an which are not? I included a link to Meyer’s website What is Gödel's Incompleteness Theorem?which discuses Gödel’s proof, and there is paper on the site which gives a detailed breakdown of the principal part of Gödel’s proof (Incidentally, I happen to believe that James R Meyer’s contribution is the most significant advance in our understanding of Gödel’s proof since it was published).

Quaeler deleted this link but left Dale Myer’s link intact. Dale Myer’s link is supposedly to a proof of Gödel’s theorem, but it has more to do with Tarski's Undefinability of Truth than it has to do with Gödel’s theorem, it is simplistic and adds no understanding of Gödel’s theorem for the reader. Although it is entitled Godel's Incompleteness Theorem, it actually covers a range of other material. There are hundreds of such sites on the web – why should Dale Myer’s be included here and not James R Meyer’s, not to mention all the others?

Therefore I propose to delete the external link to Dale Myer’s page.

Comments please

Third Merlin (talk) 20:17, 22 July 2008 (UTC)

I have no love for the particular link, it exists as it was pre-existing, and was the least commercial of the pre-existing. The James R Meyer site, though, is not only shilling for his book, but until his recent revision of the site, had a banner subtext which highlighted a megalomaniacal crackpot stance which advertised that he was likely the only person in the world who understood this theorem (his 'about' page still rambles in such a manner - i uploaded a screenshot for posterity); so the shilling, and the crack pot attitude, are both terribly good reasons to avoid this link. If you wish to delete Dale Myer's link out of some petty get-even-ness for not having your site included, start by suggesting other comparable pages that we may link in its place. Quaeler (talk) 21:02, 22 July 2008 (UTC)

It may be that some of the "miscellaneous" book references really are extraneous - for example, I am a Strange Loop. But the majority of the books listed there have one or more of these properties:

• The book is published by a well respected scientific publisher, such as A.K. Peters, Oxford press, etc.
• The book is reviewed in either MathSciNet or Zentralblatt MATH - a sign of external recognition of scholarly interest in the work.
• The author of the book is explicitly mentioned in our article - the book may be of interest to readers who want to pursue that mention further.

So there are several ways in which the book you are interested in, [3], differs from the books already included.

I also think the resource at [4] should not be linked from this article. Anyone is free to develop an argument against Goedel's theorem and seek its publication in a mathematical journal. But unpublished (or self-published) arguments against Goedel's theorem aren't suitable for inclusion here, especially because of the widespread acceptance of Goedel's work in the contemporary mathematical logic community. — Carl (CBM · talk) 21:08, 22 July 2008 (UTC)

First, every author is responsible for applying the acid test: Was the book was consulted during the writing of (a section of) the article and/or did it in any way influence the (section of the) article (even indirectly in the opinion of the author); if so then it must be on the list. Secondly, all directly- and indirectly-quoted sources should be referenced in full. Thirdly, the above is why I encourage (and use)annotated bibliographic references. When confronting a bibliography, the interested reader wonders, what here is appropriate for my experience (level of understanding) and interests? Or in other words: "Why and for whom is this book on the list?" For example the tiny [fictional] synopsis, "Although the book -- geared to undergraduates and interested non-specialists -- primarily concerns the origin of modern mathematical logic, Chapters 4 and 5 contains an elementary introduction to the theorems" might be of use to the newbie reader. Whereas: "Abstract. A dense thicket of proofs. Primarily useful for graduate mathematics students and specialists. Some premises have been challenged in recent publications" immediately warns off the newbie but provides cautionary guidance for the expert. Bill Wvbailey (talk) 21:11, 22 July 2008 (UTC)

The main difficulty with these is that they are just the opinion of the WP editors. I don't mind sorting into undergraduate/graduate/historical, which will be pretty uncontroversial. But I don't like writing our own descriptions of the references, as it isn't our role here. — Carl (CBM · talk) 21:17, 22 July 2008 (UTC)

Oooh, i'd suggest though that back in the days before on-demand-book-publishing, and xxx archiv, that there was a very valid mechanism in place involving peer review and well respected publishing channels. I wouldn't go so far as to say that agreeing with these practices as a standards bar for reference is writing our own descriptions of references. (Unless i'm misreading you).. Quaeler (talk) 21:47, 22 July 2008 (UTC)

Would it be too much to ask for logical appraisals rather than resorting to emotional tirades and personal attacks? Meyer well may be an egotist, but that of itself does not establish that he is delusional or that he is a crank or crackpot. If a contributor wants to show that someone is a crank or a crackpot, the normal method would be to demonstrate the errors in their reasoning.

Anyway, regarding the inclusion/exclusion of links and lists of books, I have been researching the Wiki guidelines. Lists such as lists of books are actually contrary to Wikipedia’s stated policy, see What Wikipedia is not. From this it seems that Wiki is intended to be a source of information, not a jumping board for the purposes of redirecting the reader elsewhere. See Wikipedia in brief: “Wikipedia aims to be a neutral compilation of verifiable, established facts.”

If a list of books about Gödel’s theorem could be justified, then the facts that there are books about Gödel’s theorem would have to be a neutral compilation of such facts, not a list of books that someone simply deems to be the ‘best books’ or the books that most support a certain viewpoint. The fact that a book has been published by a certain publisher, has been reviewed in a certain journal, etc is irrelevant.

If the reader wants to find information on books about Gödel’s theorem, he is free to use search engines for this purpose. Of course a reference to a book may be included if it is actually required to verify information in the article – this, of course, means that one should look out for articles that have been worded simply so that a contributor can surreptitiously add an unnecessary reference to a book.

So I still maintain that this partial list of books on Gödel’s theorem is, as well as being a biased selective listing of such books, is contrary to Wiki policy, and the list should be removed. Third Merlin (talk) 21:28, 2 August 2008 (UTC)

It seems like the section following this has agreement on removing Myer's link as of 2 weeks ago.. unless i'm missing some item of continued contention.. ? Quaeler (talk) 21:44, 2 August 2008 (UTC)

It certainly doesn't violate policy to give a list of good references in the references section. It only stands to reason that editorial judgment is required in choosing which books to list as references. — Carl (CBM · talk) 23:30, 2 August 2008 (UTC)

remove Myers external link?

I agree with Quaeler's idea that we should prune the external links very severely. He left the link to Myers' site, but I have to ask why we need that kind of link at all. We provide numerous very good references in the reference section - do we need to also link to a web page that sketches the argument? My general opinion is to leave just the Stanford encyclopedia link and the MacTutor link. — Carl (CBM · talk) 21:17, 22 July 2008 (UTC)

Ya, i concur. Quaeler (talk) 21:48, 22 July 2008 (UTC)

I removed the Myers link. — Carl (CBM · talk) 23:33, 2 August 2008 (UTC)