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

Archive 5

←

Archive 9

Archive 10

Archive 11

Prominence of mention of Cantor's diagonalization argument

I undid your [Leegrc's] most recent revision as I think it's simply too strong a statement to say 'based on' right in the intro...the article could use some more info about the 'diagonal lemma' and the similarities to Cantor etc but just not right at the top like that...go to that talk page if would like..68.48.241.158 (talk) 15:04, 11 July 2016 (UTC)

The lede currently indicates "Gödel's incompleteness theorems were the first of several closely related theorems on the limitations of formal systems" which is true but unprovable (hee hee). While I think it is important to credit Gödel for this giant work, it is nonetheless the case that he achieved it by standing on the shoulders of (other) giants. Gödel's insight was that Cantor's diagonalization argument could be applied to formal logic systems, if the logical statements about integers were themselves encoded as integers. I would like to see the briefest mention of Cantor in the lede; perhaps prefixing the above sentence with "Based upon Cantor's diagonalization argument," 𝕃eegrc (talk) 15:15, 11 July 2016 (UTC)

I just don't know it's fair/accurate to so strongly say 'based on' or some such right in the intro...it's possible a less strongly worded reference to Cantor could be worked in there...I do think the article itself could use a little more info about the influence/inspiration of Cantor and the "diagonal lemma" etc...there are a few others who watch this page closely and will be along to comment...68.48.241.158 (talk) 15:21, 11 July 2016 (UTC)

Perusing an online thesaurus, I see some alternatives to "based upon" such as "built on/from", "depending on", "hinging on", "standing on", "proceeding from", "grounded on/from", "rooted in", "anchored in". Do any of them put wind in your sails and/or are any of them at least in the right direction for what you are looking for? 𝕃eegrc (talk) 17:00, 11 July 2016 (UTC)

Idk it suggests something to me that isn't quite accurate, having it right in the intro like that...there's a section "relationship to liar paradox" or whatever....perhaps there could be a short section called "relationship to (or influence of) Cantor's Diagonal Lemma" or something...or maybe this info needs to be better developed/explained in the technical sections of the article....Gödel's work was influenced by/inspired by many things (including Cantor) but not sure the Cantor influence is so much more significant than all the others to necessitate such a nod right in the intro68.48.241.158 (talk) 17:17, 11 July 2016 (UTC)

but you're absolutely correct that he borrowed/used techniques developed by Cantor in the technical demonstration of the proof...I can't recall if he ever actually mentions Cantor in the paper itself..not that it matters..68.48.241.158 (talk) 17:20, 11 July 2016 (UTC)

How about "Leveraging Cantor's diagonalization argument, …"? Perhaps it is my background and my familiarity with Cantor's diagonalization argument and many of its diverse uses but, to me, these theorems of Gödel scream "Cantor" loudly enough to go into the lede. 𝕃eegrc (talk) 17:39, 11 July 2016 (UTC)

For now, I simply have to vote against any kind of statement like this...but I certainly encourage you to develop the info in the article itself (this will take more time/effort)...there are 3 or 4 other editors who watch this page closely who are fairly knowledgeable...they will be along...I strongly suspect they'll agree with me here (and they certainly don't always agree with me!) so this is why I encourage you to perhaps try the route of developing the article itself instead of the intro..68.48.241.158 (talk) 17:52, 11 July 2016 (UTC)

There is no need to acknowledge Cantor every time a diagonalization argument, a diagonalization argument-like argument or similar is used. It is part of the standard mathematical toolkit, and was so in Gödel's time too. Sometimes it is traditional to mention what is going on, naming a theorem, e.g. use of Zorn's lemma/use of the axiom of choice or the well-ordering theorem rarely goes without mention. But this is not the case here. "Using a diagonal argument" would perhaps be acceptable in some appropriate spot, not necessarily in the lead and without mention of Cantor. YohanN7 (talk) 09:59, 12 July 2016 (UTC)

Paragraph

Is the following paragraph in "first incompleteness theorem" helpful to the reading public or just confusing/not adding much??:

"Moreover, as Raatikainen (2015) states, "in favourable circumstances, it can be shown that GF is true, provided that F is indeed consistent. ... For this reason, the Gödel sentence is often called 'true but unprovable'." The word "true" is used disquotationally here: the Gödel sentence is true in this sense because it "asserts its own unprovability and it is indeed unprovable" (Smoryński 1977 p. 825; also see Franzén 2004 pp. 28–33). It is also possible to read "GF is true" in the formal sense that primitive recursive arithmetic proves the implication Con(F)→GF, where Con(F) is a canonical sentence asserting the consistency of F (Smoryński 1977 p. 840, Kikuchi and Tanaka 1994 p. 403). However, the Gödel sentence of a consistent theory may be false in some nonstandard models of arithmetic."

As is I think the section would read better with this paragraph simply deleted..68.48.241.158 (talk) 19:30, 9 July 2016 (UTC)

Honestly, I'm not hugely fond of it either.

This is the situation. The Goedel sentence of a consistent theory is true. Period. No weaseling, no waffling. Ideally, that's what we should say. We can definitely source it.

Unfortunately, the matter gets discussed to death, even though the "other side" has no valid case. This was CBM's attempt to put in something with absolutely bulletproof sourceability. --Trovatore (talk) 19:45, 9 July 2016 (UTC)

it seems unecessarily complicating..the following paragraph seems to basically cover the same ground in a way that seems more useful/appropriate for a Wikipedia article...but that paragraph seems a brief but jarring (and a bit vague) reference to more advanced technicalities and just seems distracting as stands..68.48.241.158 (talk) 20:37, 9 July 2016 (UTC)

You're kinda right, but the following paragraph buries the lede even worse than the one we're talking about. I would prefer a much less equivocal, much more direct statement, at the top of the section, pointing out that the Goedel sentence is true (full stop) but unprovable (in the theory being considered). We used to address the quibbles in an explanatory footnote, and I think that would be the way to go again. --Trovatore (talk) 21:11, 9 July 2016 (UTC)

Trovatore and I both agree that the article, like most general references, should address the truth of the Goedel sentence. Much of what was once in the explanatory footnote is now in that paragraph. It moved because we switched to a direct quote for the statement of the first incompleteness theorem. I do think that, for this kind of issue, having very clear sourcing is a must. — Carl (CBM · talk) 23:14, 9 July 2016 (UTC)

That does make sense, but I would still prefer to put the TL;DR stuff in an explanatory footnote. I'm afraid the current text really does bury the lede. --Trovatore (talk) 23:19, 9 July 2016 (UTC)

The first sentence says: in favorable circumstances, it can be shown that the Goedel sentence is true. The same sentence says: "true but unprovable". How much more direct can it be? At the same time, I don't think that the sentence about what "true" means is "TL:DR" - it's vital to understanding what it means to say that the sentence is true, which is an issue that too many people keep worrying about on this talk page. If we just say "true", we'll just get more complaints about what that is supposed to mean. — Carl (CBM · talk) 00:48, 10 July 2016 (UTC)

I think we should say flatly that it is true (when the theory in question is consistent), and deal with quibbles in a footnote. Yes, we'll get complaints, from people who have been confused by the popularizers. That should not keep us from making a direct statement. --Trovatore (talk) 00:55, 10 July 2016 (UTC)

I don't think that the meaning of "true" is really a quibble, in this case. I also think it's important to include the fact that "true" can also be read as "provable in a weak metatheory", which is to say to include the fact that the Goedel sentence is provable in a very weak theory (like PRA) from the consistency assumption. So I don't see that as a "quibble". The article needs to remain neutral between the Platonistic reading you're suggesting and a more formalistic reading of "true". — Carl (CBM · talk) 01:00, 10 July 2016 (UTC)

