Talk:Gödel's incompleteness theorems/Arguments

This page is for arguments over the validity of Gödel's incompleteness theorems. This is not an archive; you may feel free to edit this page. Please use this page for comments not directly relevant to improving the article Gödel's incompleteness theorems.

Wikipedia article Incompleteness theorems is not encyclopedic

I was disappointed when I looked up the Wikipedia article Incompleteness theorems. At the very least, I expected a treatment in terms of Provability Logic as well a more modern results. The current article should be converted into a history article. 63.249.116.52 (talk) 22:31, 2 January 2011 (UTC)

There is probably space for a more abstract treatment in terms of Löb's theorem, yes. That's an advanced topic, though; I wouldn't lead with it. --Trovatore (talk) 22:44, 2 January 2011 (UTC)

I think the problem must be the deification of Gödel. — Carl (CBM · talk) 23:06, 2 January 2011 (UTC)

There is no doubt that the current Wikipedia article Incompleteness theorem is obsolete and lacks rigour. As for the deification of Goedel, Max Planck once said "Science makes progress one funeral at at time!". 70.137.165.34 (talk) 21:29, 3 January 2011 (UTC)

What is amazing about the deification of Gödel is how long it took for recognition to spread that the emperor had no clothes: proof of incompleteness leads to inconsistency. 63.249.91.253 (talk) 05:13, 4 January 2011 (UTC)

In the end, an article on Gödel's incompleteness theorems is always going to be somewhat historical. As the title says, the article is about Gödel's incompleteness theorems. By the time that we talk about these theorems, their hypotheses, their proofs, and their common interpretations, we have a reasonably complete introduction. Indeed, that content is all that you find in many textbooks. The things in the "see also" section could certainly be put into the article, but as secondary topics rather than principal ones. — Carl (CBM · talk) 23:18, 2 January 2011 (UTC)

Computer scientists no longer accept deification of Gödel by the classical logicians. So it's time to create a separate top level article on Incompleteness theorem that does not automatically redirect to this one. The current article could provide the beginning of a derivative historical article of the new one. 64.134.224.220 (talk) 05:56, 18 January 2011 (UTC)

The incompleteness theorems are a topic of mathematical logic. The incompleteness theorems are only related to computer science in a very distant sense, e.g. by going first to theoretical computer science, then to recursion theory, then to the incompleteness theorems. Computer scientists, by and large, don't do anything related to the incompleteness theorems.

In particular, Carl Hewitt's research and opinions, while very interesting, can hardly be claimed to be reflective of the interests and opinions of all computer scientists. This article gives appropriate weight to Hewitt's work by mentioning it briefly. — Carl (CBM · talk) 12:53, 18 January 2011 (UTC)

The incompleteness theorem and consequent inconsistency are a direct consequence of the computer science need for powerful reasoning systems. The reason that computer science needs powerful reasoning systems is so that the arguments will be shorter than they would be with less powerful systems. Computer science did not take the indirect path imagined by User:CBM.

This summer at Stanford there will be an international symposium with a very prestigious program committee (Hewitt is chair) that addresses these issues. See Inconsistency Robustness 2011. Because of his philosophical attachment to classical logic, User:CBM is intent on minimizing and diminishing the work in computer science. 64.134.233.83 (talk) 17:29, 18 January 2011 (UTC)

Please refrain from personal attacks. Note that an "international symposium with a very prestigious program committee" has been held at Stanford every summer according to information provided on this very talkpage. When will something finally appear in a peer-reviewed periodical? At that stage it will be easier to incorporate this material into wiki, perhaps as a separate page on paraconsistent logics and applications in computer science. Tkuvho (talk) 17:38, 18 January 2011 (UTC)

According to the call, Inconsistency Robustness 2011 is the first such symposium. Computer science is moving much faster than peer reviewed journals can keep up. So computer scientists are now publishing in electronic journals like ArXiv and even on Google Knol. Elsewhere, in Wikipedia references are allowed to ArXiv, blogs, and news articles. That they are not allowed here is purely due to prejudice.64.134.233.83 (talk) 18:04, 18 January 2011 (UTC)

I would like to add to the title of this "Arguments" section, under this chapter title. That the standing on truth is lacking and that an abuse of the word "proof" may here, therefore, be displayed. The article can very well present a better "Criticism" section, in my opinion, even though the introduction nicely says "The two results are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible, giving a negative answer to Hilbert's second problem." Merry Christmas! 109.189.87.14 (talk) 18:11, 23 December 2012 (UTC)

The Two Last Sections of the Gödel Paper, Sections 3 and 4 - Copy-and-Paste-Ready

I'd like to inform you that the two sections of 3 and 4 missing in Hirzel's paper are now copy and paste ready for people who are interested in translating it completely. It can be found here, avoiding the difficulties in moving text from the original pdf-document to a translation-ready document: http://whatiswritten777.blogspot.no/2012/09/a-part-of-godels-paper-on-two.html . Cheers! 46.9.87.116 (talk) 03:35, 11 January 2013 (UTC)

What exactly does "True and unprovable" mean?

I have a slight problem with the word "true" in this description. Isn't it better to simply skip this word "true" and to write "there are statements expressible in its language that are neither provable nor disprovable" ? The current formulation seems to contradict Gödels completeness theorem. 147.231.6.9 (talk) 10:57, 9 April 2013 (UTC)