As you know, it is standard in mathematics to use Platonistic language whether you're a Platonist or not. I think that is the approach we should take, for the first statement we make about this. Then we can go into detail about what it means to various workers, and I think best in a footnote. --Trovatore (talk) 01:06, 10 July 2016 (UTC)

But we do just say "true" first and then explain what it means, from my perspective reading the paragraph. And the first explanation given is the Platonist one. I'm not thrilled about using a footnote, which was just there before because it was attached to the actual statement of the first theorem. If we can put the text into a regular paragraph, rather than a footnote, it's easier to read, and easier to expand on. I'm also not thrilled about the citation to the SEP article - perhaps you can find a better source for the truth of the statement? I have found it somewhat difficult to find an ideal direct quote, which is why I compromised on the SEP article. — Carl (CBM · talk) 01:09, 10 July 2016 (UTC)

At least I would get rid of "in favorable circumstances". (And also "can be shown to be".)

I generally think highly of explanatory footnotes for technical details. I think we should use them more. This strikes me as a case where one would be highly effective, as gives the main message directly at the top level, and expounds on it in a place that doesn't interrupt the flow so much.

As for direct quotes, I understand why you want to use them in contentious passages, but I think they're less than ideal in encyclopedic writing. --Trovatore (talk) 01:13, 10 July 2016 (UTC)

I agree that direct quotes are usually less than ideal, but I think this is the particular kind of circumstance where they are valuable - when there is a particular sentence which, as long as there is not a direct quote, is going to be constantly bombarded with complaints. We had the same problem with the statement of the first theorem. As for the meaning of truth here, I don't see it as a minor technical detail, but as a key part of any paragraph we would include about the truth of the Goedel sentence. In any case, if you have a better source for that paragraph, or a suggested rewording, try it out, and we can move forward from there. I spent a while looking for better sources, but what I found was not as good as what is already there. — Carl (CBM · talk) 01:19, 10 July 2016 (UTC)

paraphrasing just reads so much better...the 'background' section reads a lot better than this section, for example...the info being conveyed in this paragraph (which is correct as far as I can tell) could be better and more simply and more directly delivered using paraphrasing imo..perhaps I'll try my hand at trying something via paraphrasing...can't do it right this minute though..68.48.241.158 (talk) 01:34, 10 July 2016 (UTC)

And I agree "the favorable circumstances" clause is just so confusing..it's just a really odd way of phrasing what it's referring to, I think. It's basically this though that should be explained:

G is a well-formed proposition that indirectly points to another proposition and asserts its unprovability/undecidability within the system. But an analysis reveals that the proposition it refers to just so happens to be itself. The system, therefore, if taken to be consistent (inconsistent systems are trivial) can not decide all well-formed propositions and is necessarily incomplete. But this is exactly what the proposition asserts so the proposition is in fact true but unprovable/undecidable from within the system. Indeed, the truth of the proposition may only be arrived at via a meta-analysis from outside the system. Because of this, G is often said to be "true but unprovable."

^something more straightforward and simplified along these lines would be better/more appropriate content for the article imo..68.48.241.158 (talk) 12:40, 10 July 2016 (UTC)

Just to check, did you read the SEP article, or at least that paragraph within it, to see the reason the clause was in the original source? We could abbreviate the quote here, if we didn't want to worry about that issue. — Carl (CBM · talk) 15:41, 10 July 2016 (UTC)

just looked at it now...Wikipedia should probably be careful to not borrow too heavily from that source in its phrasing etc..I like how it explains that G isn't some universal, single proposition...I don't understand what "favorable circumstances" really means though but to simply mean the circumstances the theorems need to be applicable..68.48.241.158 (talk) 15:59, 10 July 2016 (UTC)

that is, I'm a bit lost by some of the technical detail he briefly goes into there...my intuition, however, is that it's a bit superfluous or at least distracting from what this Wikipedia article should be trying to get across in this particular passage...68.48.241.158 (talk) 16:37, 10 July 2016 (UTC)

I do not have expertise or great abilities in the technical proof itself and its technical language but I'm confident I have a very good general understanding of the proof and what it says/means...imo I also have a very good BS detector in this topic even in relation to people spouting technical BS..68.48.241.158 (talk) 16:59, 10 July 2016 (UTC)

68, you have some good stuff in there, but I would have two major objections. First, it still buries the lede. The important point is that systems of the sort under discussion cannot perfectly distinguish truth from falsity in arithmetic, because either there will be a true statement of arithmetic that the system will not find (that's the consistent case), or there will be a false statement that it will count as true (in the inconsistent case).

Relatedly, we need to point out that the Goedel sentence is a statement about the natural numbers. It is not self-referential, though it codes up certain aspects of self-reference. You do a good job of explaining at a high level how that coding part works, but it is still possible to read your text and not realize that the statement is making a very simple (in logical form, not in length complexity) statement about the naturals. --Trovatore (talk) 21:49, 10 July 2016 (UTC)

Yes, the article could potentially benefit from a stand alone section titled "truth vs provability" or some such as this trips many people up and is of particular interest to the general reader...what you refer to about the proposition is addressed in the final paragraph of the section under discussion...it's possible this paragraph should be moved to earlier in the section or the info contained within it be combined into another paragraph etc..68.48.241.158 (talk) 22:23, 10 July 2016 (UTC)

"However, the Gödel sentence of a consistent theory may be false in some nonstandard models of arithmetic." Does this sentence need to be where it is?...seems a distracting technical tangent..68.48.241.158 (talk) 00:38, 12 July 2016 (UTC)

It's quite common for people to think of truth as provability, i.e. truth in all models. So, in an elementary article, it's important to point out that the Goedel sentence is true, but it is not true in all models. — Carl (CBM · talk) 11:14, 12 July 2016 (UTC)

I also believe that the inclusion of the info about PRA is useful, along with the detailed references. These are not "tangents"; they are key aspects of the situation. — Carl (CBM · talk) 12:24, 12 July 2016 (UTC)

If this info is deemed relevant at this point in the article (instead of perhaps later in a more technical section) I think it should come in its own paragraph directly after the paragraph I just constructed...it's mostly a style thing...it just reads really clunky the way it's constructed now imo...68.48.241.158 (talk) 12:36, 12 July 2016 (UTC)

Also, can you point me to a source about "However, the Gödel sentence of a consistent theory may be false in some nonstandard models of arithmetic." It seems an odd statement to me...what are these "nonstandard models" and are they applicable/relevant to the incompleteness theorems in any direct way? What does it mean to say it is false? and how is it relevant to this section of this Wikipedia article? 68.48.241.158 (talk) 15:23, 12 July 2016 (UTC)

I'm not an expert, but the point is that Goedel sentence of a consistent theory is formally undecidable in that theory; that means that adding either the sentence or its negation (but of course not both) will yield consistent theories, and each of these will have a model. Hence, there must be a model for the theory T+not(G), but this cannot be the standard model (in which we can argue metamathematically that G is "true"). Thus, there is an interpretation of the theory (a model) in which G is false. This is not just "relevant", it is key to the Incompleteness Theorem and to the formal undecidability nature of the Goedel sentence. Magidin (talk) 18:21, 12 July 2016 (UTC)

Hmm, no, I wouldn't say "key". The incompleteness theorems are primarily proof-theoretic, not model-theoretic. By the completeness theorem, they have a model-theoretic counterpart, but while this is interesting in itself, it is not the main point. The impact of the theorems, in terms of making Hilbert's program appear hopeless and refuting at least the simplest versions of formalism and logicism, goes through the proof-theoretic formulations. --Trovatore (talk) 18:39, 12 July 2016 (UTC)

"However, the Gödel sentence of a consistent theory may be false in some nonstandard models of arithmetic." perhaps this is true but it would need context to make sense to anyone reading this article..it's just thrown in in the middle of discussion of a standard presentation of the theorem where G is simply true but undecidable by the system...the quick unexplained tangent is just like "what??"68.48.241.158 (talk) 18:51, 12 July 2016 (UTC)

I kind of agree with you, actually. The point should be treated somewhere, but I'm not sure it needs to be right there. --Trovatore (talk) 19:09, 12 July 2016 (UTC)

"Perhaps" it is true? Again, let me ask if you have read the SEP article, which has two paragraphs and a section title about the topic of nonstandard models! These are a very basic topic in logic, something that is seen in a first course, and we have an article Non-standard model of arithmetic. It is always the case that, if a consistent theory is unable to disprove some statement, then there is a model of the theory in which the statement is true. In the context of incompleteness these are important as examples of non-ω-consistent theories, which show that Rosser's trick is indeed important for the full proof of the theorem.

Frankly, I am finding this discussion somewhat surreal. To edit an article requires getting familiar with the basic topic of the article! I would recommend reading some recent sources - Peter Smith's book is excellent, Tokel Franzen's book is also quite good. The SEP article is brief, but it does show one model of an encyclopedia article about the subject. — Carl (CBM · talk) 21:46, 12 July 2016 (UTC)

Let's not fixate on the "perhaps". Yes, it's definitely true. But I kind of think 68 is correct that it's a bit jarring to suddenly drag in model theory at that point. Up to that point, no model theory has been mentioned. --Trovatore (talk) 21:53, 12 July 2016 (UTC)

yes, I'm not really suggesting it's wrong...just that it's sitting there in a vacuum or something...it's a writing style problem..the following section of this section, for lack of a better word, just sucks currently:

"...However, the Gödel sentence of a consistent theory may be false in some nonstandard models of arithmetic.

The truth of the sentence GF may only be arrived at via a meta-analysis from outside the system. In general, primitive recursive arithmetic proves the implication Con(F)→GF, where Con(F) is a canonical sentence asserting the consistency of F (Smoryński 1977 p. 840, Kikuchi and Tanaka 1994 p. 403)."

The first sentence of that next "paragraph" needs to be incorporated into the preceding paragraph, I firmly believe...and something just needs to be done differently with the technical references here.....68.48.241.158 (talk) 22:17, 12 July 2016 (UTC)

And I had solved the style problem at least to some degree by simply removing the other two sentences in a previous edit as I think the article can do away with that particular information (at least at this point in the article, etc)..68.48.241.158 (talk) 22:40, 12 July 2016 (UTC)

Section: First incompleteness theorem

The text of the section "First incompleteness theorem" was getting out of hand. I have added a section header for some of the new material on truth, and arranged the section generally as follows:

• Statement of the theorem
• First mention of "Godel sentence" , and two existing paragraphs that mention what happens when you add the Gödel sentence as an axiom, and on the general idea of the proof. The latter paragraph needs help.
• Form of the incompleteness sentence - see below
• Truth of the Gödel sentence - note: refers to the idea of the proof mentioned already
• Existing section: "Meaning of the first incompleteness theorem" - note: refers to the truth of the sentence
• Existing section: "Relation to the liar paradox"
• Existing section: "Extensions of Gödel's original result" - on Rosser's trick

It is hard to rearrange the first three bullets into a different order, because each depends on things mentioned in the previous one. — Carl (CBM · talk) 23:04, 12 July 2016 (UTC)

still needs some shaping but, yes, this was a very good idea...68.48.241.158 (talk) 23:16, 12 July 2016 (UTC)

Following a suggestion of Trovatore I added a paragraph on the form of the Gödel sentence. There are many references on this point. — Carl (CBM · talk) 23:29, 12 July 2016 (UTC)

The section on the "Meaning of the first incompleteness theorem" needs work. It is a mixture of several ideas, and not in a sensible order either. — Carl (CBM · talk) 23:55, 12 July 2016 (UTC)

definite improvements overall..and I agree that next section is/has been problematic as well..68.48.241.158 (talk) 00:11, 13 July 2016 (UTC)

The smaller, more direct to the point sections at the beginning of the article are a big improvement...with such a big rewrite/restructuring there are at least many small style tweaks that will have to be worked out slowly....some later sections that seem a little not to the point and perhaps a bit repetitive of information include "EXAMPLES OF UNDECIDABLE STATEMENTS"/"FOUR VARITIES OF THEORIES"...68.48.241.158 (talk) 13:41, 13 July 2016 (UTC)

arithmetic

I think the lede should specifically reference that we're talking about "arithmetical" relations here in a couple of those sentences...for a long while it had that parenthetical "(arithmetic)"...I suppose it's true that any relationship between them is inherently arithmetical...but for the sake of the general reader..

Also, this notion should probably be explained briefly somewhere as I don't think it's touched upon at all...these are Gödel's words from the Metzger translation:

"..there are in fact relatively simple problems in the theory of ordinary whole numbers which cannot be decided from the axioms." "theory of ordinary whole numbers" is synonymous with "arithmetic" here...his footnote for this sentence states, "ie, more precisely, there are undecidable propositions in which, besides the logical constants, there are no other concepts beyond addition and multiplication, both referred to natural numbers and where prefixes can also only refer to natural numbers." later in the paper he briefly states, "a relation is called arithmetical if it can be defined solely by the means of addition and multiplication applied to natural numbers.." (keep in mind that the inverses (division and subtraction) can be stated via the concepts of addition and multiplication in these systems..) 68.48.241.158 (talk) 16:35, 13 July 2016 (UTC)

"all truths about the natural numbers" seems vague...there are probably truths that aren't arithmetical...idk, a really dumb example is that the symbol for the number 5 can be found on my mailbox...idk, point is the general reader might not no what this means..68.48.241.158 (talk) 16:47, 13 July 2016 (UTC)

(^^I'm operating under the assumption that I'm basically talking to two other editors who understand the article edit activity that led to these threads...so these threads are likely incomprehensible to the uninitiated...I can clarify the issue better for others, if requested)..68.48.241.158 (talk) 19:04, 13 July 2016 (UTC)

References

Would anyone mind terribly if I changed the referencing style to that in e.g. Cayley–Hamilton theorem? (Signature added after original post.) YohanN7 (talk) 10:02, 14 July 2016 (UTC)

(responding to proposal above..posted by YohanN7, I think): it certainly looks better and reads easier that way..so I would certainly support unless there's a particular reason why not..68.48.241.158 (talk) 13:34, 13 July 2016 (UTC)

It is mostly a policy, WP:RETAIN, that basically says don't fix it if it ain't broken (The link talk only about US vs British English, but the same principle is rather global.) YohanN7 (talk) 13:39, 13 July 2016 (UTC)

I'm confused...you want to change it, right?

Of course. I'll begin with what can be done without protests, templetizing the reference list. This opens up for having clickable citations, whether they are explicit (like (Franzén 2004, p. 112)) or ordinary footnotes.

One huge advantage of having references in this way is that it is so much easier to add citations. YohanN7 (talk) 13:48, 13 July 2016 (UTC)

yes, sounds good to me (I think you need to resign your first comment in this thread as it went away...so it kind of looked like I posted it)..68.48.241.158 (talk) 13:53, 13 July 2016 (UTC)

I'm sorry, I thought you were referring to the article's in-text citations...so nevermind..but I'm sure what you did is good and fine...68.48.241.158 (talk) 14:44, 13 July 2016 (UTC)

Yes, I would mind. This article uses regular Harvard-style referencing, which is a common style in actual published writing. It makes the citation for each sentence clear without having to look elsewhere (i.e. at a glance the reader knows which source is used). I would not support changing to the style of Cayley–Hamilton theorem. Also, I have found that, in general, the "clickable" references tend to be very fragile, and don't work as advertised except in very simple cases. — Carl (CBM · talk) 16:20, 13 July 2016 (UTC)

I'm all confused by this...I think he did something with the references at the bottom, after the article text..??68.48.241.158 (talk) 16:24, 13 July 2016 (UTC)

I think he converted some references to use citations. I don't really like that idea, either - the article mostly does not use templates, so probably the one or two that were added with templates should be changed to match the majority, rather than vice-versa. The citation templates also turn out to be inflexible except in simple cases; if there are reprints, multiple editions, etc., the citation templates can become an obstacle rather than a tool. — Carl (CBM · talk) 16:28, 13 July 2016 (UTC)

The templates are flexible enough.

1. A formal system is said to be effectively axiomatized (also called effectively generated) if its set of theorems is a recursively enumerable set (Franzén 2004).
2. A formal system is said to be effectively axiomatized (also called effectively generated) if its set of theorems is a recursively enumerable set .

• Franzén, T. (2004). An Incomplete Guide to its Use and Abuse. A.K. Peters. ISBN 1-56881-238-8. MR 2007d:03001. {{cite book}}: Check |mr= value (help); Invalid |ref=harv (help)

Editions, reprints and the like can be handled. One will get into trouble if one wants to list the translators brother in law and his wife, but there is nothing to prevent you from writing arbitrary text after the template or after the citation template in the footnote. Then, if one still has trouble, one should probably reconsider what belongs in the reference list and what does not.

Templates standardize the way references appear. Without them, a complete mess will result, especially with many references since most people don't know how to format a reference.

Moreover, they facilitate adding new inline citations that don't clutter the source text. They are clickable. A click takes you first to the right entry in the reference list and then (if the reference is complete in this respect), you can click your way to an online copy or a place to buy the item in question. As seen above, footnotes is not the only option.

Naturally, it should be used uniformly. I begun yesterday with the reference list (didn't touch the main body), and intended to do all of them, but that was reversed by CBM along standard info such as isbn numbers and editors. I truly don't understand why it is better to have the current "system". It sucks. YohanN7 (talk) 09:59, 14 July 2016 (UTC)

I do know the arguments for templates; I just don't find them as compelling as I once did. There's no general policy in favor of templates, and I think the current system is serving the article perfectly well. It has the benefit of being easy to type, and easy for other editors to pick up. In the end it's just a matter of preference, though, and so when there is a disagreement the usual rule of thumb is to keep the original version, which in this article was to have citations without templates.

At the same time I have no problem with adding ISBN numbers, and I'll go back and re-add any that I inadvertently removed. — Carl (CBM · talk) 12:12, 14 July 2016 (UTC)

Fair enough. I should have waited longer for replies after posting this thread. YohanN7 (talk) 12:23, 14 July 2016 (UTC)

Role of Self-Reference and Franzen

This section needs to go imo...it adds little or nothing and the individual it's quoting is simply not particularly notable (ie his opinion, whether right or wrong isn't notable enough to include...unlike Wittgenstein whose opinions in this area (though mostly wrong) are most certainly notable...he's an obscure academic who wrote yet another fairly obscure book that attempted to explain the theorems to the general reader...idk how much he should even be cited in the article itself...I think the article can simply cite Gödel's paper itself for most of it's content/assertions...or is this against the rules?...like the above quotes from his paper about arithmetic...could we just cite him or do we have to cite someone else explaining it?? (I don't mind him being referenced briefly in the section just above along with Rebecca Goldstein etc, however)...68.48.241.158 (talk) 17:38, 13 July 2016 (UTC)

^as stands, I feel it's basically exactly analogous to Hewitt's desire for commentary by whoever it is he wants commentary by.....68.48.241.158 (talk) 17:53, 13 July 2016 (UTC)

Generally secondary sources are better for our purposes than primary. Certainly Gödel's own views are relevant, especially for the historical angle, but ideally what we're looking for is the conclusions that experts have come to in the intervening decades, with lots of time to think about it and polish their formulations.

Franzén is a useful source because he was a very smart guy who spent a lot of time analyzing the import of the theorems and making them accessible, but unlike the popularizers, he was personally an expert in the field.

I don't entirely like his take on this aspect, as I don't think the theorems are self-referential in the first place, so there is no need to strain to find formulations that are not. But I do think he's a good source. --Trovatore (talk) 18:50, 13 July 2016 (UTC)

depends what you mean, I guess..the notion of self-reference plays in with the meta-analysis from outside the system that discovers the truth of the proposition...in any event, this stand-alone section seems entirely dedicated to a fairly unimportant, idiosyncratic opinion of a fairly non-notable person...68.48.241.158 (talk) 19:10, 13 July 2016 (UTC)

The more I look at that section, the odder and more inappropriate it looks to me...it's an undeveloped stand alone section dedicated to an idiosyncratic opinion statement by a contemporary, non-notable academic...I'm going to delete it...per my reasoning and apparent at least soft support of Trovatore....if CBM or someone else wants to reinsert it please come here and explain....68.48.241.158 (talk) 00:10, 14 July 2016 (UTC)

I "approved" the edit, but that term was a bad choice by the software engineers. In general, I will approve edits even when if I have no opinion or possibly even disagree with them, so just because I "approved" them should not be taken as a comment other than that I don't want to see them "pending". (This is why sometimes I may "approve" a revision and then undo parts of it.) — Carl (CBM · talk) 00:38, 14 July 2016 (UTC)

fair enough, thanks..68.48.241.158 (talk) 00:48, 14 July 2016 (UTC)

I'm not sure I agree with the cavalier dismissal of Franzen by 68/anonymous editor. Franzen was a well-regarded expert in the field who wrote several books on the subject, both in terms of addressing a general audience and in terms of a mathematical one. I would put him on par with Raymond Smullyan in terms of reliability. The entire tone above sounds to me like "I don't like this quote. Since I've never heard of him, he is not a notable source and this should be deleted." The comments on self-reference are at least somewhat relevant (probably more), especially when you have folks in this talk page who imply and argue that the statements are self-referential and hence should be "disallowed". Magidin (talk) 03:29, 14 July 2016 (UTC)

this single opinion/commentary quotation simply doesn't warrant its own stand alone section imo...it's also basically repeating information from an earlier section in the article (as the explanation sentence below the quotation even says...imo work it in up there very briefly, if deemed worthwhile..but not with the whole long quote...nobody's quoted at such long length in the article...not Bertrand Russell, not Wittgenstein, not Godel himself...but "Torkel Franzen"??? It's the same thing as Hewitt wanting some long, also odd quotation by whatever unimportant person he wanted commentary by....68.48.241.158 (talk) 12:19, 14 July 2016 (UTC)

And again, and now scare quotes. Let me just say: just because you don't know who a person is does not mean that person is a nobody or an unknown, or an unreliable source. So, again, thanks for the cavalier dismissal of someone based mainly on your ignorance. I disagree on your analogy with Hewitt; the objections to the additions proffered by Hewitt are on their lack of substantive support of the views espoused. This is not the case with these; and, again: you may have no clue about who Franzen was. That does not make him the nobody you want to pretend he was. Last I checked, Argumentum ad Ignorantium was still a fallacy. Magidin (talk) 16:01, 14 July 2016 (UTC)

The quotations at [1] are substantive and support the views espoused.

Frazen is as authoritative as Smullyan and Hofstadter.

Carl (talk) 16:02, 14 August 2016 (UTC)

I know who the guy is in the sense that I read through his book quickly at a Borders Books nearly a decade ago now..He even has a small Wikipedia page too etc...my objections partly in that he's simply not notable enough to have a stand alone section devoted entirely to a single quotation of his..and partly that the section is itself just sort of odd itself in the context of the rest of the article...68.48.241.158 (talk) 18:25, 14 July 2016 (UTC)

Yes, I think Franzén is a fine source. Not as many people know him as know (say) Hofstadter, and he's not as good a writer (that's a high bar), but he has a much deeper and more solid understanding of the subject matter.

In context he doesn't seem to be saying that the sentences in question are self-referential, just that people perceive them to be and that misunderstandings result from this. I agree that's probably accurate; I just have a different strategy, and would prefer to tackle that misunderstanding at its source, by showing that the sentences are very ordinary (if long-winded) assertions about natural numbers, not about the sentences themselves.

But I obviously can't demand that Franzén follow my strategy. I think the material is reasonable to include. I'm not sure it merits its own section, though. --Trovatore (talk) 04:59, 14 July 2016 (UTC)

I agree it at least doesn't seem to merit its own stand alone section, at least as currently constructed..68.48.241.158 (talk) 11:36, 14 July 2016 (UTC)

Of course there is beaucoup literature that describes the Goedel sentence as self-referential, so it won't work for us to simply claim it isn't. Of course, the self-reference is indirect, just as with the recursion theorem in computability theory. And the Goedel sentence is just a $\Pi _{1}^{0}$ sentence of arithmetic, like the statement of Goldbach's conjecture and like many other statements about elementary number theory. Franzen's text is quite high quality and "mainstream" within the limited number of scholarly secondary sources directly about the incompleteness theorems. In the end, the Goedel sentence relies more on a kind of diagonalization than it does on self-reference, but finding a source that clearly expresses that may be challenging.

I don't mind the current set up, in which the article points out that the Goedel sentence indirectly refers to itself. On the other hand, it would be worth pointing out that the underlying phenomenon does not really depend on self-reference, because when we view the Goedel sentence as just a formula of arithmetic, forgetting its intended meaning, there is no self-reference there. Goedel mentioned this fact in print, as well, in responding to Wittgenstein, as we quote. For that subject, I am sure we can assemble something from a few sources - I suspect Peter Smith's book also comments on the issue. — Carl (CBM · talk) 12:50, 14 July 2016 (UTC)

The indirect reference is for the Gödel number of the string used to create the proposition I'm unprovable using the diagonal lemma. However in general, mathematical propositions do not have Gödel numbers because there are unaccountably many mathematical propositions (as was noted early on by Zermelo).

Carl (talk) 20:44, 14 August 2016 (UTC)

^and some of this speaks to confusions even otherwise learned people like Hewitt have about this topic imo..indeed, perhaps some of the new phrasing in the article along these lines will be helpful to readers..68.48.241.158 (talk) 13:11, 14 July 2016 (UTC)

For those of you interested in the current academic controversy concerning the validity of Gödel's proposition in mathematics, see the YouTube video of the recent SRI seminar [see link on my Google+ homepage (at CarlHewitt-StandardIoT) or go the the SRI International YouTube channel].

Carl (talk) 20:44, 14 August 2016 (UTC)

Diagonal Lemma produces the Liar Paradox

Using the Diagonal Lemma, there is a proposition P such that

   P ⇔ ¬P

Of course, the above proposition immediately infers a contradiction.

See Inconsistency Robustness in Foundations

Carl (talk) 16:12, 4 November 2016 (UTC)

I didn't realize propositions could be sentient. (The verb you're looking for is "implies", not "infers".) </pedant> —David Eppstein (talk) 18:15, 4 November 2016 (UTC)