Skipping the word "true" isn't better, because the fact that the Gödel sentence is both true and unprovable is a key point (false unprovable statements are much less interesting...). Moreover, if we did not say which one was true, people would ask whether Gödel sentence or its negation is true. The footnote in the article gives a good explanation of exactly what "true" means. The completeness theorem is not about true sentences, however, it is about logically valid sentences. Not all true sentences are logically valid; the incompleteness theorem is one way to see that fact. — Carl (CBM · talk) 11:51, 9 April 2013 (UTC)

Well, as I understand it, there exists a sentence phi such that there exists a model of the Theory in which phi is true, as well as a model in which phi is not true. In other words, if you add the negation of phi as a new axiom, the theory is still consistent. So, it is very confusing to say that it is "true". Even the remark is confusing, because it deals with a "metalanguage-interpretation of the sentence" (or how to say it..), but the sentence itself is still just some complicated first-order sentence. Or am I wrong? Thanks for the feedback. Franp9am (talk) 15:08, 9 April 2013 (UTC)

The sentence itself is a complicated first-order sentence, that happens to be true. It asserts that there is no natural number having a certain property, and in actual fact, no natural number has that property. --Trovatore (talk) 15:27, 9 April 2013 (UTC)

In which theory? In which model? As I said before, there are models where some number actually has that property. You can only speak about "truthness" in some model, or in each model. I really think that you are wrong here... Franp9am (talk) 15:37, 9 April 2013 (UTC)

P.S. maybe you think that it is true in the standard model of natural numbers in ZFC, is this what you mean by "true"? If yes, it should be said more clearly in the article.. Franp9am (talk) 15:39, 9 April 2013 (UTC)

Exactly - one property of arithmetic is that there is a particular distinguished standard model in addition to many nonstandard models. "True" means "true in the standard model" - in other words, true as a statement about the actual set of natural numbers with their usual operations.

Back up for a second, though. In the hypothesis of the incompleteness theorem, there is an assumption that the theory is consistent. In order to even read the theorem you already have to be able to quantify over all proofs to express consistency. If you can quantify over all proofs, you can quantify over their lengths - which means you can quantify over natural numbers. Then the Gödel sentence is "true" in exactly the same sense that "the theory is consistent" is true. This is what "disquotational truth" means - that the Gödel sentence of a theory is true in exactly the same sense that the hypotheses are true as statements about that theory. People who are comfortable talking about the standard model realize this is the same as "true in the standard model". — Carl (CBM · talk) 15:50, 9 April 2013 (UTC)

Ok, now I see what you mean. However, I believe that wikipedia should be readable not only for experts in one field, but even for people with some mathematical education, like me. Do you think that it would be ok to add everywhere where the "true" concept is mentioned, something like "true in the standard model"? The current formulation really seems to contradict the completeness theorem.. Franp9am (talk) 15:59, 9 April 2013 (UTC)

I would be happy to add the words "standard model" to the footnote, but I would wait a little while to see if anyone else objects. Some people manage to be comfortable saying "disquotational truth" without being comfortable with the term "standard model". I think that is why the article is phrased the way it is. — Carl (CBM · talk) 16:02, 9 April 2013 (UTC)

Ok, let's see what other people think about this. I personally find it quite fascinating that "truth" and "provability" are so closely connected, therefore I objected. I added a new section for this part of the conversation, I hope it is ok. Franp9am (talk) 16:06, 9 April 2013 (UTC)

Carl, with your permission, I will present a less technical answer that may not be entirely right but hopefully helpful. Namely, a fairly high percentage of mathematicians tend to hold Platonist views, at least about the natural numbers. For this reason, it is "safer" to describe statements about N as either true or false. Meanwhile, certain logical systems allow you to prove a certain proper subcollection of the true statements. While set theorists like Kunen tend to formulate Goedel's result in terms suggested by User:Franp9am, it is often safer to formulate them in terms currently dominant in this page. Tkuvho (talk) 16:54, 9 April 2013 (UTC)

Does the notion of standard model of arithmetic have a definition? If so, then the notion of truth in the standard model might be intelligible. If not, then how are we to know what is true and what is false? By relying on some Platonic insight? But then if a mathematician is not a Platonist, how does the mathematician recognise the truth? Ought there not be a better criterion than "insight"? Compulogger (talk) 08:43, 10 April 2013 (UTC)

To answer your first question: You assume ZF, and then use long strings of curly braces to define N. That's the standard model. Here truth is intelligible until you ask whether Cons(ZF) is true. From them on, it's infinite regress. Tkuvho (talk) 10:42, 10 April 2013 (UTC)

To know that the original theory is consistent, you have to be able to quantify over proofs in the theory and recognize that none of them proves 0=1. But then, to know that the Gödel sentence for the theory is true, you only have to recognize that the Gödel sentence is unprovable in the theory, which again only requires you to be able to quantify over proofs in the theory. So the truth of the Gödel sentence is no more or less intelligible than the truth of the hypotheses. However, people who recognize the standard model will also recognize that saying "the Gödel sentence is disquotationally true" has the same meaning as saying "the Gödel sentence is satisfied by the standard model of arithmetic". — Carl (CBM · talk) 11:39, 10 April 2013 (UTC)