Inference (⊢) is different from entailment (⇒) for inconsistency robust logic ;-)

See Formalizing common sense reasoning for scalable inconsistency-robust information coordination using Direct Logic™ Reasoning and the Actor Model

Carl (talk) 18:52, 4 November 2016 (UTC)

I don't see why what "Inconsistency Robust Logic" or "Direct Logic" (disputed trademark) has to say has any place in this article, except as it relects your expert, but not reliable, opinion. It might, if accepted. — Arthur Rubin (talk) 17:48, 12 November 2016 (UTC)

Classical Direct Logic is highly relevant to strong incompleteness theorems. See Proposals for article on Incompleteness theorem

Carl (talk) 19:07, 12 November 2016 (UTC)

An independently published source would be great, rather than your own thoughts expressed on Wikipedia. Binksternet (talk) 04:01, 13 November 2016 (UTC)

Language

From a Linguists viewpoint it might be OK, but this is really confusing: "The next step in the proof is to obtain a statement that says it is unprovable." What is "it"? The proof? There's a bit of irony in using self-reference in an argument about the incompleteness of (some?) self-referential logics. 91.66.3.34 (talk)

Further into the paragraph: "[... the diagonal lemma] says for any sufficiently strong formal system and any statement form F there is a statement p such that the system proves [...]". Nevermind that the term "statement form" isn't introduced before it is used. Maybe it's knowledge that I am expected to know (I get it, you talk about F). The sentence is still hard to parse. If the "system proves", then the system is a proof, which is idiosyncratic language, but the whole paragraph is trying to say in the end that the system cannot prove in this particular case, so it's mathematically misleading. 91.66.3.34 (talk)

"This sentence does not directly refer to itself" The mentioned sentence is not a correct sentence at all, most of all because the quote "when preceded by [...]" is not a syntactically correct statement in English and thus can't become a proven statement. 91.66.3.34 (talk)

Ultimately, all three points I made before concern a section that is covered again in another article Proof_sketch_for_Gödel's_first_incompleteness_theorem. 91.66.3.34 (talk) —Preceding undated comment added 22:24, 24 July 2016 (UTC)

Some of these are easy to resolve; others don't seem to be issues.

The "it" in the first case seems unobjectionable: "it" refers to the previous noun, "a statement". But it would be easy enough to say "says of itself that it is unprovable", so I will make that edit.

The "statement form" language should be rewritten, along with that whole section. But saying that a formal system, or a formal theory, "proves" a certain statement is perfectly normal usage.

In the third point - there is no reason that the content of the quote itself needs to be grammatically correct. For example, "bob purpled jump" when preceded by "blue" becomes "blue bob purpled jump" - and none of the quoted phrases is a sentence. The claim is not that the quoted statement is provable, but rather that the result of performing a certain transformation is provable. Analogy: "+2=4", when preceded by "2", is provable. This is because when "+2=4" is preceded by "2" it becomes "2+2=4".

Similarly

", when preceded by itself in quotes, is unprovable.",

when preceded by itself in quotes, gives exactly the phrase:

", when preceded by itself in quotes, is unprovable.", when preceded by itself in quotes, is unprovable.

which is a grammatical sentence regardless what is in the quotes. — Carl (CBM · talk) 22:26, 24 July 2016 (UTC)

It is worth noting that the Diagonal Lemma can also be used to produce the Liar Proposition: The negation of this proposition holds.

Carl (talk) 21:06, 14 August 2016 (UTC)

Up front: It's far besides the point to argue the lyrical analogue, while I don't understand the mathematical argument and the diagonal lemma.

I am trying to say that the liars paradox, "this sentence is wrong", is not a paradox. The easy way out of the paradox is to forbid this self reference. "this sentence is not a sentence" can be true and wrong depending on the interpretation. It is the most obvious contradiction. You can choose: either it is a sentence and wrong, or it is not a legal sentence but anything else.

I assume, a quote cannot grammatically correctly stand in for a subject. That is the whole sentence would at least have to start introducing the subject. I'll try:

'The quote, "The quote, X, when substituting the first X with the whole quote, is unprovable", when substituting the first X with the whole quote, is unprovable'

Now this seems to come down to saying that a free variable X is unprovable. Which is, depending on the definition of provability, which I'm not sure about, unremarkable.

And what about deduplicating the section and the other article? 31.16.51.96 (talk)

I was concerned with my previous post for quite a while. Now it appeared to me, I was basically saying, that sentence is not a sentence in first order logic. Why is Higher Order Logic useful at all? I'm still on the case. 91.66.7.227 (talk) 02:13, 3 March 2017 (UTC)

But Carl isn't on the case anymore, he was banned for other reasons (which in my mind comes down to misrepresenting the completeness theorem). Some else care to pitch on my request for deduplication? 91.66.15.241 (talk) —Preceding undated comment added 02:35, 17 March 2017 (UTC)