I would be gratefull if you add a few very short remarks "true in the standard model of N", resp. "true in the standard model of N in ZFC" or so. "Disquotationally" is a quite complicated concept (though I don't want to remove it) that is, at least in my opinion, not sufficient to clerify it to most readers. If you even add some of the remarks that you wrote here, Carl, it would be definitely better (if you have time for this, of course).. Thx Franp9am (talk) 13:09, 10 April 2013 (UTC)

No, that would be completely wrong. It's a category error to say "true in the standard model in ZFC". It sounds like you're using "true" to mean "provable". But the most important takeaway from the Goedel theorems is precisely that provability is not strong enough to capture truth. --Trovatore (talk) 22:51, 10 April 2013 (UTC)

I think that's a little strong. "True in a model" is not the same as "true", but the standard model is a model and "true in the standard model" is a perfectly reasonable notion. — Carl (CBM · talk) 01:40, 11 April 2013 (UTC)

It's a perfectly reasonable notion; the problem is the addition of "in ZFC", which makes it appear that he's still identifying truth with provability, just provability in ZFC instead of in the object theory. --Trovatore (talk) 01:51, 11 April 2013 (UTC)

(Not that that's the only problem — the other problem is that bringing up the standard model, as far as I can see, only serves to add confusion to something that is really very simple.) --Trovatore (talk) 01:52, 11 April 2013 (UTC)

Just defining what is a number in ZF doesn't define addition and multiplication. I don't see how ZF helps with this. If anything it just gets in the way.

By the way, Davis, M. (1980). The mathematics of non-monotonic reasoning. Artificial Intelligence, 13(1), 73-80 presents a first-order theory which has a unique minimal model, which is, as he says, "the standard model of arithmetic". What's wrong with understanding this as a "definition" of the standard model? At least it's intelligible. Compulogger (talk) 13:55, 10 April 2013 (UTC)

Defining addition and multiplication of natural numbers in ZFC is easy. However, with or without ZFC; I just want to say that the word "standard" should appear somewhere. Franp9am (talk) 14:06, 10 April 2013 (UTC)

ZFC is a red herring, and the word "standard" is unnecessary weaseling. If T is consistent, then its Goedel sentence is true, period. There is no need to qualify or soften the word. --Trovatore (talk) 00:32, 11 April 2013 (UTC)

So, what do you mean by "true" if not "true in the standard model"? Franp9am (talk) 08:39, 11 April 2013 (UTC)

Given a formal theory T, its Goedel sentence, G_T, says that there is no natural number n with a certain property P(n). The property P is one that can be checked by a fixed computer program, one we can actually work out, and one that is guaranteed to terminate in an amount of time we can calculate in advance, given n.

Now, if T is consistent, then G_T is true. What does that mean? It means that no natural number has property P. What does that mean? It means that P(0) is false (that is, if you give 0 as an input to the program, it will respond "false"). And that P(1) is false, P(2) is false, P(3) is false, and so on.

So that's what it means. Can you word this as "true in the standard model"? Sure, you can. It isn't wrong. But it's unnecessary, and it makes it sound complicated when it's actually simple. If T is consistent, then G_T is just plain true, which means the thing I said above, which is the obvious thing it should mean. --Trovatore (talk) 13:27, 11 April 2013 (UTC)

I agree with you on this. Also see Emil J.'s comment below. Goedel's "satisfiability" criterion (Theorem X) is an iff, i.e. a logical equivalence so it defines what is meant by "true" in this context; as noted by Nagel and Newman 1958 this bridges the expanse between an arithmetical purely-mechanical computation, and the metamathematical "true". On pages 79 and 80 they state it this way: "We now ask the reader to observe that a meta-mathematical statement which says that a certain sequence of formulas is a proof for a given formula is true, if and only if, the Godel number of the alleged proof stands to the Goedel number of the conclusion in the arithmetical relation here designated by 'Dem'. Accordingly, to establish the truth or falsity of the meta-mathematical statement under discussion, we need concern ourselves only with the question whether the relation Dem holds between two numbers. Conversely, we can establish that the arithmetical elation holds between a pair of numbers by showing that meta-mathematical statement mirroed by this elation between the number is true". On page 91 a footnote describes pretty much what Trovatore wrote above about testing property P. Bill Wvbailey (talk) 14:41, 11 April 2013 (UTC)

But G_T can be chosen to be Cons(T) itself! So what you are claiming is that the sentence "Cons(T) implies Cons(T)" is just plain true. I would agree with that. Tkuvho (talk) 13:41, 11 April 2013 (UTC)

It seems to me that you are trying to prove from first principles that the Platonist view is better than the Pragmatic view (see my comments below). Perhaps we can try to avoid philosophical commitments altogether. Tkuvho (talk) 13:42, 11 April 2013 (UTC)

What I am doing is pointing out that it is very simple. I am deflating, if you like. What does it mean to say the Goedel sentence is true? The Goedel sentence says that no natural number has a certain property. Saying that it's true says only that no natural number really has that property. The only way that can be wrong is if some natural number does have that property, and if that were true, then by the arguments used to prove the theorems, from that number, you could recover a proof of a contradiction in T. There is really no way around this. --Trovatore (talk) 13:51, 11 April 2013 (UTC)

OK, well, perhaps the Platonist view is provably superior to the Pragmatic one, but perhaps User:Franp9am and I can still raise the issue whether Kunen's Pragmatic formulation can be mentioned in a subsection (perhaps subsubsection) toward the end of the article? Tkuvho (talk) 14:04, 11 April 2013 (UTC)

You keep trying to un-deflate. There is no need to talk about Platonists or pragmatists. The formulation I gave works for everybody. --Trovatore (talk) 14:07, 11 April 2013 (UTC)

Are we to assume that Kunen is provably wrong? Tkuvho (talk) 14:16, 11 April 2013 (UTC)

I am saying Kunen would agree with me. --Trovatore (talk) 15:13, 11 April 2013 (UTC)

But Kunen is the one who gave a non-Platonist formulation of Goedel's theorem on page 38 of his book Kunen, K.: Set theory. An introduction to independence proofs. Studies in Logic and the Foundations of Mathematics, 102. North-Holland Publishing Co., Amsterdam-New York, 1980. Do you think he changed his mind after reading your post? Tkuvho (talk) 15:20, 11 April 2013 (UTC)

Ah, found my copy (had to dig a little — had to box up some books a while back). I see nothing on page 38 that is in any way incompatible with what I say above. --Trovatore (talk) 16:11, 11 April 2013 (UTC)

I wonder if we are looking at the same edition. In my edition, Kunen certainly does not formulate the result as asserting that there are propositions that are true but not provable, which is the formulation you appear to favor. Tkuvho (talk) 16:17, 11 April 2013 (UTC)

He omits to discuss the truth of the proposition. It's an enormous leap to conclude he has no opinion about it, and an even bigger one to conclude that he would actively disagree with what I've said. If that's all you're going on, that's an awfully thin reed. --Trovatore (talk) 16:23, 11 April 2013 (UTC)

Again, what I am "going on" is not to disagree with what you've said (as I already mentioned we are not going to resolve the Platonist-Pragmatic discrepancies from "first principles"), but merely to see if editors support the inclusion of Kunen's type of formulation of the incompleteness result. To the extent that he does not formulate it in the way it is currently formulated in the article, the inclusion of a Kunen-type formulation may be justified on the grounds of notability. In other words, I am recommending a mitigation of an "all-or-nothing" attitude. Tkuvho (talk) 16:31, 11 April 2013 (UTC)

That does not require any change at all, as far as I can see. Kunen says that the Goedel sentence can neither be proved nor disproved from T, assuming T is consistent. We say that as well, I think (right?). We also provide the extra information that the sentence, understood as a sentence of arithmetic rather than necessarily as one talking about the objects of discourse of T, is true. --Trovatore (talk) 16:34, 11 April 2013 (UTC)

I just looked through the article again. The first three formulations I found all insist on "true but not provable" aspect. If it's there, you would need a microscope to find it. Also, Kunen prefaces the "true but not provable" comment by explicitly referring to a Platonist interpretation, which suggests that it is not the only one. I would propose creating a subsection where a non-Platonist formulation is clearly stated without the terminology "true but unprovable". Tkuvho (talk) 16:50, 11 April 2013 (UTC)

It is certainly true that the information that the sentence cannot be disproved by the theory is also important. Perhaps we should say "true but not provable (and also not disprovable)" or some such. --Trovatore (talk) 16:54, 11 April 2013 (UTC)

Sorry to belabor the point, but Kunen does not say that. You keep trying to get to the bottom of the "truth of the matter", whereas I keep trying to insist on sourceability. Tkuvho (talk) 16:57, 11 April 2013 (UTC)

It is sourceable, and well-sourced. It's not sourced to Kunen. Kunen says less; he doesn't in any way say anything that contradicts what we have. --Trovatore (talk) 16:59, 11 April 2013 (UTC)

Kunen certainly does not contradict the Platonist formulation, because it is not something that can be refuted mathematically. He does provide an alternative formulation, which is therefore sourceable, and yet not represented in our article. Tkuvho (talk) 17:09, 11 April 2013 (UTC)

So what do you want to write? "Some sources say A and also B, and some other sources say A but don't mention B (but also don't say anything contrary to B; they just don't mention it)"? What's the value in that? --Trovatore (talk) 17:12, 11 April 2013 (UTC)

No, I would suggest reproducing Kunen's "Pragmatic" formulation, which does not make Platonist assumptions, to complement the current formulation. There is no end to discussions at mathexchange, stackoverflow, and the like :-) pitting Platonist and Pragmatic viewpoints, with no clear consensus in sight. Similarly, as was already pointed out by User:Franp9am, other wikis follow Kunen's formulation and not ours. He checked it for the German wiki, and I obtained the same result for the French wiki. This in itself is not conclusive, but it is hard to understand why our page should be dominated by the Platonist formulation when there is a variety of views out there. Tkuvho (talk) 11:51, 15 April 2013 (UTC)

Kunen's formulation is a subset of ours (or, at least, of what ours probably should be). If you want to leave a part of it out, you should have a source that makes a point of leaving it out. There is no direct evidence that Kunen even disagrees with what you're calling the "Platonist" formulation (it doesn't even have to be Platonist, as explained by the footnote), and I would suggest that he almost certainly does agree with it — it just wasn't important to mention it at that point in the book. --Trovatore (talk) 18:05, 15 April 2013 (UTC)

Perhaps I can try to elaborate on the point about Platonism that I already made earlier. If the natural numbers N are assumed to be just "there", then it does not make sense to talk about "standard models", and assertions about N are either true or false, period. I don't think one could resolve this issue from "first principles", without recognizing that there are differing philosophies underlying the divergent views. From a Pragmatic viewpoint, one could see difficulties with the Platonist view. If N is "just there", with the implied background of naive set theory, then so is its field of fractions Q, as well as its completion by Dedekind cuts, namely R. But then questions such as "Does R contain a subset of strictly intermediate cardinality between N and R" should have a determinate answer. This seems to be at tension with Cohen's work on the CH. There are certainly responses to this, but my main point is not to resolve this century-old dispute. Rather, my point is to suggest that, instead of pitting a Platonist view against a Pragmatist view, one could perhaps develop a formulation that would be acceptable to both. Tkuvho (talk) 09:08, 11 April 2013 (UTC)

Yes, I think I understand. So, could you suggest such formulation? I suggested one (to mention the word "standard" in the text, and, maybe, to explain this Platonic versus non-Platonic POV in some remark). However, I'm not sure if people agree with this; there are many theoretical discussions here but few proposals. Franp9am (talk) 10:46, 11 April 2013 (UTC)

From my previous experience arguing in favor of such a change, there appears to be little chance of getting this into the lede or anywhere near the top, but perhaps there could be a subsection near the end of the article citing, for example, Kunen's formulation which is of a Pragmatist type. Tkuvho (talk) 11:33, 11 April 2013 (UTC)

@User:Compulogger: Thanks for the Davis reference, it's a nice paper. When Davis writes on page 74 that "It is readily observed that there is a unique minimal model of $\Gamma$ namely the standard model of arithmetic (with Z(x) interpreted as 'x is zero', etc.)", he is referring to the real number "zero" in the standard model of N built in ZF. His "uniqueness" is with respect to a fixed world of ZF. Tkuvho (talk) 14:33, 10 April 2013 (UTC)

Actually, there is a simpler definition than Martin Davis', which doesn't require ZF, but uses the so-called Herbrand universe, constructed from the constant symbol 0 and the successor function symbol:

add(0,X,X)

add(s(X),Y,s(Z)) <- add(X,Y,Z)

prod(0,X,0)

prod(s(X),Y,U) <- prod(X,Y,V)& add(Y,V,U)

This set of Horn clauses has a unique minimal Herbrand model.Kowalski claims that this is the standard model of arithmetic on page 274-275 of http://www.doc.ic.ac.uk/~rak/papers/newbook.pdf

Compulogger (talk) 15:42, 10 April 2013 (UTC)

I would like to understand this "unique minimal model" better. Is it provably consistent? Tkuvho (talk) 15:50, 10 April 2013 (UTC)

I moved the following discussion to the relevant section. Sorry, my earlier mistake.Compulogger (talk) 07:24, 11 April 2013 (UTC)

Every set of definite Horn clauses (with at least one positive literal) as in this example, is itself consistent. Moreover, it has a unique minimal Herbrand model, which is the intersection of all Herbrand models. The minimal model of a set of definite Horn clauses can also be characterized in several other equivalent ways, for example as the least fixed point of the "immediate consequence" operator. These characterizations make use of a variant of the Skolem-Lowenheim-Herbrand theorem, which says that if a set of clauses has a model, then it has a Herbrand model, i.e. a model consisting of the set of all atomic sentences (constructed from the variable-free terms of the language) that are true in the model. These are standard notions in logic programming.Compulogger (talk) 17:07, 10 April 2013 (UTC)

I fail to see how this is supposed to be easier than a direct definition. It boils down to exactly the same construction as if you used integers directly, except that it carries along a huge baggage of the general theory of Horn theories that you need to develop first. In any case, this just defines the model as an algebraic structure, it does not help the least bit with constructing the satisfaction predicate for first-order formulas, which is needed to explicate what is meant by true.—Emil J. 17:31, 10 April 2013 (UTC)

Maybe it's easier to understand definite Horn clause as monotonic inductive definitions, using the standard notion of inductive definition. The relations so defined are a Herbrand model of the clauses (the minimal model). There is no more baggage here than there is in defining the notion of the extension of a monotonic inductive definition. The definition of truth in the resulting minimal model is the standard Tarskian definition, which would be need no matter how the standard model is understood. In fact, the definition of truth for Herbrand models is actually simpler than the standard definition of truth because it does not require the use of "valuations". In any case, my point is that the standard model of arithmetic needs an explication, ideally a definition. If you can suggest a simpler one, that would be great. What did you have in mind?Compulogger (talk) 20:03, 10 April 2013 (UTC)

Let me reformulate the "definition" informally. The definition still has two parts: First there is an inductive definition of the standard model. Then the definition of truth in the standard model. Here the standard model is represented by the atomic sentences that are true in the standard model. (This is what is meant by a Herbrand interpretation.)

The domain of the standard model is the set {0, s(0), s(s(0)),...},

i.e. the smallest set containing 0 and s(t) whenever it contains t.

There are two relations in the standard model,

add(t,u,v), standing for t plus u = v, and

prod(t,u,v), standing for t times u = v.

The standard model S of arithmetic is the smallest set containing the atomic sentences

add(0,t,t) for all t in the domain

prod(0,t,0) for all t in the domain

add(s(t),u,s(v)) whenever it contains add(t,u,v)

prod(s(t),u,v) whenever it contains prod(t,u,w) and add(u,w,v) for some w.

Now for the definition of truth:

An atomic sentence s is true in S iff s is in S.

A universally quantified sentence forall X s(X) is true in S iff s(t) is true in S for all t in the domain.

The negation not s of a sentence is true in S iff s is not true in S.

etc., as in standard Tarskian model theory. Compulogger (talk) 08:04, 11 April 2013 (UTC)

I added a the string

However, the arithmetic statement in question is false in some nonstandard models of arithmetics

into the "remark", explaining the meaning of truth in the first incompletenss sentence. I hope that this is ok. I didn't want to start a long dispute; I was just confused when reading this first time. I checked the article on german wikipedia, and the concept of "truthness" is not mentioned there at all. I checked 4 or 5 books on mathematical logic and in most of them, this theorem is formulated only in terms of incompleteness (although I also have seen this "platonic" remark somewhere). I still believe that the current formulations are not very good, because I got to understand the meaning only after reading this discussion. For a reader that is not an expert, just wants to read something about Godel's Theorems and starts with the Completeness Theorem and then reads this, it must seem contradictory. However, I don't have the courage to do larger changes now. Franp9am (talk) 20:15, 11 April 2013 (UTC)

That seems OK, I guess. Should be "arithmetic" rather than "arithmetics", though. --Trovatore (talk) 20:57, 11 April 2013 (UTC)

The above discussion is confused because of the mistake of focusing attention on cut-down first-order theories, which cannot even prove that there are no infinite elements in a model. Using the method developed by Church and Turing, it is easy to show that there is a proposition that is neither true nor false in the standard model.64.134.238.90 (talk) 21:55, 11 April 2013 (UTC)

No, every proposition in the language of arithmetic is either true or false in the standard model. --Trovatore (talk) 22:04, 11 April 2013 (UTC)o

In more-powerful systems than first-order, it can be the case that a proposition is true if and only if it is provable, i.e., satisfaction in the standard model is the same as provability.64.134.238.90 (talk) 22:16, 11 April 2013 (UTC)

Yes, if you identify provability with, say, second-order logical implication (though Carl apparently holds that that's a nonstandard usage), then truth is the same as that sort of provability. But the Goedel theorems don't apply to that sort of provability, so it doesn't follow that there's a sentence that can neither be proved nor disproved in that sense. --Trovatore (talk) 23:21, 11 April 2013 (UTC)

That proofs are recursively enumerable is a proposition in the meta-theory. Church and Turing proved that there is a sentence that is neither proved nor disproved (lest provability be computationally decidable). However, Goedel's Second Incompleteness result is false.64.134.238.90 (talk) 00:02, 12 April 2013 (UTC)

No, sorry. First-order proofs are r.e., yes. Second-order logical consequence is not. The Goedel theorems don't apply. --Trovatore (talk) 00:04, 12 April 2013 (UTC)

Of course, proofs in second-order Peano number theory are recursively enumerable and consequently so are the theorems. What do you think that it means to be a theorem of second-order Peano number theory? Perhaps you meant say that the true sentences of second-order Peano number theory cannot be recursively enumerated?50.131.244.2 (talk) 20:46, 13 April 2013 (UTC)

Ah, you may have missed the context (I'm assuming you're a different person from 64.134). Certainly, proofs in second-order arithmetic are r.e. But second-order arithmetic, despite the name, is a first-order theory (that is, it uses first-order logic. The Goedel theorems do apply, but they do not imply what 64 claimed.

There is a collection of axioms in the second-order language of arithmetic that completely determine the model up to isomorphism, and therefore completely determine truth in the standard model, when using second-order logic. That's what I assume 64 was talking about. But these second-order logical implications are not r.e., and the Goedel theorems do not apply. --Trovatore (talk) 21:17, 13 April 2013 (UTC)

So theorems of the second-order Peano theory are recursively enumerable and furthermore the second-order theory proves that all structures that satisfy the axioms of the theory are isomorphic. Also, by the argument of Church and Turing, there is a formula that can neither be proved or disproved in the second-order theory because otherwise provability in the second-order theory is computationally decidable. On the other hand, the second-order theory self proves its own consistency.64.134.224.132 (talk) 00:04, 16 April 2013 (UTC)

No. You're confusing the two senses of "second-order" here. There is a theory called second-order Peano arithmetic whose theorems are r.e., but this theory is actually a first-order theory (meaning that it is to be interpreted in first-order logic). It does not determine its models up to isomorphism.

On the other hand, there is a theory of second-order arithmetic that, when interpreted in second-order logic, does indeed characterize its models up to isomorphism. However, logical consequence in second-order logic is not recursively enumerable. So your conclusion that there is a proposition that is "neither true nor false" fails. --Trovatore (talk) 00:24, 16 April 2013 (UTC)

Of course, the second-order Peano theory is in no way first-order and its proofs and consequently its theorems are recursively enumerable. Are you familiar with the second-order induction axiom? What do you think that it means to be a theorem of the second-order theory using the second-order induction axiom? And the second-order theory famously proves that all structures that satisfy its axioms are isomorphic.64.134.224.132 (talk) 00:46, 16 April 2013 (UTC)

Look, you've just misunderstood this. I've tried to explain it to you but you won't listen. Go ask your professor to go over it again. --Trovatore (talk) 00:55, 16 April 2013 (UTC)

I discussed the above with my professor at Stanford. He said that I am technically correct in my comments, but this is an area of cutting-edge research and very controversial. Some professors and graduate students working on logic in computer science fundamentally disagree with some professors in the philosophy department. Professors in CSLI are sitting on the fence waiting for the dust to settle! 64.134.224.132 (talk) 01:03, 16 April 2013 (UTC)

Ah, now I understand who you are. You got me again. Good one. --Trovatore (talk) 06:11, 16 April 2013 (UTC)

I would like to learn more about the controversy. Were there any articles discussed in class? — Preceding unsigned comment added by 63.249.97.145 (talk) 03:18, 16 April 2013 (UTC)

There is no controversy. --Trovatore (talk) 06:11, 16 April 2013 (UTC)

Another student told you the arguments being debated here and you just blew them off. Everyone knows about the controversy. Why the dogmatism and pretence? 70.137.139.15 (talk) 17:06, 16 April 2013 (UTC)

Philosophers are very keen on inventing controversies about the usage and merits of second-order logic, but that’s completely besides the point here. There’s no controversy about whether and how Gödel’s theorems are applicable to second-order systems, there’s just a confusion of two terms. A confusion is not a controversy.—Emil J. 17:26, 16 April 2013 (UTC)

Funny thing is that the logic philosophers here are very conservative and not keen on inventing controversies about second-order logic. It's some computer scientists who are keen on second-order logic in order to overcome the very significant limitations of first-order logic. But second-order logic is very different with respect to Gödel’s results:

1. There is a proposition that can neither be proved nor disproved in the second-order theory.
2. Consistency can be proved using a simple proof by contradiction.

Around here, 1.) is uncontroversial but 2.) is very controversial. 64.134.228.109 (talk) 21:10, 16 April 2013 (UTC)

historical context

I'm going out on a limb here and present a historical context RE what Goedel meant by "true", "provable" and "formal system". Observe that it has nothing whatever to do with ZFC, except that ZFC is one of many "formal systems"; in fact his standard model appears to be "arithmetic" computed by Turing machine:

I remember [altho I now think my memory was planted there by space aliens] challenging Trovatore [and/or Carl] to find the word "true" in Goedel’s 1931 and indeed [this was confirmed . . . at least this is how I remember the dialog going, caution: aliens at work. Indeed] much to my chagrin [the world "true" does appear] in at least three places (cf van Heijoort p. 598, 599 (twice), 612). There are two places of particular interest: (1)In the intro (page 599), Goedel says outright that he's going to "replace the second of the assumptions" -- this being "that every provable formula is true in the interpretaton considered" -- "by a purely formal and much weaker one", and then where he actually does this: (2) Theorem X where Goedel asserts that:

"Theorem X. Every problem of the form (x)F(x ) (with recursive F) can be reduced to the question whether a certain formula of the restricted functional calculus is satisfiable (that is, for every recursive F we can find a formula of the restricted functional calculus that is satisfiable if and only if (x)F(x) is true." (cf van Heijenoort p. 612)

So I wondered what kind of "true" this was and Trovatore assured me it means true. So what is this true, what does it mean -- as a philosopher I know precisely what it means to me, but what did it mean to Goedel? Although reputed to be a Platonist, we know that the young, tentative Goedel at the time (1931) was quite sensitive to Formalism and Intuitionism, indeed he states in a discussion of Theorem VI that it is “constructive . . . [that it] has been proved in an intuitionistically unobjectionable manner”. Back then this would mean that he can exhibit the objects that he's constructed, without use of the LoEM over the infinite, inside his formal system.

In his Princeton lectures of 1934 he uses the words "true" and "provable" freely: cf "On Undecidable Propositions of Formal Mathematical Systems" at "§7: "So we see that the class α of number of true formulas cannot be expressed by a propositional function of our system, whereas the class β of provable formulas can. Hence α ≠ β and if we assume β ⊆ α (i.e. every provable formula is true) we have β ⊂ α., i.e. there is a proposition A which is true but not provable. ~A then is not true and therefore not provable either, i.e. A is undecidable." (page 64-65) in The Undecidable.

By 1946 (cf Undecidable p. 84) he states that "with this concept [of computability by general recursion or "Turing's computability"] . . . one has for the first time succeeded in giving an absolute defintion of an interesting epistemological notion, i.e., one not depending on the formalism chosen.*" He added this footnote in ca 1965: *"To be more precise: a function of integers is computable in any formal system containing arithmetic, if and only if it is computable in arithmetic, where a function f is called computable in S if there is in S a computable term representing f"].

Furthermore, that by 1963 we know that Goedel came to accept that “due to A. M. Turing’s work a precise and unquestionably adequate definition of a formal system [Footnote here: “ . . .formal systems in the proper sense of the term, whose characteristic property is that reasoning in them, in principle can be completely replaced by mechanical devices”] can now be given . . . that is, it can be proved rigorously that in every consistent formal system that contains a certain amount of finitary number theory there exist undecideable arithmetic propositons and that, moreover, the consistency of any such system cannot be proved in the system” [Note added 28 Aug 1963 to his 1931; cf van Heijenoort p. 616].

In Vol II of Collected Works, Gregory H Moore observes: "The Platonist views put forward by Goedel in 1947 were strengthened in 1964 . . . where he described himself as "someone who considers mathematical objects to exist independently of our constructions" ". Moore then quotes from the supplement to the 2nd edition (1964) where Goedel "pursued at some length the analogy between mathematics and physical theories" in which "sense preception . . . induces us to build up physical theories and to expect that future sense perceptions will agree with them . . .." Goedel's philosophy can be found on page 268 of vol. II. It's too involved to quote in full here, but here is a snippet: "Evidently the "given" underlying mathematics is closely related to the abstract elements contained in our empirical ideas. It no means follows, however, that this data of the second kind, because they cannot be associated with actions of certain things upon our sense organs are purely subjective, as Kant asserted. Rather they, too, may represent an aspect of objective reality, but, as opposed to the sensations, their presence in us may be due to another kind of relationship between ourselves and reality." (p. 268) [emended] Bill Wvbailey (talk) 20:17, 15 April 2013 (UTC)

Just a little note: It wasn't I who did the literature search Will is talking about. I have never read Goedel's 1931 paper. My guess is, it was Carl, but I'm not sure of that either. --Trovatore (talk) 21:58, 13 April 2013 (UTC)

Actually I miswrote: it was I who followed up by finding the four places mentioned (there may be more). This is at least the third round of argument concerning this issue of "truth". There's one on 8 September 2010 that Tkuvho started off with a question about truth and numbers, then you, Carl, and I did indeed have a dialog around this issue of "truth". Then there's another long dialog on 12-16 July 2011 around challenges from editor Drgao; it's actually very interesting to read after reading the above, which is pretty much a repeat. I'm not sure how many more times we can beat Theorem X. Bill Wvbailey (talk) 20:17, 15 April 2013 (UTC)

It is well-known that Goedel was a Platonist. User:Franp9am's question concerns how this page could be presented from a non-Platonist viewpoint. Tkuvho (talk) 15:39, 10 April 2013 (UTC)

Chaitin's critique of Gödel's approach to incompleteness theorems

Gregory Chaitin [“Dangerous Knowledge” BBC4 documentary. 2007.] famously complained about the triviality of basing something as important as incompleteness on such a ridiculous solipsistic sentence saying

"[Gödel’s argument for incompleteness] was too superficial. It didn't get at the real heart of what was going on. It was more tantalizing than anything else. It was not a good reason for something so devastating and fundamental. It was too clever by half. It was too superficial. [It was based on the clever construction] “I'm unprovable.” So what? This doesn't give any insight how serious the problem is."

Carl (talk) 16:07, 23 April 2016 (UTC)

Gödel's proof is what it is. And it's correct. this is indisputable. it can clearly and unambiguously be explained and described. whether or not it's superficial or important or anything else is a matter of pure opinion. the term "incompleteness" was never even used in his paper, by the way. if someone's notion of "incompleteness" needs to be based on something other or beyond Gödel's paper, so be it. It's irrelevant.68.48.241.158 (talk) 21:54, 4 May 2016 (UTC)

No doubts about the consistency of mathematics are resolved by the proof of the formal consistency of mathematics.

As the article currently points out: No doubts about the consistency of mathematics are resolved by the proof of the formal consistency of mathematics.

As Professor Meyer pointed out in his review of Vol. 52 of Studies in Logic, the existence of such a formal proof is primarily of philosophical interest. Also, as pointed out by Meyer, the existence of a proof of formal consistency means that there is no reason to suppose that it is impossible to prove constructive consistency. Unfortunately, such a proof seems to be very difficult. Carl (talk) 16:25, 23 April 2016 (UTC)

Article does not give a precise statement of the theorem.

I am not a Wikipedia editor, so I will not correct this myself since I do not know the guidelines. However, I do have expertise in mathematical logic. Most Wikipedia articles on mathematical theorems have a section titled "precise statement" which gives an accurate statement of the theorem. This one does not. The statement of the first incompleteness theorem in the opening paragraph is fine for lay readers but is not a precise statement of the theorem for two reasons:

First, "whose theorems can be listed by an effective procedure (i.e., an algorithm)" should be replaced with "whose axioms are decidable" or "with a general recursive set of axioms." Second, "proving all truths about the arithmetic of the natural numbers" should be replaced with "proving all true statements of first order Peano arithmetic". I can basically tell what is intended by the statement that is there now, but it is too sloppy to be considered a precise statement of the theorem in my professional opinion.

I do not necessarily think the statement in the opening paragraph should be changed, but I do think a section should be added with a precise statement of the theorems, as seems to be standard Wikipedia practice.

Of course, a theory can be axiomatized with a decidable set of axioms if and only if the theory can be axiomatized with a recursively enumerable set of axioms. So there is no need for the first replacement. Also, no theory with a recursively enumerable set of axioms can prove all true statements of Peano arithmetic - the set of true sentences of arithmetic is not r.e. - so the second suggestion would not be an improvement, and would be incorrect. I do think that "proving all truths about the arithmetic of the naturals" is not very clear, but the suggestion goes too far. Of course, there is a better statement already under the section "First incompleteness theorem" for those who read beyond the introduction. — Carl (CBM · talk) 23:57, 24 September 2017 (UTC)]