Floyd and Putnam's vs Floyd's and Putnam's

In light of the anonymous editor's multiple attempts: The Chicago Manual of Style gives:

When two nouns “possess” the same entity, only the second takes an apostrophe (‘):

my aunt and uncle’s house

Gilbert and Sullivan’s lolanthe

Minneapolis and Saint Paul’s transportation system

On the other hand, when two nouns possess different entities, both possessives take an apostrophe:

my aunt’s and uncle’s specific talents

New York’s and Chicago’s transportation systems

our friends’ and neighbors’ children

Note in particular the second example. In the present instance, since Floyd and Putnam possess the same paper, the apostrophe goes only after the second, not both. Magidin (talk) 14:34, 12 April 2017 (UTC)

Agreed - it should be "Floyd and Putnam's" rather than "Floyd's and Putnam's". We are talking about the argument of Floyd and Putnam, not separate arguments of Floyd and Putnam. There is hardly a need to check this kind of standard rule, but it is explicitly laid out in section 7.22 of the Chicago Manual of Style. — Carl (CBM · talk) 17:04, 12 April 2017 (UTC)

"Thus, although the Gödel sentence refers indirectly to sentences of the system F, the Gödel sentence is actually written as a statement about natural numbers solely."

I think this sentence requires a bit of explanation - it's not immediately clear (at least, to me) what it's supposed to mean. The Gödel sentence is not a sentence in natural-language. It is a sentence in a formal language. It need not necessarily be "a statement about" anything, in particular - and speaking to intended meaning is more confusing, still (sure, Gödel may have intended it to speak of natural numbers - but the mathematics does not care about what Gödel was trying to say, it only cares about the axioms and manipulations he performed). This section does a remarkably poor job of separating matters of interpretation (which are contentious and seldom agreed-upon) from matters of mathematics (which are utterly uncontroversial). At the very least, some account needs to be given for what is meant by a formal sentence being "about" something in the metatheory (as opposed to in the theory).

Perhaps, a separate "interpretation" or "meaning" section is in order, in which this can be discussed with a bit more clarity? 173.49.79.101 (talk) 05:38, 16 April 2017 (UTC)

One of the hypotheses is that a certain amount of the theory of the natural numbers is relatively interpretable in the theory under consideration. The Goedel sentence is a Π⁰₁ sentence in the language of arithmetic. The sentence that the theory neither proves nor disproves is the corresponding sentence in the language of F, after applying the relative interpretation. --Trovatore (talk) 05:56, 16 April 2017 (UTC)

I understand that, if we explicitly interpret the Gödel sentence in the context of a broader theory, then this makes sense. I don't object to pointing out that "true but unprovable" is a useful interpretation of the Gödel sentence (we're usually working within such a larger system), I only think that the current writing does a really awful job of making it clear that this is what is meant. Rather than state that "the Gödel is actually written as a statement about the natural numbers solely" ("written about?" by whom? it's just a string of symbols) I think it would be far more readable and helpful to just say, quite simply, "if we interpret the Gödel sentence in the context of a larger theory, etc." Interpretations of formal sentences are, in an important sense, separate from the sentences themselves - the Gödel sentence, qua a mathematical object, is not innately "about" anything. 173.49.79.101 (talk) 06:23, 16 April 2017 (UTC)

The above are useful clarifications. Won't you please edit the article? AmirOnWiki (talk) 07:59, 16 April 2017 (UTC)

I edited a sentence to say "Thus, although the Gödel sentence refers indirectly to sentences of the system F, when read as an arithmetical statement the Gödel sentence directly refers only to natural numbers.". I am not sure about what confusion that sentence can cause, given the two paragraphs before it. The overall theme of the section is that, although the sentence is designed to capture some fact about proofs, taken literally it is a (formal) sentence in the language of arithmetic about natural numbers. I don't think it is more confusing to mention the interpretation. In general, very concrete edit suggestions are easier to respond to than general comments about entire sections. — Carl (CBM · talk) 18:35, 16 April 2017 (UTC)

I think you might slightly misunderstand my concern (I apologize for not being sufficiently clear) - my issue was that we cannot say that the Gödel sentence refers to "natural numbers" (as opposed to generic "formal objects of a system whose axioms meet the given requirements") without explicitly choosing to speak of it in that context from the point of view of some broader theory in which the natural numbers are actually defined (the Peano axioms can't really be said to, per se, be "about" the natural numbers for precisely the same reason). In a larger context, we can say that the Gödel sentence is a true-but-unprovable statement about the natural numbers - but equally, we could call it a false-but-unprovable statement about, say, the hypernatural numbers. In this sense, saying that the Gödel sentence is "about" the natural numbers is, in some sense, making a choice to read it in a specific context (a particularly useful and natural context, and the one in which Gödel originally conceived it, perhaps - but I don't think this really affects the point). Your "when read as an arithmetical statement" wording does improve this somewhat, I think. 173.49.79.101 (talk) 02:55, 17 April 2017 (UTC)

I think you're getting a little confused here. We are not working in the context of the formal theory under discussion, when we prove the incompleteness theorems. We're working in the context of general mathematics (perhaps or perhaps not in some formal theory, depending on how you understand general mathematics). The formal theory under discussion is in this context an object of study, not a tool for deriving mathematical truths. --Trovatore (talk) 05:00, 17 April 2017 (UTC)

The Gödel sentence itself isn't necessarily a statement about general mathematics though. It's just a formal sentence - another "object of study," as it were. To interpret it in the more general context (be it a larger formal theory, or else some intuitive notion of "mathematical reality," or whathaveyou) is something quite separate from simply proving the theorem. 173.49.79.101 (talk) 05:08, 17 April 2017 (UTC)

The Goedel sentence itself is constructed as a statement about the natural numbers. It says "there does not exist a natural number that codes a proof of ..." where of course the dot dot dot is a little bit involved. That's what you start with; that's how you prove that it can't be proved by the object theory. Then if you like you can forget the interpretation in terms of the naturals, but it was there to start with.

This "forgetting" is unfortunately often part of what looks like an attempt at mystification. A lot of people read the popularizers and come away with the impression that the Goedel sentence and its negation are "equally good" ways of extending a theory, which in general they are not. --Trovatore (talk) 05:12, 17 April 2017 (UTC)

Your "construction" is what I would call "motivation." It is not a necessary portion of the mathematics (in a strictly formal sense), and the history of mathematics is littered with theorems originally intended to describe one kind of thing actually being a general description of many kinds of things. I think it is inaccurate (or at the very least somewhat misleading) to describe such theorems as "about" the things they were originally intended to describe. 173.49.79.101 (talk) 05:16, 17 April 2017 (UTC)

No, it is exactly part of the mathematics, the mathematics used to prove the incompleteness theorem in the first place. The incompleteness theorem is proved in some theory (formal or otherwise) that understands arithmetic. --Trovatore (talk) 05:18, 17 April 2017 (UTC)

That it is proved in some metatheory that understands arithmetic does not necessarily imbue the formal sentence with some sort of objective meaning - it cannot, precisely because the sentence can be formalized by axioms that have models other than the natural numbers. Whether these models are "equally good," insofar as they are useful for doing what we'd like to do in arithmetic, is sort of orthogonal to this point. 173.49.79.101 (talk) 05:24, 17 April 2017 (UTC)

Surely what we'd "like to do in arithmetic" is find out truths about the natural numbers? These other models have false beliefs about the natural numbers, and I don't think that's at all orthogonal to the point. --Trovatore (talk) 05:29, 17 April 2017 (UTC)

If you view it as a statement about arithmetic, sure. My whole point is that I do not see that we need to view the Gödel sentence as such (in the same way that many very-general mathematical results were motivated by study of a narrower field that we no longer view them, at least without specific indication, as being "about"). As I said, though, the new wording of "when read as an arithmetical statement" does somewhat resolve this. 173.49.79.101 (talk) 05:35, 17 April 2017 (UTC)

Presburger axioms

What is the difference between the Peano axioms as given here and Presburger axioms? I don't see any, though I might be missing some subtlety. The Presburger axioms seem to be the same. The Presburger axioms are described in their own article on Wikipedia https://en.wikipedia.org/wiki/Presburger_arithmetic (which ought to be linked with the other See Also links). There is a good description of the Presburger axioms and a proof of their consistency and completeness for arithmetic with sum in Bruno Poizat, A Course in Model Theory, Springer-Verlag, 2000, section 7.3 beginning on page 111. Peano's axioms, which includes multiplication, are discussed in section 7.7, beginning on page 134, where they are contrasted with Pressburger's axioms. The reason Pressburger's axioms are provably complete and consistent is that they do not capture multiplication, only addition. Multiplication is necessary to form internally the self-referential statement that leads to incompleteness of axiomatizations of Peano arithmetic.

I would recommend that Poizat's book be listed as a reference here since it gives a comprehensive discussion of the notions of completeness versus incompleteness and provides several examples of provably complete axiomatic systems of mathematical theories. It also discusses Tarski's fundamental role in this work.

Ichafe (talk) 15:21, 26 April 2018 (UTC)

The difference lies in the Axiom Schema for induction: the formula must be "in the language of Pressurger arithmetic" for Pressburger arithmetic, while in Peano the formula is in the language of Peano arithmetic. That is, the statement you are trying to prove by induction in Pressburger arithmetic can only use $0$, $1$, and $+$ (plus any derived notions); whereas in Peano arithmetic that statement can also use multiplication. So the axiom schema for induction includes more statements in Peano than in Pressburger. It's as if there is an additional language you can use in Peano to make statements.

That said, there seems to be a serious break in tone between your first two sentences above and the rest of what you write.Magidin (talk) 16:06, 26 April 2018 (UTC)

Not sure what you mean by change in tone. I didn't intend any tone. Is there an axiomatization for clarifying such a thing?

The article gives the impression that formal systems of axioms are somehow always incomplete. That is not what is meant directly, but I believe that stating clearly that there exist formal systems that are not trivial that are complete and consistent, such as Presburger's axioms for addition, would be a useful addition to the site. Many people are confused about this. It is important that multiplication and addition are both required for incompleteness, since without them the language for expressing the statements that cause incompleteness is not available internally. The reference by Poizat is one of the better rigorous texts in logic that discusses such clearly and in detail, though it is from a model theoretic point of view.Ichafe (talk) 22:01, 10 May 2018 (UTC)

Non-breaking spaces

There's been some recent editing regarding non-breaking spaces here and at infinity. Just looking at this article, I have to say that the use of &nbsp; seems to be a bit haphazard. For example,

Each effectively generated system has its own Gödel sentence. It is possible to define a larger system F’ that contains the whole of F plus GF as an additional axiom.

Here the &nbsp; after F’ note that this ’ is probably not in line with the MOS, but that's a separate issue seems to be designed to prevent a line from ending with F’. That might make sense, but then why not one after G_F as well? Or at the end of the paragraph,

in that GF′ will refer to F’, rather than F.

the nonbreaking space appears meant to prevent F from appearing all by its lonesome on a line. OK, but then earlier in the paragraph,

no contradiction is presented by its provability within F’.

why isn't there one before F’? Granted that there's another sentence that follows it, but it would still be awkward for a line to start with F’.

I think we should either figure out some clear rationale for the use of &nbsp; and use it consistently (which sounds like a lot of work), or just drop it, which seems a lot easier. The existing uses look like they were added because of how it looked on a particular editor's screen at one time, which is not a very useful criterion. --Trovatore (talk) 17:46, 1 November 2018 (UTC)

sound vs true

The line under " Extensions of Gödel's original result":

This is mostly of technical interest, because all true formal theories of arithmetic (theories whose axioms are all true statements about natural numbers) are ω-consistent, and thus Gödel's theorem as originally stated applies to them.

should read "all sound formal theories of arithmetic..." — Preceding unsigned comment added by 128.111.173.2 (talk) 17:56, 28 April 2019 (UTC)

Skepticism about Con(PA)

I recently accepted three pending revisions that cleaned up some repetitive language about the assumption of the consistency of the underlying theory. However, one of them removed the word "apparently" from "PA is consistent".

Looking at the article, it asserts uncritically that PA is consistent in at least two places. I don't personally have any serious doubts about that proposition, but it is possible to doubt it without being entirely ridiculous, and there is a small minority of serious mathematicians who do doubt it. I think we should acknowledge this position somehow, but I don't have immediate clarity on the best way to do it. --Trovatore (talk) 17:10, 31 May 2019 (UTC)

Huh. Actually it looks like I was confused about what I accepted. The first two revisions were actually adding skepticism rather than removing it; the third removed redundancy. Question is still open about the best way to handle this. --Trovatore (talk) 17:26, 31 May 2019 (UTC)

Right now, I think it's trying to hit that particular nail a little too hard. Saying it three times in as many sentences reads like there is much more doubt about the issue than I think there actually is. In particular, the second parenthetical comment, "(if it's really consistent as it seems to be)" could be read as somewhat dismissive. Also, "apparently" in the first sentence might be read as saying that it may appear to be, but in fact is not. I understand (I think) where the editor was coming from, if we dismiss the consistency proofs that go beyond finitistic methods, at any rate. Ideally we would open by saying it is "generally believed to be consistent", though that would require some citations. Pending that, perhaps something like:

The theory of first order Peano arithmetic seems to be consistent. Assuming this is indeed the case, note that it has an infinite but recursively enumerable set of axioms, and can encode enough arithmetic for the hypotheses of the incompleteness theorem. Thus by the first incompleteness theorem, Peano Arithmetic is not complete. The theorem gives an explicit example of a statement of arithmetic that is neither provable nor disprovable in Peano's arithmetic. Moreover, this statement is true in the usual model. In addition, no effectively axiomatized, consistent extension of Peano arithmetic can be complete.

In any case, we may want to change the second "Moreover" in the paragraph as it currently stands. 22:05, 31 May 2019 (UTC)

I took the easy way out and just copy-pasted your version into the article. It at least seems like an improvement over what was there. --Trovatore (talk) 01:50, 1 June 2019 (UTC)

Okay; I've put back the two links that were in the original paragraph that I omitted above (to Peano arithmetic and to model). Magidin (talk) 02:23, 1 June 2019 (UTC)

Adding a proof generalization based on The Hilbert–Bernays conditions

I think it is in place to add a generalization of the proof of both theorems, based on the Hilbert–Bernays conditions and the diagonal lemma, due to the following reasons:

1. These are arguably important generalizations and the proof do not depend on the details of the specific theory.
2. As for the question whether it is too detailed, proof sketches are given in the article anyway, and the one given for the 1st theorem is already quite elaborated. However, using the the Hilbert–Bernays conditions and the diagonal lemma the proof is much much shorter than the proof sketch.
3. These proofs give a good idea of how to use the language/notations of the Hilbert–Bernays conditions in this context.

I have made such an edit which was reverted by User:Trovatore, which I am not sure was the best way to handle the issue.

Opinions? Dan Gluck (talk) 22:52, 13 July 2020 (UTC)

One possibility is to write the proof in the very short Hilbert–Bernays provability conditions article, which then shows how these conditions are actually used, and only refer to that here. As the current (Gödel's incompleteness theorems) article is quite lengthy and might actually need a severe diet, this could be a good idea. But I'ld love to hear other opinions as well. Dan Gluck (talk) 22:57, 13 July 2020 (UTC)

It shouldn't say most mathematical proofs are written in natural language

They're not, they're written in "mathese", where even relatively simple things are so obsfucated by postsecondary education-level (or almost) jargon that even an educated young adult genius (non math-major) might need many multiples of the reading time just to translate it. i.e. what does nu subscript xi2 stand for, what's this symbol, what's this word, what's the math-only meaning of this word? Etc, etc. Even legalese is probably closer to natural language than modern math proofs and some legaleses come with a (non-binding) natural language "translation". The purpose of that text portion seems to be to make a distinction between proofs by humans and computer-assisted proofs (presumably ones so painstaking to check well (machine code too!) that it wasn't done). There must be a good way to state that without claiming that most mathematical proofs are written in natural language. Sagittarian Milky Way (talk) 19:07, 25 February 2021 (UTC)

The definition of "natural language" is: a language that has developed naturally in use (as contrasted with an artificial language or computer code) (Oxford). Wikipedia describes it as "any language that has evolved naturally in humans through use and repetition without conscious planning or premeditation. Natural languages can take different forms, such as speech or signing. They are distinguished from constructed and formal languages such as those used to program computers or to study logic." What you describe as "mathese" is in fact a natural language under this definition. You seem to be suggesting that "natural language" is supposed to means something like "language that can be easily understood". Alas, that is not what it means. Magidin (talk) 21:52, 25 February 2021 (UTC)

Why are the equations not natural language if they are logic but are always natural language if they are a different field of mathematics? Okay I'm being too harsh, there are still sentences in math proofs but (correct me if I'm wrong) the equations are needed to follow what's going on right? Maybe not every last equation but often (the simplest alienese I've seen is an entire glyph-dense article on the tautology that an ordered set member or real number is either above, equal to or below another one, there was a long string of Byzantine glyphs just to say "if {x, y} in ℝ, x<y or x=y or x>y". What's wrong with saying something more Englishy like that instead of alienese?) Sagittarian Milky Way (talk) 00:30, 26 February 2021 (UTC)

They're written in natural language as opposed to, say, first-order logic. I think this is a reasonable distinction to make, and a reasonable way of putting it. I wouldn't object to an explanatory footnote pointing out that this is not the same thing as layman's language, if you really think this is a likely confusion on a reader's part. --Trovatore (talk) 01:02, 26 February 2021 (UTC)

Ah I see, it's not that this is one of the few where they took the effort to check for human bugs with computer and presumably painstakingly checked the binary maybe even hardware for bugs. They rewrote anything not in fundamentalest-possible logic into a thing so basic logic-y and probably verbose that an algorithm can spit out true or false just fromfollowing logic equations and making sure none of those Greek philosophy laws and stuff are violated. Not everyone would be interested enough to follow the links like automated theorem proving thus this interesting point could be unrealized by them. Could you say something to the effect of this is one of the few theorems that have been broken down into raw first-order logic for automated proving most are written in traditional human-friendly/-readable mathematics while most (including the original) are written in traditional human-friendly/-readable mathematics? Maybe natural language is a traditional phrase in mathematics (?) and likely most readers have seen enough alienese to not think it's just sentences at the highest level but they will think your idea of how dense a natural language can be is weird. Even if natural language is very barely technically correct, a correctness that is ironically not the plain English meaning of natural language. Sagittarian Milky Way (talk) 02:10, 26 February 2021 (UTC)

Your naive ideas of what computer proof assistants can handle have caused your description of this process to be inaccurate, so you're kind of missing the point. It is not necessarily broken down into more basic steps; it is, however, written in a more formalized and artificial language. It's like if I said, in English, that it doesn't matter what order you add two real numbers, their result will be the same, or if I wrote using logical notation $\forall x\in \mathbb {R} :\forall y\in \mathbb {R} :x+y=y+x$. The two things I might say mean more or less the same thing as each other, at similar levels of detail, but one is in a precise formalized language more easily read by computers and one is in natural language more easily read by people. You might also note that the formalized version is actually less verbose than the human version, not more. The point that you're missing is, this computer verification step leads to greater belief in the reliability of the same proof, because it's not the proof that had to be changed to make it verifiable, it's just the language it was written in. —David Eppstein (talk) 02:58, 26 February 2021 (UTC)

I see, a flaw does seem to have a slightly higher chance of sneaking through when the proof is partly words than when it's fully in logic glyphs and checked by computers. And now I know what upside-down A and tridents ∈ ∉ ∋ mean, heck if they're all this easy then maybe they're not so bad, maybe I could learn a few of the ones under the edit box a day. Sagittarian Milky Way (talk) 04:14, 26 February 2021 (UTC)

"Maybe natural language is a traditional phrase in mathematics (?)" Actually, the term comes from linguistics, not mathematics. Again, it is to distinguish regular languages that arise and evolve naturally, from artificial and created languages, like elvish, klingon, or esperanto; and from computer languages. The term includes technical, even highly technical, discourse, provided it takes place in the context of a natural language (like technical medical language being spoken in English; but not technical medical language being spoken in Esperanto). It does not mean "jargon free and accessible to a layman without any effort or knowledge". Magidin (talk) 17:27, 26 February 2021 (UTC)

That does expose a possible flaw in the presentation, though — we really aren't trying to distinguish mathematical English from mathematical Esperanto. Esperanto would also count as a "natural language" in the meaning we're trying to get at here. The point we want to make is that proofs are appeals to human reasoning, presented in human language, showing the reader/listener a path of reasoning that (barring mistakes or bad initial assumptions) leaves no room for doubt. This is as opposed to formal string manipulations in (say) Hilbert-style or Gentzen-style predicate calculus, which do not require thinking about their meaning at all in order to verify them. I'm not sure what the best way to get this across is. I don't quite agree with David that it's just a different language. --Trovatore (talk) 19:19, 26 February 2021 (UTC)

Mathematicians don't have a term of art or traditional word or phrase for logic element crunching in general? Like Boolean algebra, those Greek logic laws transcribed to formal p's, q's, if symbols etc... Sagittarian Milky Way (talk) 19:45, 26 February 2021 (UTC)

What does "logic element crunching" mean? For that matter, what does "logic element" mean? And what does this have to do with your initial request/complaint/edit suggestion? It all seems to be rooted in you misunderstanding the phrase "natural language" to mean "non-technical and jargon-free". Having cleared up this misunderstanding, is this just devolving into whether mathematics uses symbols and words that don't mean what you think they do or should mean? Also, that's not what "Boolean algebra" means, either. Magidin (talk) 21:07, 26 February 2021 (UTC)

It's clear SMW is not a mathematician; I don't think we need to keep pointing that out. Let's see if we can clarify the point being made. Do we first agree what point we actually want to make? I really don't think that point, whatever we agree on, would make any distinction between English and Esperanto, which possibly makes the phrase "natural language" problematic. --Trovatore (talk) 21:51, 26 February 2021 (UTC)

I called the logic symbols "logic elements" cause I don't know the answer to numeral:number::logic symbol:(proper mathematical name for these things). Operations (or manipulations or whatever the proper term is) being done on numbers is sometimes informally called number crunching so whatever the proper analogous term is for operations that can be done on logic thingies seems to be the important point Trovatore is mentioning rather than constructed vs natural language. And Boolean algebra is only one kind of logic symbol crunching, one of the few I've heard of, I do not know if the proof even used Boolean. Sagittarian Milky Way (talk) 22:47, 26 February 2021 (UTC)

".... were written in a way intended for human readers"? Magidin (talk) 22:10, 26 February 2021 (UTC)

Works for me. --Trovatore (talk) 22:12, 26 February 2021 (UTC)

Sounds good. Sagittarian Milky Way (talk) 22:47, 26 February 2021 (UTC)

The Paulson 2013 reference makes a stronger related point, that Gödel himself was philosophically opposed to exactly the sort of formalization of proof that was done in this case to his proof. —David Eppstein (talk) 23:58, 26 February 2021 (UTC)