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

Archive 5

←

Archive 8

Archive 9

Archive 10

Archive 11

"theorems" vs "proofs"

had this thought..nitpicky lol but for sake of accuracy, I suppose....the theorems are technically statements of what the proofs demonstrate...and the proofs are the actual demonstrations...is this right? so like in that first sentence (and throughout where "show" etc is used instead of "demonstrate"): "Gödel's incompleteness theorems are two theorems of mathematical logic that demonstrate..." "demonstrate" should technically be "state"...?? or technically rewritten to something like, " Gödel's incompleteness theorems are formulations of two proofs in mathematical logic that demonstrate...." ...perhaps much ado about nothing...but maybe matters if indeed making an obvious language error right off the bat..68.48.241.158 (talk) 16:04, 19 March 2016 (UTC)

I partly created the problem btw by suggesting "demonstrate" instead of "establish" in first sentence (still think "establish" is poor though) ...but there are instances throughout where "show" etc is used in reference to the theorems, instead of the proofs themselves.. 68.48.241.158 (talk) 16:13, 19 March 2016 (UTC)

It's normal to use the words "show", "demonstrate", and "establish" for theorems. As long as we don't say that the theorem *is* a proof, I think we should be OK here. — Carl (CBM · talk) 18:27, 19 March 2016 (UTC)

odd revert

Trovatore reverted this entirely factual statement (and helpful within the confines of an encyclopedia, I think):

"It is important to note that this sentence (or "string") is purely syntactical and composed entirely of formal symbols, and should, therefore, not be thought of as a "sentence" in the normal sense of the word."

His reasoning was, "what? No, it is not purely syntactical, and it is indeed a sentence in the normal (math-logic) sense of the word)"......the "it is not purely syntactical" statement is very odd as, of course, the proof (and the string that's referenced here) is by definition entirely formal and syntactical...what gives????68.48.241.158 (talk) 02:15, 3 April 2016 (UTC)

The statement I removed is false. The sentence is not "purely syntactical"; it has a completely standard meaning interpreted as a statement about the natural numbers. It is not just a string of characters — it means something. --Trovatore (talk) 03:25, 3 April 2016 (UTC)

On the one hand, the Goedel sentence of a theory is written in the formal language of the theory, as we all know. So in some sense it is syntactical. However, it also does express a fact about the natural numbers, like every sentence in the language of arithmetic. To me, the language that was removed from the article does have an issue, in that it is not clear why the reader should remember not to think of the Goedel sentence as a sentence in the normal sense of the word. To analyze the truth of the Goedel sentence (in the metatheory), treating the Goedel sentence like any other mathematical proposition is exactly what we do. Also, as a tangent, the language "it is noted" is usually a sign that the text can be rewritten in some way, to have a more encyclopedic tone.

I'd like to ask the IP editor to chime in with the concern that the sentence was intended to convey about viewing the Goedel sentence as a sentence. If the language was taken from some book, I'd be glad to look at that to see the context. — Carl (CBM · talk) 12:13, 3 April 2016 (UTC)

the statement is meant as quick summary/clarification for the encyclopedia reader...who might easily get confused by what "sentence" is meaning in this context....I don't know, I can try to find a reference but seems utterly uncontroversial to me....the sentence or "string" is, of course, entirely formal (ie meaningless symbols) and the rules of string manipulation are, of course, entirely formal and syntactical...a computer program can make strings all day long without a care in the world about "meaning."....the interpretation of "meaning" involves a meta-analysis....this is very basic stuff in this topic...I think this involves confusion about what a "formal system" is..which should be more carefully explained in this article...68.48.241.158 (talk) 13:15, 3 April 2016 (UTC)

article woefully in need to a stand alone section "Formal Systems" or some such thing...never seen a book or introduction on the topic that didn't spend a lot of time explaining this core concept, it's like explaining general relativity without explaining...well, I don't know what the analogy is...but anyway..68.48.241.158 (talk) 13:28, 3 April 2016 (UTC)

I don't need a reference for the removed sentence, I only thought you might have been quoting from one.

Because the Goedel sentence is about numbers, though, it is not entirely "meaningless" symbols - which is why we can prove that the Goedel sentence is actually true. Yes, of course, that involves an analysis in the metatheory, but such an analysis must rely on the "meanings" of the symbols, as far as I can see. The proof is not entirely syntactic exactly for this reason (we can demonstrate the unprovability of the Goedel sentence syntactically, but not its truth). The "background" section has a paragraph on formal systems, and I think that section is where background information on formal systems belongs. You had previously argued (above) that the section should be deleted... — Carl (CBM · talk) 13:32, 3 April 2016 (UTC)

At the same time, this is an encyclopedia article, not a textbook. So we can't and shouldn't try to have an entirely self-contained presentation of everything that begins with no assumptions. Most background material should just be briefly summarized, while the material directly about the incompleteness theorems should be written in more detail. — Carl (CBM · talk) 13:34, 3 April 2016 (UTC)

well, the deleted sentence avoids the word "meaningless" anyway to avoid controversy...so what it does state are simply facts.."It is important to note that this sentence (or "string") is purely syntactical and composed entirely of formal symbols...." this is a statement of pure fact; it's not even contestable, you'd agree, right????....so, what's the problem? I suppose one could feel it's unhelpful to the encyclopedia reader...not sure why though......and I guess I just felt the background section would be more background if it included a bit of historical context, perhaps idk...for the general reader....but this article would certainly be improved if somebody created a section explaining what a formal system meant in the context of this topic...this topic is itself meaningless (particularly to the general reader) if not understood in the realm of "formal systems" and "formal provability"....68.48.241.158 (talk) 13:57, 3 April 2016 (UTC)

I didn't remove the sentence, but I think that Trovatore may have noticed the claim that the Goedel sentence "should not" be thought of as a sentence in the "normal sense" of the word. To the extent that the normal meaning of the word "sentence" in mathematical logic is a formal sequence of symbols, the Goedel sentence should be thought of as a sentence. Moreover, I suspect Trovatore does not want to downlplay the fact that the Goedel sentence expresses a meaningful statement about the natural numbers (so it is like a 'sentence' in the more informal sense of 'meaningful statement about mathematics'). I thought that the phrase that was removed from the article did start to move too far in taking a position towards formalism, while the article here should be neutral, but I didn't think it was too far yet. Whether the reader "should" or "should not" view the Goedel sentence in some way is something the reader should usually decide for herself. I would be glad to expand the background section with about one more paragraph that summarizes the idea of a formal system for arithmetic. But it would be out of place for us to have hundreds of words trying to formally define a "formal system" in the way that a set of lecture notes would - we should just summarize here. — Carl (CBM · talk) 14:27, 3 April 2016 (UTC)

Idk seemed an odd revert out of the blue with a stated reason that on its face suggests an erroneous understanding of a particular aspect of the topic...all it was doing was clarifying in a factual way what is technically meant by "sentence" in this context and distinguishing this from a nontechnical use of the word "sentence"..to aid the general reader...I think Travatore was partly misreading/misunderstanding the sentence (ie reading way too much into it) and partly, perhaps, slightly misunderstanding this aspect of the topic...that is, not understanding the inherent and intentional internal meaninglessness (or formalness) of the systems involved (ie 100% formal and syntactical)...so think the sentence benefits the article in an uncontroversial way and shouldn't be struck, particularly for an on its face erroneous reason ("it is not purely syntactical")...so I vote to keep it, you're sorta okay either way...would need a couple others to weigh-in, I guess....68.48.241.158 (talk) 17:55, 3 April 2016 (UTC)

btw just noticed your edits to background along these lines...quite good..perhaps a few more sentences in this regard may be in order eventually68.48.241.158 (talk) 18:05, 3 April 2016 (UTC)

this is well put by Braithwaite: "..what he proves in Proposition VI is a result about the calculus and not about what the calculus represents, for what it directly establishes is that neither of two particular formulae can be obtained from the initial formulae of the calculus by the rules of symbolic manipulation of the calculus. If the calculus is interpreted (as it can be interpreted) so that it represents the arithmetical part of the Principia Mathematica...." Calculus a synonym for formal system here....anyway, I'd like to perhaps try clarifying this notion in the article somewhere (as it trips people up, including myself at one time) perhaps using this cite....68.48.241.158 (talk) 19:20, 3 April 2016 (UTC)

The claim that the sentence is "100% formal and syntactical" is simply false. There is no misunderstanding here; Braithwaite is just wrong. The sentence is about natural numbers. --Trovatore (talk) 20:20, 3 April 2016 (UTC)

Oh, wait a minute, here is a possible point. The Goedel sentence is about the natural numbers, no matter what the objects of discourse of the theory in question are. That could be what Braithwaite is talking about, albeit disguised as talking about the formulas. In that case he's not wrong, but it's phrased very unfortunately. --Trovatore (talk) 20:24, 3 April 2016 (UTC)

he's not wrong at all...you're confusing two things..the formal system itself (and how it works), and the interpretation of the formal system...nobody is disagreeing that said system can be interpreted as being about the natural numbers; that's the only reason it's of interest, actually....idk you seem to be confused in the same way as I was once confused about this difference...68.48.241.158 (talk) 20:32, 3 April 2016 (UTC)

I am not confusing anything at all; I understand this material quite well. --Trovatore (talk) 21:21, 3 April 2016 (UTC)

you're displaying a confusion about "formal systems" in the context of this topic (it confuses a lot of people, including smart and learned people as yourself)...I can't try to explain it to you here beyond what I wrote in my last post...the famous Nagel and Newman book carefully explains it, if you're interested...I'll add this though: the Gödel sentence isn't itself about anything at all (it's just a formal construct)...it can be interpreted, however, as being about the natural numbers.. 68.48.241.158 (talk) 00:30, 4 April 2016 (UTC)

I am not confusing anything. You are just wrong. --Trovatore (talk) 01:34, 4 April 2016 (UTC)

OK, sorry, maybe that's not helpful. But please do me the courtesy of realizing that I understand the material quite well. There is nothing you need to "explain" to me about the material itself.

It is true that the reasoning about provability of the sentence does not involve the objects of discourse of the formal theory under consideration. If that is what you mean, that is a valid point. But the way you expressed it does not get that across. --Trovatore (talk) 01:42, 4 April 2016 (UTC)

nothing personal but I can't just realize you understand the material quite well when you continue to make odd and erroneous statements like, "the claim that the sentence is '100% formal and syntactical' is simply false." ...as the sentence or string is BY DEFINITION 100% formal and syntactical...if you don't understand this, then look into it...if you refuse to understand this, you're simply being unhelpful...68.48.241.158 (talk) 02:33, 4 April 2016 (UTC)

That claim is in fact simply false. --Trovatore (talk) 02:51, 4 April 2016 (UTC)

To me the intended connotation (whether or not it is the actual literal meaning) of "100% formal and syntactical" was "arbitrary string of symbols divorced from any meaning as a description of the behavior of the integers". Which is, as Trovatore says, a very misleading way of thinking of the Gödel sentence. —David Eppstein (talk) 02:52, 4 April 2016 (UTC)

well, let's stick to the literal meaning please...as the string is literally and by definition 100% formal and syntactical.....instead of inventing a silly connotation....68.48.241.158 (talk) 02:58, 4 April 2016 (UTC)

OK, why don't you try rewording what you mean by "100% formal and syntactical"? As far as I can see, this claim is in direct contradiction to the claim that it has something to do with its meaning as a description of the behavior of the integers.

You may have had something correct in mind; I made an attempt at rephrasing that: "The reasoning about provability of the sentence does not involve the objects of discourse of the formal theory under consideration". Is that what you meant? If not, then what? --Trovatore (talk) 03:36, 4 April 2016 (UTC)

I don't actually know what it would literally mean for a string to be "100% formal and syntactical". That's why I discussed its connotation rather than its literal meaning above. Is it possible for a string to not be "100% formal and syntactical"? What is the difference between the ones that are and the ones that aren't? How does inserting this phrase into our article aid reader understanding? —David Eppstein (talk) 04:21, 4 April 2016 (UTC)

Yeah, thanks David, that might be a more fruitful line of inquiry. Of course formal sentences are formal sentences; that's a tautology. The Goedel sentence happens to have a preferred natural interpretation, which the disputed language appears to be denying. Maybe that was never the intent?

How about it, 68? What would be an example of a sentence that is not "100% formal and syntactical"? --Trovatore (talk) 05:21, 4 April 2016 (UTC)

right, the string is formal and syntactical because it is formal and syntactical by defintion...it is a tautology...what you reverted was simply reminding the general reader of this simple fact...you kept trying to argue that this simple fact was somehow wrong...which is what was so odd....nonetheless it seems you have difficulty with the distinction between the internal meaninglessness (ie formalness) of a formal system on the one hand and the act of interpreting it in a particular manner from outside the system on the other....this concept isn't even part of what you reverted anyway.. 68.48.241.158 (talk) 11:03, 4 April 2016 (UTC)

It's formal, but it's not "internally meaningless". It's not meaningless, ever. It has a canonical, preferred interpretation. --Trovatore (talk) 17:45, 4 April 2016 (UTC)

you have to look at where it's placed in context to see why it's helpful to the general reader...as the section is paraphrasing things in ordinary English and then talking about G as a "sentence" etc...so we're alerting the reader that "sentence" here actually has a technical meaning and shouldn't be confused as some kind of ordinary language paraphrase or statement..an additional problem is the use of the word "sentence" itself...it would be better "formula" or "string" or "proposition" or "formal proposition"...because "sentence" is obviously going to confuse the general reader...but either way the terminology should be consistent throughout the whole piece...68.48.241.158 (talk) 13:35, 4 April 2016 (UTC)

so I propose putting the following sentence back in (which I've slightly modified): "It is important to note that this sentence (or "string") is a construct of entirely formal logic and should, therefore, not be thought of as a "sentence" in the regular sense of the word." It's a statement of fact and it's at least a little bit helpful in context to the general reader...so I think the philosophy of Wikipedia would certainly side on including it instead of reverting it....and then hopefully we can put this nonsense of arguing about nothing behind us.....68.48.241.158 (talk) 14:05, 4 April 2016 (UTC)

No, I'm sorry, I still don't agree at all. It is not in fact important to note that, and it is not helpful to the general reader. It is more likely to suggest to the reader that the Goedel sentence is meaningless, which it is not. --Trovatore (talk) 17:40, 4 April 2016 (UTC)

"Trovatore" deleting valid and helpful content because "he doesn't agree with it"

added most of this paragraph to Background, Trovatore (who has demonstrated a poor understanding of some of the concepts) deleted most of it because he doesn't agree with it....He's becoming problematic to the project...he wants to delete things that are uncontroversial summary because he doesn't understand them....and causes a long talk thread because he can't understand (or refuses to understand) the most basic of concepts (ie formal strings=formal strings)....I may have to see about requesting input from others, as I don't think CBM or Eppstein really want to side against their Wikipedia friend (even though I think CBM behaves quite competently on this topic)....and I don't think too many others (if anyone) are paying attention to this.... " In general, a formal system is a deductive apparatus that consists of initial strings of symbols (the “axioms”) and rules of symbolic manipulation (or rules of inference) that allow for the creation of new strings. By definition formal systems lack content and are entirely formal exercises. However, a formal system may be intentionally designed so that it will simultaneously mirror and allow for interpretation about some other phenomena. One example of such a system is first-order Peano arithmetic, a system in which all variables are intended to denote natural numbers. In other systems, such as set theory, only some sentences of the formal system express statements about the natural numbers. The system relevant to Gödel's theorems was designed to mirror whole number arithmetic so as to explore the possibility of Hilbert's program."68.48.241.158 (talk) 18:13, 4 April 2016 (UTC)

Let's try to dial back the emotions a bit. It's hard for me too, but I'll try if you will.

I object strongly to "[b]y definition, formal systems lack content". It is true that the content is not contained within the formal system itself, as it were. But some languages have an intended interpretation, and the language of arithmetic is certainly one of these. To say it "lacks content" seems to be to deny that.

It is true that the intended interpretation of the language of arithmetic is not involved in the reasoning about formal derivability of formal theorems in the language of arithmetic. However, that is not the same as to say that the language of arithmetic lacks an intended interpretation, aka meaning. --Trovatore (talk) 18:32, 4 April 2016 (UTC)

I mean it's all right here for you, clearly laid out..if you really want to understand what a formal system is/its definition...there's no controversy as to defining such...I won't personally respond to you along these lines anymore though...it isn't helping anything...others would have to try..http://www.britannica.com/topic/formal-system 68.48.241.158 (talk) 19:05, 4 April 2016 (UTC)

You really don't have to explain formal languages or formal deductive systems to me. I understand them quite well. It's true that their standard definitions are noncontroversial well, I should be careful; almost everything has some controversy somewhere; let's say "not noticeably controversial". It is also true that those definitions do not actively assert meaninglessness or lack of content. Certainly the one you pointed me to at Brittanica does not; I made a point of checking before responding.

So that by itself refutes your claim that "by definition" they lack content — the lack of content is not included in the definition. You might say that the definition does not assert that they have content; that would be true, but I don't think it would be useful to say at that point in the text. --Trovatore (talk) 19:16, 4 April 2016 (UTC)

i'll take the bait one last time (but this isn't the place for discussion..and you're the one challenging uncontroversial statements...quotes from Brittanica: Models—structures that interpret the symbols of a formal system—are often used in conjunction with formal systems. (this is what my paragraph explains)... In an axiomatic system, the primitive symbols are undefined...In general, then, a formal system provides an ideal language by means of which to abstract and analyze the deductive structure of thought APART FROM SPECIFIC MEANINGS. Together with the concept of a model, such systems have formed the basis for a rapidly expanding inquiry into the foundations of mathematics......"the concept of a model" is the separate interpretation part...this is tripping you up...68.48.241.158 (talk) 19:26, 4 April 2016 (UTC)

Nothing is tripping me up. I also understand models, interpretations based on models, and the distinction between these and formal languages and deductive systems.

The "apart from specific meanings" quote from Brittanica is fine; it still does not justify your text.

Let me speak to my larger concern here; I've avoided it so far because it might just provoke more emotional argument, but maybe it will help. There is a strange social phenomenon whereby many people come to the Goedel theorems with a preconception they've picked up from popularizers or I don't know where. The preconception is that the Goedel theorems somehow support the foundational philosophy of formalism.

In fact, the theorems make formalism (and logicism) more difficult to sustain, not less. They actually work in support of realism ("Platonism", if you like), not by making any of the difficulties of realism lighter, but by handicapping its main competitors without affecting realism at all. (I've left out intuitionism, which I see as a variant of realism, albeit a crippled one. The theorems don't really hurt intuitionism either, but they also don't make it any less crippled.)

So we have to be very careful to avoid reinforcing this preconception through incautious claims that particular sentences are "meaningless". --Trovatore (talk) 19:35, 4 April 2016 (UTC)

^philosophical implication stuff not relevant here...I'm just relaying facts about how the proof works (there's no opinion content in my paragraph)..68.48.241.158 (talk) 19:46, 4 April 2016 (UTC)

Yes, there is. You actively assert that "by definition", formal systems have no content. That is not true. What is true is that the definition of the formal system does not mention any content, that no content is necessary to the definition. But that is not the same. --Trovatore (talk) 19:49, 4 April 2016 (UTC)

RfC Formal System

user "Trovatore" is disallowing content relating to the straightforward/uncontroversial definition of "formal system"...his statements in the above two sections demonstrate on their face that he doesn't understand/refuses to understand the difference between the formal system itself on the one hand and the interpretation of the formal system on the other....(this is a crucial and well-understood distinction in the realm of this topic which needs to be explained in the article)...he also doesn't/refuses to understand that formal systems are indeed formal...his motivation seems to be in part based on his personal philosophy about the topic (as can be seen in his final long post in previous section) which is inappropriate in the confines of Wikipedia...Here's a link to Britannica explaining the definition of "formal system" if that's helpful...http://www.britannica.com/topic/formal-system

(note: I don't think "Trovatore" has ill-intent but that he's just gone off course on this particular aspect of the topic...but it's disruptive as he's putting up a roadblock to the addition of helpful content)..

Also, someone let me know if I've done this RfC thing wrong.....68.48.241.158 (talk) 13:06, 5 April 2016 (UTC)

• Comment Removed RfC tag for now. Question completely unclear. Please see Wikipedia:Request for comments for example RfC questions. Kindly re-start a new RfC with a clear question without assuming access to other sections of this talk page and without any attack/criticism of any editor.. Spirit Ethanol (talk) 13:11, 5 April 2016 (UTC)

hmmm...this is odd...you're disallowing others from commenting? the problem requires "criticism" as his against policy behavior (removing things based on personal philosophy etc) is part of the problem....what do you suggest??? my request if for others to weigh-in to get consensus as to what a "formal system" is...which shouldn't be difficult as the definition is well-understood/uncontroversial...so that he can't disrupt things based on his erroneous understanding of it.....????68.48.241.158 (talk) 13:36, 5 April 2016 (UTC)\

and you're suggestion that I "attacked" him is COMPLETELY not in the record and totally ridiculous...this suggests you may not be unbiased here (you've recently been involved in this article...and probably know this "Trovatore"...)...68.48.241.158 (talk) 13:44, 5 April 2016 (UTC)

For what it's worth, I agree that 68 has not "attacked" me per se. I do not, however, appreciate the claims that I don't understand the subject matter, which I do. --Trovatore (talk) 04:12, 6 April 2016 (UTC)

Of course we don't understand the question. We may understand how scholars understand the subject matter and context, but it appears that the unregistered editor has his own concept that he hasn't explained in the usual scholarly terms, and so we can't understand. Maybe it is a waste of time for him to try to communicate with us (but, if so, a waste of Wikipedia time and pixels). Robert McClenon (talk) 10:59, 6 April 2016 (UTC)

If the question is not clear, you can't expect to get answers. For widest community participation, I advise you to further refine question, and add examples if possible. Spirit Ethanol (talk) 18:24, 5 April 2016 (UTC)

RfC formal system

The following discussion is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

---

For the benefit of adding new information to this article, can consensus be reached that "formal systems" are 1. entirely formal and consist of only formal content..and 2. that there is a distinct difference between the workings of a formal system on the one hand and interpreting the formal system on the other (which involves interpretive modeling)...???? here's link to Britannica definition if helpful: http://www.britannica.com/topic/formal-system 68.48.241.158 (talk) 14:54, 5 April 2016 (UTC)

No because I have no idea what this is trying to say, other than this particular editor appears to want to filibuster this talk page by poorly defined complaints. I won't object if another editor pulls the RFC tag becaue this RFC is incomprehensible as written. Robert McClenon (talk) 16:46, 5 April 2016 (UTC)

I assume that this unregistered editor has an ulterior motive for posting this, but I am not sure what it is. If this unregistered editor posts any more bizarre or obscure posts here, I will request semi-protection so that to allow registered editors who understand the theorems to discuss improving the article without being shouted down. Robert McClenon (talk) 16:46, 5 April 2016 (UTC)

certainly this question makes no sense if you are not familiar with the concepts involved with this topic...but you shouldn't comment if you're not...there's guidelines about that in the article about RfC....if we end up getting some substantive input can I request that the above vote not be counted as it doesn't address the substance in any way whatsoever..and acknowledges not understanding the question...68.48.241.158 (talk) 17:18, 5 April 2016 (UTC)

note too in the history that I've made dozens upon dozens of beneficial contributions to this article...so don't really appreciate the ulterior motive accusation...68.48.241.158 (talk) 17:19, 5 April 2016 (UTC)

Oppose. This goes too far in trying to convey the point of view that these systems are meaningless symbol-manipulation, a point of view that I disagree with. —David Eppstein (talk) 17:55, 5 April 2016 (UTC)

totally fine..expect you and Trovatore to stick to your positions and be counted in the vote...hope to get some other knowledgeable people who haven't been involved to weigh in substantively too, whichever way they do....(I continue to be thrown by all this concern about what facts might convey to people, as opposed to just worrying about stating the facts)..68.48.241.158 (talk) 18:00, 5 April 2016 (UTC)

Okay. I am a neutral editor that just stumbled upon this. I haven't been biased in any way before reading this. Now, I'm no extreme math expert, but I'll weigh in. I have to agree with David and Robert on this one. You have repeatedly complained about an editor editing in Good Faith that did something you didn't like. It seems to me as if you have avoided many valid points by very experienced editors by dismissing them as "unrelated." This talk page now consists of 90% your rantings and other's responses to them and 10% actual constructive criticism and comments. So oppose to your RfC and I agree that you should just drop this. Taking it to the Help Desk was taking it too far. Those are my views and I would ask that they not be degraded or dismissed. Thank you, Fritzmann2002 19:04, 5 April 2016 (UTC)

I don't understand the point of the question. You've presented only one side of the dispute in a very non-neutral way, and in a way that seems to be manipulating the consensus building system. You seem to be WP:FILIBUSTERing this talk page, and you're not clearly presenting the dispute such that an outside editor can meaningfully contribute. —  crh ₂₃  (Talk) 19:14, 5 April 2016 (UTC)

I don't really know how to deal with this...3 people have now weighed in on a specific and technical question in a completely unsubstantive way...they practically admit they don't know the first thing about the topic....you're NOT suppose to weight-in like this according to the RfC guidelines!! it's filling up the thread and ruining it....just don't weigh in and allow time for others to weigh in substantively....do I have a recourse if this keeps happening??68.48.241.158 (talk) 19:26, 5 April 2016 (UTC)

• Comment. I do not think it is correct to say, in absolute terms, that formal systems are purely a formal exercise that is devoid of content. As an encyclopedia, we should summarize notable perspectives, according to their weight in reliable sources. Philosophers have written screeds on the implications of this theorem, so we should summarize what they have to say, not conduct our own original research in discussing our own personal views on formal systems. Trovatore has in the past articulated that Goedel's incompleteness theorems are more consistent with mathematical realism than formalism. I would say that he is right, at least as far as the kind of "naive formalism" that is being presented in this RfC. Trovatore and I have clashed in the matter of personal philosophy in the past. I disagree with the view that the incompleteness theorem necessarily gives evidence of mathematical realism. I do not think "mathematical realism" is meaningful, any more than "musical realism" or "poetic realism" are. No one will ever exhibit a "real" triangle, or produce a "real" number. They are idealizations. Mathematics is an activity performed by human beings. Sławomir
  Biały 19:22, 5 April 2016 (UTC)

the idea is to explain that they are intentionally fabricated to be just this (formal); that they are just this by definition....but to then explain how the concept of 'content' later comes in....but Trovatore objects to even this first part....so I'm only worried about the definition of a formal system...does this change your sense on this at all, Sławomir
Biały(trying to alert that guy but don't know how) ??68.48.241.158 (talk) 19:40, 5 April 2016 (UTC)

so maybe I should've better explained what I'm trying to achieve with this consensus...too late now though...already got all kinds of people mad at me for even trying to request comments...don't think I can try a new RfC now....68.48.241.158 (talk) 19:58, 5 April 2016 (UTC)

Is there agreement, among all except the unregistered editor, that this RFC will never improve this article, and so should either have the RFC tag removed or should be "closed as uncloseable" (incapable of being closed by an experienced editor with appropriate knowledge of the subject after 30 days of discussion)? Robert McClenon (talk) 20:21, 5 April 2016 (UTC)

it's only been open for a few hours a two people have already taken the time to respond substantively....a few others have responded inappropriately according to the RfC guidelines, including yourself...so this line by you is inappropriate interference and just mischief...you don't understand the topic or the question...your involvement is inappropriate...68.48.241.158 (talk) 20:26, 5 April 2016 (UTC)

I understand the topic of Godel's incompleteness theorems quite well. It is true that I don't understand the question in the RFC, and why it is applicable here rather than at formal systems. Do not tell me that my involvement is inappropriate. That tone on your part is inappropriate. To restate, it isn't clear why you think that this point about formal systems is applicable here. (While formal systems are indeed formalisms, Godel's theorem is more than a formalism. It, and Turing's halting problem, which is Godel's theorem applied to a particular type of abstract system, have deep implications for computability, and some argue that it has deep implications in artificial intelligence and elsewhere. A general question about formal systems is more applicable to formal systems than to Godel's theorem(s).) It is true that some editors have responded substantively, and have said that this has to do with formal systems in general. I see at least four ways forward with some overlap. First, someone can put this RFC out of its misery. It doesn't belong here, even if it does belong in formal systems. Second, we can waste 30 days letting it run, and then have the closer conclude that it cannot be closed in a useful way. Third, a thread can can be initiated at WP:ANI against the original poster. Fourth, this talk page can be semi-protected. Those are what I see. Robert McClenon (talk) 21:02, 5 April 2016 (UTC)

As for me, the matter is simple and clear, and does not involve any philosophy.

(1) Yes, a formal system, given just syntactically, is completely formal. It is either consistent or inconsistent; this property is well-defined on the syntactical level (if we are within first-order logic).

(2) However, in such case the notion "capable of proving all truths about the relations of the natural numbers" is not defined. This is why the first theorem does not apply. It is a theorem about interpreted formal systems.

Similarly, the notion "bounded" applies to sets in (say) a Euclidean space, but not applies to abstract sets. Boris Tsirelson (talk) 20:29, 5 April 2016 (UTC)

so as far as the definition of "formal system" this would be an Affirm right?, Boris Tsirelson (not sure I'm pinging people right, please fix if needed) 68.48.241.158 (talk) 20:33, 5 April 2016 (UTC)

Did I leave any doubt? Again: "This is a theorem about interpreted formal systems". What else to say? Boris Tsirelson (talk) 20:40, 5 April 2016 (UTC)

right but the question is about the definition of a "formal system"...you agree with my (the) definition of a "formal system"??? right...understanding how interpretation is of course involved in the theorems.....Boris Tsirelson68.48.241.158 (talk) 20:50, 5 April 2016 (UTC)

A lot of notions are defined. I am not an expert here. Probably, some authors consider even so much general "formal systems" that even consistency is not defined for these. As noted somewhere above, this is a question to the article about formal systems. To this article, only interpreted formal systems are relevant. Boris Tsirelson (talk) 20:55, 5 April 2016 (UTC)

By the way, you do not need to ping me. This talk page is on my watchlist. Boris Tsirelson (talk) 20:58, 5 April 2016 (UTC)

Oppose. There seems to be an unspoken agenda behind the proposal, and the belligerent tone taken by the anonymous editor is grating. But in any case, the claim that "by definition" a formal system lacks semantic meaning is false. The definition itself does not require a semantic content, but it also does not prohibit there being a semantic content (or multiple semantic contents, e.g., absolute geometry as a formal system that can be modelled in different ways). Though the distinction between syntactic and semantic content of a formal system is relevant to many technical issues (and to avoid misuse of Goedel's Theorem and related items). To claim that the definition of formal system requires that the system have no semantic content would be like saying that the definition of "group" requires that groups be finite (or that elements be denoted by letters). Finally, such additions, if they were accurate and relevant (big if in my opinion) don't belong in this page; they would belong in a page discussing formal systems directly rather than incidentally as it happens here. Magidin (talk) 20:37, 5 April 2016 (UTC)

Oppose. The first question is can consensus be reached that "formal systems" are 1. entirely formal and consist of only formal content. This does not mean anything without an accurate definition of what means "entirely formal" and what is a "formal content". As far as I know, there is no consensus among philosophers about this, and most mathematicians do not care about this. Therefore this RfC is a tentative for deciding a question that is not solved in the literature. Thus it seems that this rfc is intended for getting a consensus about some WP:OR. Therefore, the answer cannot be anything else than oppose. D.Lazard (talk) 20:56, 5 April 2016 (UTC)

Oppose, per the Mathematica page you linked: "A formal system that is treated apart from intended interpretation is a mathematical construct and is more properly called logical calculus". While a formal system can be treated entirely separately from its intended interpretation, it usually isn't. Could you clarify the dispute that prompted this RfC?—  crh ₂₃  (Talk) 21:22, 5 April 2016 (UTC)

yes, their synonyms, particularly back in the 1920s/1930s...that's the point that travatore wouldn't understand..that a system itself is formal and the interpretation of the system is something different (semantical/informal)...68.48.241.158 (talk) 21:39, 5 April 2016 (UTC)

The only thing I was trying to establish was that a formal system is just that, a formal system....Trovatore literally had issues with this and was deleting things based on his problem with this...expecting people would weigh in with the obvious trivial answer that yes, a formal system is just that, a formal system....but people are all confused about what's being asked....partly my fault as I've never done a RfC before....partly the fault of a bunch of people who weighed in inappropriately and muddied up the thread with nothing of substance....but most people aren't answering the simple question but going on long philosophical rants...so Idk....68.48.241.158 (talk) 21:30, 5 April 2016 (UTC)

I think that's the core of the dispute here: you expected the question to have a clear cut answer, but as it turns out, it doesn't. That possibly why Trovatore originally disputed it. Sometimes different things have different meanings to different people, and it is easy to be unaware of the differences, as they can be quite subtle. In fact, that's one of the reasons we use a consensus system here: the sometimes isn't a single answer. Additionally (as with many things in this area of mathematics) it is tricky to avoid straying into philosophy, so some of the arguments may include comments from that field. —  crh ₂₃  (Talk) 21:38, 5 April 2016 (UTC)

the philosophical implications of course don't have clear cut answers...but defining what a formal system is..is trivial...if you go a couple threads back you'll see a paragraph I wanted to insert in bold (which is totally uncontroversial) but trovatore reverted because he doesn't think formal systems are formal systems....68.48.241.158 (talk) 21:43, 5 April 2016 (UTC)

You really need to stop ascribing reasons to others, especially when you seem to do so as a way to engage in backhanded insults. Magidin (talk) 21:47, 5 April 2016 (UTC)

why was your comment necessary? what of substance did it add here? what is it even referring to?68.48.241.158 (talk) 21:59, 5 April 2016 (UTC)

The comment is necessary because you are poisoning the discussion by being purposefully and unnecessarily rude towards other editors. It refers to comments such as "reverted because he doesn't think formal systems are formal systems", "most people aren't answering the simple questions but going on long philosophical rants", "people are all confused", "fault of a bunch of people who weighed in inappropriately and muddied up the thread with nothing of substance." Those comments are belligerent, have absolutely nothing of substance, are rude, and get in the way of discussion. If you can't assume good faith and can't be civil, you shouldn't be here. Magidin (talk) 22:08, 5 April 2016 (UTC)

"because he doesn't think formal systems are formal systems.."....this is literally the problem..he thinks formal systems are somehow more than just formal..when they're entirely formal by definition....this is what this thread is about, this is the point of this thread...he's disrupting the article because of this erroneous belief...I'm trying to help the Wikipedia article by putting an end to this...and yes, this thread did get all confused (and therefore people were confused), as I said, partly my fault in not explaining the issue better and partly the fault of others who behaved inappropriately according to stated RfC guidelines....I can't be accused of being mean to people because I point out that they are behaving inappropriately...68.48.241.158 (talk) 22:25, 5 April 2016 (UTC)

You continue to conclude that because people disagree with you therefore they must be ignorant or lack comprehension. That is not pointing out people are behaving inappropriately, that is you being insulting and obnoxious. And to repeat what you have been told repeatedly: just repeating the same assertion over and over is not an argument, and does not establish your assertion. You claim that "by definition" a formal system is "entirely formal". The definition does NOT say that; the definition says what a formal system is, but does not contain the words "entirely formal", does not assert that it cannot have semantic content attached to it. That's your interpretation of the definition. Just asserting over and over that you are right and therefore anyone who agrees with you is ignorant or confused is not an argument, and is in fact inappropriate behavior. If you really need to find someone who seems unable to behave according to the norms, I suggest you purchase a mirror and learn how to use it. Finally, I did not "accuse" you of "being mean". I accused you of being purposely and unnecessarily rude, not assuming good faith, and apparently being unable to be civil. And your response just proved all of my points, so thank you. Magidin (talk) 05:17, 6 April 2016 (UTC)

I'm bored by your unsubstantive tangents...but feel free to get the last word..i won't respond anymore...68.48.241.158 (talk) 10:39, 6 April 2016 (UTC)

Oppose - "consist" and "entirely" are overly tricky words in this context. If a formal system has an intended semantics, as the relevant systems of arithmetic do, it is not an abuse of language to talk of sentences of the formal system as being meaningful. On the one hand, it is clear what we mean when we say that the interpretation is in addition to the structure that defines the formal system, on the other hand it is also clear what we mean if we say that (formal) semantics is part of (formal) language. I agree with Robert McClenon that the language of the RfC seems to be calculated to filibuster Trovatore and so I cannot support it. — Charles Stewart (talk) 09:39, 6 April 2016 (UTC)

it's about explaining the distinction..he won't allow an explanation of the distinction...as he doesn't think there is one...I apparently didn't explain the RfC well enough..though tried to make it as straightforward as possible....68.48.241.158 (talk) 10:39, 6 April 2016 (UTC)

I don't think that's the case. An advanced degree does not mean someone is always right, but it does reduce the general chance of completely misunderstanding basic concepts. Quite a few of the people who commented in this thread, based on my knowledge and belief, have PhDs in logic. The chance that so many well-educated commenters would all misunderstand the question in the same way seems to me to be very low. There is certainly a distinction between syntax and semantics. Perhaps the distinction might be misrepresented in some references (e.g. Braithewaite, which we know to be a problematics source), to an extent that would not be reasonable for this article. — Carl (CBM · talk) 10:58, 6 April 2016 (UTC)

When adding explanatory text to an article, we always have to ask "what is the purpose"? In the case of the incompleteness theorems, I see no reason to overly emphasize that formal systems can be considered without interpretations, because the formal systems to which the theorems apply always have at least one interpretation, which is about the natural numbers. The word "entirely" is confusing in that situation, because the interpretation in terms of numbers is a central part of the incompleteness theorems (and important to the truth of the Goedel sentence). Most formal systems of foundational interest (PRA, PA, ZFC, etc.) include both a formal syntax and an intended interpretation, and in that sense they don't consist entirely of formal content. It would go against the general goal of "neutral point of view" to write this article from a more extreme formalist perspective, because that is not the way that the majority of sources treat the theorems - particularly more modern scholarly sources. — Carl (CBM · talk) 10:52, 6 April 2016 (UTC)

my explanatory text was exactly for the sake of explaining what you state here; though just a little more carefully for the sake of accuracy...you state, "include both a formal syntax and an intended interpretation.." ...they only include a formal syntax...the intended interpretation is a separate, outside thing (and this is what I explain)...I think you'd agree this is uncontroversial....(I have no interest in supposed credentials either, basically irrelevant in the world of Wikipedia, referencing them shouldn't even be allowed...as someone can advertise them for the sake preserving their erroneous understanding of something...68.48.241.158 (talk) 11:23, 6 April 2016 (UTC)

this is the paragraph I put together that was objected to on erroneous grounds if anyone is interested at this point:

"In general, a formal system is a deductive apparatus that consists of initial strings of symbols (the “axioms”) and rules of symbolic manipulation (or rules of inference) that allow for the creation of new strings. By definition formal systems lack content and are entirely formal exercises. However, a formal system may be intentionally designed so that it will simultaneously mirror and allow for interpretation about some other phenomena. One example of such a system is first-order Peano arithmetic, a system in which all variables are intended to denote natural numbers. In other systems, such as set theory, only some sentences of the formal system express statements about the natural numbers. The system relevant to Gödel's theorems was designed to mirror whole number arithmetic so as to explore the possibility of Hilbert's program." 68.48.241.158 (talk) 11:52, 6 April 2016 (UTC)

The issue, of course, is the claim "By definition formal systems lack content and are entirely formal exercises. ". The systems of interest to the incompleteness theorem do not lack content - they must be able to prove various facts about arithmetic, which means that they must be able to express these facts, which means that some method of interpreting statements of arithmetic into the theory must be available. Moreover, it is not clear to me what an "entirely formal exercise" would be - systems of foundational interest possess that interest because they have intended interpretations, and calling them "entirely formal exercises" is a particular POV that I don't find to be mainstream in the literature. So I don't think such a claim would be desirable in the article. Moreover, I disagree with including that claim about Hilbert's program, which also seems to promote a particular POV. When I see PA defined in textbooks, they do not say that it is designed to explore Hilbert's program, and ZFC certainly was not designed for that purpose. — Carl (CBM · talk) 14:18, 6 April 2016 (UTC)

well perhaps it could be "By construction (or by intention) formal systems lack semantic content and are entirely formal exercises." But this is all just definitional...there's no philosophic agenda here...the idea is to explain the distinction....and, of course, this is all about the Hilbert Program zeitgeist, PA came out of this zeitgeist, Gödel's work came out of this zeitgeist...in fact, I really do think this zeitgeist needs to be discussed and explained in the history section or somewhere....68.48.241.158 (talk) 14:43, 6 April 2016 (UTC)

if you google HP and PA the Stanford encyclopedia comes up for HP which has a big section on PA, for example68.48.241.158 (talk) 14:49, 6 April 2016 (UTC)...

Exactly which section of [1] do you mean? You should keep in mind, in any case, that the specific formalistic viewpoint that led to Hilbert's program is not very common in contemporary sources. — Carl (CBM · talk) 14:53, 6 April 2016 (UTC)

section 1.2 "the influence of PA"68.48.241.158 (talk) 14:56, 6 April 2016 (UTC)

PA is an abbreviation for Peano Arithmetic, rather that Principia Mathematica. Principia Mathematica, like Hilbert's program, is primarily of historical interest today, and indeed few students learn anything about Principia as part of their PhD education. On the other hand, Peano Arithmetic is a very different theory which is very commonly used for foundational purposes in contemporary literature. — Carl (CBM · talk) 14:59, 6 April 2016 (UTC)

oh, my mistake as far as what you were abbreviating...all of these things are subjects of the Hilbert Program zeitgeist, of course..."PM" is work in this program and the theorems are work about PM, and "related systems"...68.48.241.158 (talk) 15:28, 6 April 2016 (UTC)

To me, the paragraph in bold takes too much of the POV of certain authors in the first half of the 20th century, in terms of promoting a formalist viewpoint, and I find that viewpoint to be less than mainstream today. Our article needs to be balanced between formalism and other viewpoints. Did you take my advice to obtain a copy of Peter Smith's book? He has a long discussion of this on page 19, which he ends with "But it is one thing to ignore their semantics for some purposes; it is another thing entirely to drain formal proofs of all semantic significance. Anyway, we can think of a formal language L as in general being a pair (L, I) where L is a syntactically defined system of expressions and I gives the intended interpretation for these expressions". I recommend that book, as Smith does a good job of presenting things in a neutral way with awareness of the various philosophical positions. (Also, we do discuss Hilbert's program at several points of the article.) — Carl (CBM · talk) 14:18, 6 April 2016 (UTC)

he's explaining exactly what I'm explaining...though in a slightly more difficult way to understand...this could be used as a cite for my paragraph!!68.48.241.158 (talk) 15:32, 6 April 2016 (UTC)

Oppose: The text in Goedel is clear (quoted below) on this point of "truth" versus "formal system", so I oppose. But I'm not surprised that 68 is having difficulties. This is not trivial stuff; it requires readings in philosophy as well as all the writings of Goedel with respect to the incompleteness theorems. Reading a biography of Goedel would help, too.

RE what a "formal system" is (clue -- it's not symbols on paper). Later in life Gödel answered the question of what he thought was the only appropriate definition of a formal system: "In consequence of later advances, in particular of the fact that due to A. M. Turing's work [footnote 69 See Turing 1937] a precise and unquestionably adequate definition of the general notion of formal system [footnote 70] can now be given . . .. [Footnote 70: ". . .[transfinite generalizations of formalisms are] something radically different 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".] (Goedel added this note to his 1930 in 1963, cf van Heijenoort 1967:616). So there you go: a formal system is an appropriately-programmed Turing machine, or a person with paper and pencil observing symbols and acting as if they are a mechanism: active agent + formation rules + symbols, all effective for the specified task at hand.

RE the notion of truth in Gödel's 1930. A number of years ago, on these very pages, Trovatore and CBM corrected my thinking about what "truth" means in this proof. I challenged them to find the word "truth" in Gödel's 1930 (cf van Heijenoort 1967:592ff). I was assured that the word is in the document, and indeed it is, at least three times. Here's the key usage: "From the remark that [R(q); q] says about itself that it is not provable it follows at once that [R(q); q] is true, for [R(q); q] is indeed unprovable (being undecidable). Thus, the proposition that is undecidable in the system PM still was decided by metamathematical considerations. The precise analysis of this curious situation leads to surprising results concerning consistency proofs for formal systems, results that will be discussed in more detail in Section 4 (Theorem XI)." (italics in the original, van Heijenoort 1967:599, last paragraph before "2"). In other words, exterior-to-the-formal-system truth is required as well as the "formal system".

RE: "truth" in the context of the incompleteness theorems. Trovatore was correct when he brought up the philosophy of realism in relation to "truth" and "formal systems". Of particular concern is the notion of "univerals" in Platonism. For a very clear reading of a realist/Platonist's thinking find a cc of Bertrand Russell's The Problems of Philosophy. (Russell is known as a realist (see Perry's introductory notes) but also as neutral monist with Platonist sympathies; Goedel is well-known to be a Platonist). Russell drives both his realism and Platonism from his observations of the world and thinking about objects and minds with "beliefs". More to the point: toward the end of the book, in his chapter TRUTH AND FALSEHOOD (pp. 119ff) he asserts that truth has three observable characteristics: (I) it has an opposite, falsehood, (II) truth and falsehood are properties of beliefs and statements as opposed to "a world of pure matter" [this is a very important discussion], and (III) however, "truth or falsehood of a belief always depends upon something which lies outside the belief system". Eventually he is "driven back to correspondence with fact as constituting the nature of truth" (p. 123). He then proceeds to discuss what 'facts' are in relation to "beliefs" and "truth" and "knowing".

I'm going to leave with this: This stuff is hard. 68 should give it a breather. Find copies of van Heijenoort and Russell and read a biography of Goedel, think a bit more about why metamathematical "truth" is required for his proofs. Bill Wvbailey (talk) 15:41, 6 April 2016 (UTC)

you seem to be discussing something entirely different (or WAY beyond) what's being discussed here....this whole notion of "truth" is an entirely different subject...the discussion of formal systems you mention is correct, fine, and totally in line with what a formal system is...68.48.241.158 (talk) 15:54, 6 April 2016 (UTC)

this has been a problem in general, though...if you go read my question precisely and answer ONLY what is being asked, you'd probably AFFIRM...based on the info you cite relating to formal systems....68.48.241.158 (talk) 16:02, 6 April 2016 (UTC)

And again. Stop it. People are not disagreeing with you because they don't understand you, or because they are ignorant. You continue to assert that the only reasons for people to not agree with you is lack of knowledge or lack of understanding, and that's obnoxious and rude. You are, in essence, insulting people because they don't agree with you. Stop making claims about what other people know, don't know, or would do if only they could understand your lofty goals. Magidin (talk) 16:50, 6 April 2016 (UTC)

you stating that I'm calling people ignorant or stupid (which I'm not, and haven't) is likely to make them think that, perhaps, I'm calling them these things...it is ENTIRELY inappropriate...if it seems he obviously answered a different question, I can point this out and ask for clarification...he can then choose to clarify, or not...68.48.241.158 (talk) 16:59, 6 April 2016 (UTC)

Stop playing games. If I were to take the same attitude, I would say "Your assertion that I'm stating that you call people ignorant and stupid is a lie, because I never said the words 'You are calling people ignorant or stupid'". You are telling everyone who disagrees with you that the reason they disagree with you is that they don't understand, or that they don't know what they are talking about, or that they are saying things that are patently silly; not in so many words, but you are essentially saying that. So stop playing the silly word lawyer. You are being insulting and rude, but prefer to play games and hide behind "I never said the word, so you can't claim that I'm calling people that." In addition, apparently everyone else makes statements of opinion but you are in a unique epistemic position to make statements of fact and only statements of fact. You are not. Nor are you in a position, clearly, to decide what is and what is not appropriate, entirely or not, so you can also cut that out. Shouting does not make it so. Drop the stick. The consensus is pretty clear, and nobody is agreeing with you. If you follow your pattern, you will dismiss all of them as "ENTIRELY inappropriate", "misguided", "irrelevant", etc. Nonetheless, the consensus is against you, and quite clearly so. And if you still think you are not being rude or obnoxious, I have news for you: you are ENTIRELY wrong. Magidin (talk) 17:10, 6 April 2016 (UTC)

• Oppose The RFC does not belong to this article because it is about the definition of the notion "formal system", and must be (a) discussed in "formal system" article (BTW which sucks) and (b) based on analysis of sources, not on personal opinions. At the same time, I suspect that the proposer tries to implement here a well-known philosophical apposition of "form" vs. "content". In this case the proposer is rather confused, because in this respect the phrase "formal content" is nonsense. Staszek Lem (talk) 16:39, 6 April 2016 (UTC)

the proof is a proof about formal systems...so they naturally are and should be discussed to some degree in this article...it would be very odd and probably unworkable to not do so (so not too helpful to just make this blanket statement)....but perhaps would better to say "composed entirely of formal rules and symbols..."68.48.241.158 (talk) 16:50, 6 April 2016 (UTC)

• Tally: Currently we are at 10 Oppose and 2 Support (including OP) just fyi... Fritzmann2002 17:05, 6 April 2016 (UTC)

  Who is the second person? — Carl (CBM · talk) 17:14, 6 April 2016 (UTC)

I will point out that the tally of !votes includes both those who disagree with the formal statement about formal systems and those who think that the whole RFC is badly stated and will get nowhere. Since the Original Poster agrees "I didn't pose it as well as I could", I would suggest that the OP withdraw the RFC as written, and engage in discussion here about how to reword the RFC. The discussion should define the actual question about how the formal definition of formal systems related to Godel's theorem. AS it is, the RFC as worded is almost certainly either to be closed as No, or to be closed as No Consensus because the comments are not all focused on one question, or to be boxed by the closer with the statement that a formal close (that's getting very formal) is not feasible. (Different closers have different approaches to badly stated RFCs.) So my advice is for the OP first to withdraw the RFC by pulling the bot tag, and then engage in dialogue about how to word the RFC. The alternative will be to let it run for 29 more days, and then address the recommendation of the closer to run another RFC. Robert McClenon (talk) 18:35, 6 April 2016 (UTC)

yeah, perhaps...I tried to ask for clarification from a few who seemed to "AFFIRM" if you looked at just their relevant statements...the RfC was only looking to get agreement on the definition of a formal system, which should be trivial...but I didn't pose it as well as I could..and a couple people followed me over from the help desk who didn't like that I asked them not to move my help desk questions..they then started the answers in a real bad faith way (personal attacks, no substance toward RfC), and this then colored others input to a degree...68.48.241.158 (talk) 17:19, 6 April 2016 (UTC)

User:Tsirel was the second. Fritzmann2002 17:22, 6 April 2016 (UTC)

I'm not sure if even him lol..I asked for clarification from him and even after the clarification I couldn't understand whether he was "affirming" or not..he might not be a native English speaker, not sure..68.48.241.158 (talk) 17:28, 6 April 2016 (UTC)

Right, the boldface under Tsirel was again by the IP, not Tsirel. I think Tsirel's position was that Gödel's theorem is not about purely formal systems (as the IP is trying to argue), but rather about interpreted formal systems, so that the proposed text (about the definition of purely formal systems) is true but irrelevant. —David Eppstein (talk) 17:51, 6 April 2016 (UTC)

not trying to argue that..trying to get agreement on what a formal system is...and the distinction between a formal system and its mechanisms and interpreting said formal system....68.48.241.158 (talk) 18:12, 6 April 2016 (UTC)

Exactly so. Sorry for being unclear. I never participated in RfC before; and I was not quite understanding, what is asked. Boris Tsirelson (talk) 18:00, 6 April 2016 (UTC)

So, this thread is probably a "Fail" as they say...it's not really clarifying anything as the question posed was a bit too vague (oddly I think it ended up being too vague because it was too specific...ie didn't provide any context...tried to save it a bit by seeking some clarification from people but this is difficult)....I was trying to nail down a definition of "formal system" (which I do believe is in fact trivial) that could be worked from...but it was launched in a very negative direction by the first person to respond..which caused a lot of mess....there were a few good tidbits that perhaps could be helpful in future editing of the article though....68.48.241.158 (talk) 18:12, 6 April 2016 (UTC)

The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

vanity content? "formalized proofs"

a professor recently added a brief nod to himself in the article that lacks context or explanation...the entire section lacks context or explanation...and I don't think is even properly stated....(ie they are talking about digital/computerized proofs or something...Gödel's proof itself is formalized)...so seems inappropriate..then someone else tried to erase the supposed citation (at least the professor bothered to put in a cite)...but whole thing seems problematic...but the person should at least bother to explain the content in this section to some degree to see if it rises to relevance...instead of just coming along and putting his name in a prestigious article topic.....68.48.241.158 (talk) 13:27, 9 April 2016 (UTC)

See User_talk:Lcpaulson. Changes are still pending revisions. Baking Soda (talk) 13:30, 9 April 2016 (UTC)

Goedel's original proofs were written in natural language. The incompleteness theorems are among a very few nontrivial theorems for which fully formalized and machine verified proofs have been produced. The inclusion of references to that is not vanity content. We don't want to overemphasize that section, but it is an important secondary point to make in a comprehensive article about the incompleteness theorems. — Carl (CBM · talk) 13:44, 9 April 2016 (UTC)

granted, you just explained in less than a minute's time better than it's explained in the article...(ie we're talking about a computer/digital demonstration of the proof here or something...I can't say I know exactly what's being talked about)..so that should be added...and the section should be renamed for clarity (ie "Machine or (Computer) Verified Proofs".....and the professor's own inclusion of himself in the article I think is completely against policy (not that I care that much about this...if he'd had bothered to improve/explain the section....instead of just plant his name in the article)....68.48.241.158 (talk) 13:59, 9 April 2016 (UTC)

granted, too: I know exactly what you mean when you say "were written in natural language"...but this notion can create the confusion that the section title can create, ie that Gödel's proof is informal and these computer proofs are formal...whereas that's not the distinction...the distinction is something else, clearly...but exactly what this distinction is needs to be mentoned in at least a couple sentences in the section.....68.48.241.158 (talk) 14:23, 9 April 2016 (UTC)

Gödel's incompleteness results and strong types

The use of strong types in Computer Science has brought into question Gödel's meta-mathematical results as to which proposition of the Dedekind/Peano theory of numbers is true but unprovable. Gödel proposed the sentence "I an not provable." as the true but unprovable sentence. However, Wittgenstein correctly pointed out that Gödel's sentence leads to inconsistency in mathematics. The resolution is that using strong types, it can be shown that Gödel's sentence is not a sentence of mathematics. Consequently Gödel's argument (using his sentence) is incorrect that mathematics cannot prove its own consistency without itself falling into inconsistency. In fact, mathematics formally proves its own consistency (using a very simple proof by contradiction) without evident self-contradiction in mathematics (e.g., all the usual paradoxes such as Russell, Berry, Girad, etc. do not produce inconsistencies).

Carl (talk) 16:00, 20 April 2016 (UTC)

Note: References to published literature that were previously here have been deleted by another editor.Carl (talk) 13:20, 21 April 2016 (UTC)

Discussion

• This is already adequately addressed in the section "Limitations of Gödel's theorems". Do you have any specific issues with that section? (And type theories either fall into the category "cannot prove their own consistency", e.g. the Calculus of Constructions, or are inconsistent to begin with, e.g. System U. I'm thus not seeing how "strong types bring Gödel's results into question".) —Ruud 17:05, 20 April 2016 (UTC)

This discussion is probably not going to get far if references to the published literature are barred and deleted from the discussion. So what exactly are the rules as to references to published literature that can be posted here? Carl (talk) 13:13, 21 April 2016 (UTC)

Carl (CBM) summarizes this excellently in the section below. This talk page is intended to make suggestions for improvements to the article. The article should give a balanced overview of the literature on this topic. As such:

1. It is not appropriate to refer to obscure sources that present a minority point of view. Such sources, nor the arguments they make, will be included in the article, per the "undue weight" rule.
2. It is not appropriate to use discussions on this talk page as a coat rack for publicizing talks or papers.

If you believe there is an accepted view that "types bring Gödel's results into question", then you should be able to point to more widely cited sources than your own paper supporting such a claim.

—Ruud 15:26, 21 April 2016 (UTC)

Relevance of the results on Gödel's incompleteness theorems in articles of Vol. 52 Studies in Logic and its reviews

The following discussion is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

---

Deficiencies of section on "Limitations of Gödel's theorems"

An editor above has called for a discussion of the deficiencies of the section "Limitations of Gödel's theorems". A major deficiency is that it lacks discussion of the controversy over whether or not Gödel's sentence "I am not provable." is a valid sentence of mathematics. Godel's sentence in not valid in systems that use strong parameterized types because the construction in section "Diagonalization" cannot be carried out according to the book "Inconsistency Robustness". Carl (talk) 13:38, 21 April 2016 (UTC)

Let me first point out that this talk page is not a forum to debate the merits of any claims. I encourage all editors, to the greatest extent possible, to avoid arguing over the correctness of claims, and to look instead at Wikipedia's content policies.

The key policy regarding this content is the section Due and undue weight of WP:NPOV. It can be summarized with the following three bullets which I will quote directly:

• If a viewpoint is in the majority, then it should be easy to substantiate it with reference to commonly accepted reference texts;
• If a viewpoint is held by a significant minority, then it should be easy to name prominent adherents;
• If a viewpoint is held by an extremely small (or vastly limited) minority, it does not belong on Wikipedia, regardless of whether it is true or you can prove it, except perhaps in some ancillary article.

In my opinion, the claim that the Goedel sentence of a theory is "a sentence of mathematics" is the position of essentially all authors in the reference literature. To quote from the SEP: "The sentence in question is a relatively simple statement of number theory, a purely universal arithmetical sentence." [2]. It is very easy to substantiate the claim "The Goedel sentence of a formal theory is a mathematical statement" with numerous other references to standard references on the incompleteness theorems.

On the other hand, the viewpoint that the Goedel sentence of a formal theory is *not* a mathematical statement seems to be a position with a vastly limited amount of support in the literature, namely a few publications by Dr. Hewitt. As such, I do not see any true "controversy" in the literature, nor do I think that there is enough of a discussion in the literature to discuss in this article the position that the Goedel sentence of a formal theory is not a mathematical statement. As the policy states, "Generally, the views of tiny minorities should not be included at all, except perhaps in a "see also" to an article about those specific views." For better or worse, the position espoused by Dr. Hewitt appears to be that of a tiny minority, based on my knowledge of the literature on the incompleteness theorems. Indeed, apart from Dr. Hewitt, I can name no prominent adherents to this viewpoint. — Carl (CBM · talk) 14:34, 21 April 2016 (UTC)

I completely agree that this talk page is not forum to debate the merits of any claim. However, reporting on controversies in the literature is reasonable.

It is perfectly fair to point out that the views of Professors Hewitt, Meyer, and Woods are currently in the minority among philosophers. See the following:

• "Inconsistency: Its present impacts and future prospects." Professor John Woods in "Inconsistency Robustness" Carl Hewitt and John Woods assisted by Jane Spur editors. College Publications. ISBN-10: ISBN 1848901593. 2015.
• "Review of 'Inconsistency Robustness'" Professor JJ Meyer. Vol. 52 of Studies in Logic. College Publications website. 2016.
• "Two sources of explosion" Dr. Eric Kao in "Inconsistency Robustness" Carl Hewitt and John Woods assisted by Jane Spur editors. College Publications. ISBN-10: ISBN 1848901593. 2015.

The book "Inconsistency Robustness" claimed that the sentence "I am not provable" is very dubious as a sentence of mathematics because it is not a sentence about mathematical objects such as numbers, triangles, groups, etc. In fact, Gregory Chaitin 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."

The claim is that there is a much more important proposition (which derives from the work of Church) for the Dedekind/Peano theory of numbers that is true but unprovable.

In order to promote greater robustness in operations and security, computer scientists have embraced strong parameterized types, which rules out validity of the Gödel sentence "I an not provable." The book "Inconsistency Robustness" points out that allowing such a sentence could cause security holes in computer systems. The view that strong parameterized types are crucially important is strongly held and growing in Computer Science although it is not universally accepted.

Carl (talk) 17:58, 21 April 2016 (UTC)

Deficiencies of section on "Implications for consistency proofs"

1. An editor above has called for a discussion of the deficiencies of the section "Implications for consistency proofs". A major deficiency is that it lacks discussion of the controversy over whether or not the proof is valid that mathematics proves its consistency (published in the book "Inconsistency Robustness"). Carl (talk) 13:58, 21 April 2016 (UTC)
2. An editor above has raised the issue of consistency for strong parameterized type systems (such as the one published in the book "Inconsistency Robustness") that con proved their own consistency. Strong parameterized type systems defeat Girard's paradox because the type Type is parameterized. For example if τ is a type, then Type◅τ▻:Type◅Type◅τ▻▻. Carl (talk) 14:24, 21 April 2016 (UTC)

As I mentioned in the previous section, it is best to avoid debate here on the merits of the material being discussed. Looking at WP:DUE again, I do not see that there is sufficient weight in the published literature to support discussion in this article about inconsistency robustness or about the claim "mathematics proves its own consistency". Indeed, I cannot name *any* prominent adherents of the latter viewpoint, apart from Dr. Hewitt, despite being very familiar with the literature on the incompleteness theorems. The viewpoint that "mathematics proves its own consistency" is simply not mentioned at all in the standard reference literature (much of which is mentioned in the references section of this article). The general practice described by Wikipedia policies such as WP:NOR and WP:V is to wait until a viewpoint has at least a significant minority position and enough independently published secondary sources to write a neutral article on the issue. This means that, from time to time, new viewpoints should not be reported at all, until they have gained sufficient attention in the literature. — Carl (CBM · talk) 14:44, 21 April 2016 (UTC)

Previously, logicians and philosophers have been those most interested in the material in this article. Computer scientists have different concerns (for example security) and methodology (for example basing mathematical foundations on strong parameterized types). It is not too surprising that the Computer Scientists have come to some different conclusions than previous logicians and philosophers. The Computer Scientists have held two important international symposia at Stanford that have resulted in the publication of an important volume in what is arguably the most prestigious series of books in the area, namely, "Studies in Logic." The reviewers, editors, and authors of articles of the "Inconsistency Robustness" volume should not be dismissed as lightweights.

That said, it is not the job of Wikipedia to decide whether or not the above Computer Scientists are correct. Carl (talk) 18:31, 21 April 2016 (UTC)

Your claim to speak for "the computer scientists" is extremely dubious, and that's putting it politely. Prove that computer scientists in general agree with you, or stop doing it. --Trovatore (talk) 19:23, 21 April 2016 (UTC)

Good point. I added the clarifying word "above" to my comment. Carl (talk) 19:43, 21 April 2016 (UTC)

@Prof. Carl Hewitt:, can you please provide secondary sources (publications/books) that asses and/or cite the work in "Inconsistency Robustness". "Secondary or tertiary sources are needed to establish the topic's notability and to avoid novel interpretations of primary sources." Baking Soda (talk) 18:38, 21 April 2016 (UTC)

Probably the most famous is "Review of 'Inconsistency Robustness'" by the noted Computer Scientist Professor JJ Meyer, which has appeared various places including the catalogue listing for Vol. 52 of Studies in Logic on the College Publications website. Carl (talk) 18:55, 21 April 2016 (UTC)

A book review on a book about "inconsistency robustness" does not warrant mentioning inconsistency robustness in the article about Gödel's incompleteness theorems. What we are looking for would be surveys on Gödel's results discussing the relevance of inconsistency robustness to the incompleteness theorems. Such sources do not appear to exist. Hence, this article should not mention inconsistency robustness. —Ruud 20:17, 21 April 2016 (UTC)

In his review, Professor Meyer states:

"As Hewitt says in his preface: “The field of Inconsistency Robustness aims to provide practical, rigorous foundations for computer information systems having pervasively inconsistent information in a variety of fields e.g., computer science and engineering, health, management, law, etc.”

The approach defies Gödel’s famous 2nd incompleteness theorem (traditionally deemed to be one of the greatest achievements in logic in the last century), which states that mathematics, if consistent, cannot prove its own consistency. In the Classical Direct Logic, mathematics is provably formally consistent! By formally consistent, it is meant that an inconsistency is not inferred. The proof is remarkably tiny consisting of only using proof by contradiction and soundness. In fact, it is so easy that one wonders why this was overlooked by so many great logicians in the past. The proof is also remarkable that it does not use knowledge about the content of mathematical theories (plane geometry, integers, etc.). The proof serves to formalize that consistency is built into the very architecture of classical mathematics. However, the proof of formal consistency does not prove constructive consistency, which is defined to be that the rules of Classical Direct Logic themselves do not derive a contradiction. Proof of constructive consistency requires a separate inductive proof using the axioms and rules of inference of Classical Direct Logic. The upshot is that, contra Gödel, there seems to be no inherent reason that mathematics cannot prove constructive consistency of Classical Direct Logic (which formalizes classical mathematical theories). However, such a proof is far beyond the current state of the art."

Carl (talk) 20:32, 21 April 2016 (UTC)

Again: A book review on a book about the issue does not constitute a reliable or notable secondary or tertiary source. As such, what it actually says or does not say is irrelevant. We are still talking about the views of a tiny minority, with nothing but primary sources to substantiate them. Including them would be undue weight, and the lack of notable, reliable secondary or tertiary sources is a major problem. The precise wording of the review is irrelevant. Magidin (talk) 20:36, 21 April 2016 (UTC)

By the official criteria of Wikipedia, Professor Meyer's review is a reliable and notable secondary source and consequently what it says is important. Professor Meyer's work and stature compare favorably with just about any prominent active logician.

Admittedly, it will probably take a while for the above Computer Science view to become a majority view among very senior philosophers who work in this area. However, the above Computer Scientists are having considerable impact in their field because of the increasing prominence and use of strong parameterized types. The invalidity of Gödel’s sentence "I'm unprovable." is necessary to maintain system security.Carl (talk) 21:13, 21 April 2016 (UTC)

My understanding of the official criteria is that a book review does not constitute a notable secondary source, any more than a review of an article on MathScieNet would constitute a reliable secondary source for the original article, regardless of who is the author of the review. It would have to be some sort of survey that places the work being discussed in context or reviews the actual contents, rather than a simple reivew. Final paragraph is irrelevant, and continues to harp on irrelevant considerations; nobody is asking that the view become "a majority view", but rather that it be a view held by a significant minority and have a verifiable impact. The final sentence of the second paragraph continues the author's attempt at arguing about the importance of his own work and its validity, neither of which is relevant and constitutes little more than continued spam on this talk page. If you have nothing to add beyond repeating how important this is according to you and your collaborators for Computer Science, then your point has been made and rejected as irrelevant for this article; you can stop repeating it and wasting your time and everyone else's. Magidin (talk) 21:22, 21 April 2016 (UTC)

Professor Meyer's review is clearly a secondary source because according to official Wikipedia policy:

A secondary source provides an author's own thinking based on primary sources (for example the volume "Inconsistency Robustness", Gödel's article, as well as articles on intuitionistic and paraconsistent logic), generally at least one step removed from an event. It contains an author's analysis, evaluation, interpretation, or synthesis of the facts, evidence, concepts, and ideas taken from primary sources. Secondary sources rely on primary sources for their material, making analytic or evaluative claims about them.

Professor Meyer's review places the works being discussed in context and reviews their actual contents.

Carl (talk) 22:04, 21 April 2016 (UTC)

Reliability and notability are two different things; sources may or may not be reliable, subjects notable. In this case the question is whether Meyer's review is reliable, and if so whether it confers enough notability on Hewitt's theories to make them worth including in the article. Meyer certainly provides non-trivial secondary coverage of Hewitt's theories. But as far as I can see it does not pass WP:RS because it has not been published in a venue with any editorial oversight of such publications (such as a peer-reviewed journal); instead I can only find it at the web site of the book's publisher, giving it the appearance of a commercial blurb rather than a piece of scholarly writing. As such it appears neither reliable nor to confer any notability. —David Eppstein (talk) 21:58, 21 April 2016 (UTC)

These are good questions! According to Wikipedia policy, the following should be examined:

• The type of the work (some examples include a document, an article, or a book) In this case, it was a critical academic review that is a piece of scholarly writing.
• The creator of the work (for example, the writer). In this case, it was Professor JJ Meyer, who is a prominent academic in this area of research.
• The publisher of the work (for example, Oxford University Press). In this case, it was College University Press, which is arguably the most reputable publisher for this area of research.

Professor Meyer's article was reviewed by the prestigious and extremely competent series editors that provide academic editorial oversight over "Studies in Logic".

Consequently, by the official criteria of Wikipedia, it seems clear that Professor Meyer's review is reliable and notable.

Nevertheless, it will be challenging to incorporate this material into the article. In this regard, it would great if we could attract some new editors.

Carl (talk) 23:46, 21 April 2016 (UTC)

To my mind, I simply don't see enough evidence that there is enough worry in the literature about "mathematics proves its own consistency" to warrant even mentioning it in this article. If this was a topic with which a significant minority of the logical community was engaged, we would not need to worry about whether to use a book review as a source, because there would be several peer-reviewed papers published by clearly independent authors. Perhaps that will happen one day, at which point we should re-evaluate the issue. Quoting from the sources at length is not necessary, in any case, because we are not here to discuss the content of those sources nor evaluate their correctnsss. In the interest of avoiding unduly long conversations, I will generally try to limit my responses to one per day. — Carl (CBM · talk) 10:40, 22 April 2016 (UTC)

The above Computer Scientists did not initially set out to overthrow Gödel's approach to incompleteness. However over time, Gödel's sentence "I'm unprovable." became an obstacle to the Computer Scientist's security requirements. Fortunately, strong parameterized types enabled them to show that Gödel's sentence is neither valid nor needed in mathematics. However, once Gödel's sentence was thrown out, whether or not mathematics can prove its consistency once again became an open question. At this point, the Computer Scientists discovered a remarkably simple proof that mathematics does formally prove its consistency. So Computer Science is in relatively good shape and is coming to a consensus around using strong parameterized types for the mathematical foundations of Computer Science and also using them in the foundations of their programming languages.

So where does this leave traditional senior philosophers and logicians who previously thought that they owned this subject matter because of their previous publications? There are at least two possibilities:

• The field splits and senior traditionalists try to ignore the Computer Scientists' prestigious published volume and its reviews.
• Some younger philosophers and logicians join with the Computer Scientists pushing forward with strong parameterized types in foundations. At this point, the above Computer Scientists are firmly ensconced in their field and have a head start in that they have held two international symposia at Stanford and published a well-regarded volume of articles on their results in what is arguably the most prestigious academic series of volumes in the area. But there is still much work to be done!

Carl (talk) 14:11, 22 April 2016 (UTC)

The reasons why the editor, commenting glowingly on himself in the third person, entered into this area are irrelevant to the article. The application of his ideas to Computer Science, and their importance, are irrelevant to the article. The editor's musing about the future of his field are irrelevant to this article. In short, all of the recent comment is irrelevant and spammy, and seems designed mainly so the editor can praise himself in the third person. That editor might perhaps consider stopping it. Magidin (talk) 14:26, 22 April 2016 (UTC)

The volume "Inconsistency Robustness" (a collection of articles) and its reviews were very much a community effort. Progress would have been impossible without the collaboration of many participants at two Stanford international symposia. Personally, I spend time and enjoy promoting my colleagues. Carl (talk) 15:32, 22 April 2016 (UTC)

It's nice that you have hobbies. However, the talk page of the article is not the place for you to indulge in them. It is not a place for promotion, either of yourself or of your colleagues. Magidin (talk) 16:08, 22 April 2016 (UTC)

The participants at the two Stanford symposia and the authors of the articles in "Inconsistency Robustness" were dedicated professionals and computer science graduate students, who should not be dismissed as "hobbyists." They are not particularly interested to promoting themselves or others. It is true that the most senior among them are charged with with writing letters of recommendation for academic jobs and promotions. However, the major interest of those professionals is almost entirely dedicated to advancing science. Consequently, they have issues with Wikipedia articles that are unbalanced, biased, and inaccurate. Carl (talk) 19:06, 22 April 2016 (UTC)

The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

Continued

I suggested the improved title "Relevance of the results on Gödel's incompleteness theorems in articles of Vol. 52 Studies in Logic and its reviews" for the section below so that editors could better understand the subject matter under discussion. The current title "Inconsistency Robustness" is inappropriate because the discussion has almost nothing to do with "inconsistency robustness" and has everything to do with the relevance of the results on Gödel's incompleteness theorems in articles of Vol. 52 Studies in Logic and its reviews. I apologize for not making this suggestion earlier, but I had no idea that the discussion could be closed without notice.

Also, many Computer Scientists are unhappy with the current biased, unbalanced, and inaccurate state of the article. But they are reluctant to contribute for fear that they will be personally attacked. Carl (talk) 02:52, 23 April 2016 (UTC)

For what it's worth, I support allowing Prof. Hewitt to change the section heading. Come on, everyone, let's not argue the toss. --Trovatore (talk) 03:06, 23 April 2016 (UTC)

Done. —Ruud 10:48, 23 April 2016 (UTC)

Thanks to Ruud for restoring the more accurate title!!

Wikipedia policy states that "primary sources that have been reputably published may be used in Wikipedia; but only with care, because it is easy to misuse them. Any interpretation of primary source material requires a reliable secondary source for that interpretation." In this case we have a reliable primary source, namely, "Vol. 52 of Studies in Logic" with a reliable secondary source, namely, the review by Professor JJ Meyer that backs up the primary source. So what does it take for the Computer Scientists to have standing in Wikipedia? Would it be sufficient for another very prominent and prestigious Computer Scientist to publish a review? Carl (talk) 13:51, 23 April 2016 (UTC)

I'll answer per my own humble needs. What is missing is a couple "interpretive" sources, "written down" for guys like me who are not computer scientists working "at the edges" but who have read, for example Nagel and Newman's interpretive account of Goedel's theorem, written for a more general, but probably academic, audience. Other excellent, more-scholarly examples -- notice that they are not reviews -- are (i) the various commentaries by van Heijenoort and others before his collected papers (his (biased) attempt to "prune" the literature to those papers "most significant" in the early 20th C), and (ii) the extended commentaries before the various writings of Goedel in the 5 volume set of his nachlass. I will opine that a review is of limited value unless it is an extended interpretation -- e.g. it gives definitions for unfamiliar words, attempts to make the material understandable by wider audience (e.g. philosophers of mind, mathematicians curious but outside "the field", engineers), and most importantly it includes commentary about and quotations from detractors (you see this in van Heijenoort, where detractors are quoted) plus sources (footnotes, references) pointing to those detractors. Hope this helps. BillWvbailey (talk) 14:35, 23 April 2016 (UTC)

Thanks for your helpful comments. Of course, you are correct about the need for interpretation of technical results for those who are not "working at the edges." This was a major motivation for the Computer Scientists to create Vol. 52 of Studies in Logic. Unfortunately, senior philosophers have chosen not to engage intellectually and instead some have attempted to suppress mention of the Computer Scientists' approach using strong parameterized types even though it is at the foundation of programming languages like Java and C++. Since security has become of paramount concern, the Computer Scientists are grimly determined to succeed in putting their mathematical foundations on a sound basis. The Computer Scientists would be happy to engage with detractors to their approach if and when they appear in public. Carl (talk) 15:16, 23 April 2016 (UTC)

In my professional work, I have never found a need to cite a book review in any of my research papers, and I generally don't view book reviews as being at the same level, scientifically, as research articles. So I don't think that more book reviews of the same book would convince me there is active interest about "mathematics proves its own consistency" among a significant number of logicians. This is partially because, if a reviewer really wants to engage scientifically with the content of a book, the reviewer is much more likely to write a paper than to write a review.

It is hard to talk about sources that don't exist - I am sure there are many things that could convince me to include material in this article, and it is impossible to catalog all of them. One of the strongest signs of broader interest in the field about the topic of "mathematics proves its own consistency", as mentioned in your work, would be researchers who are clearly independent (i.e. not close colleagues nor PhD students of each other) publishing peer-reviewed papers in independent forums (in particular, such as well-established journals in mathematical logic or philosophy, where the editorial board has no direct ties to the researcher). Those papers would then provide enough information for us to write clearly about the topic on Wikipedia. Wikipedia aims to lag behind the state of the art to some extent - by the time something is ready to put here, there will be numerous independent sources for us to use. It is acceptable, for Wikipedia, if it takes several years before a topic is ready to include here.

As a point of comparison, Dan Willard has published more than 10 papers on "self-verifying axiom systems" [3], since at least 2001, in multiple clearly independent research journals - his own publications on that subject are more than the total amount of work on "inconsistency robustness". Willard's papers have been published in several independently-edited and well-respected journals. Yet Willard's work receives (appropriately) a single sentence in this article, because although he has put a enormous amount of effort into it, the broader field has yet to show signs that other researchers are interested. The systems in which he is interested are not the same as the systems that are of general interest for the incompleteness theorems (this is also true of Direct Logic). This is not a criticism of Willard's in any way, just an evaluation of its current prominence in the field. So, if "mathematics proves its own consistency" were to have the same level of publication and dissemination as Willard's work, it would surely also merit a single sentence in this article, probably under the section on paraconsistency. But I do not think that it is there yet. — Carl (CBM · talk) 14:49, 23 April 2016 (UTC)

I agree with editor CBM that Williard's "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles" is of only marginal interest to this Wikipedia article. Willard's results are for a very weak mathematical system that does not even include multiplication of integers! Carl (talk) 15:48, 23 April 2016 (UTC)

Focus of the talk page

The focus of this talk page is to discuss improvements to the article. It is not the place to post musings about mathematical topics, to write essays about the incompleteness theorems, or to discuss the mathematics and philosophy behind the incompleteness theorems more generally. Accordingly, discussion here should be focused on specific changes to the article. I have moved two sections to the Arguments page which stated some claims without any description of how the article might actually be edited. Such threads distract the conversation and inhibit rather than encourage article improvement. I encourage others to review that move, and to move other sections in the future if appropriate.

I suggest that anyone who wants to see the article changed should make specific suggestions about how to improve it. Ideally, post the actual text and references that you think the article could include. Suggestions are likely to be more compelling if they are detailed and based on multiple secondary sources in a way that minimizes any potential appearance of conflict of interest. Opening numerous discussion sections simultaneously, or pointing at the same sources repeatedly instead of finding new ones, is less likely to lead to progress. General comments that merely say some section of the article should be edited, with no specific suggestions, are hard to act upon.

I encourage everyone to keep the discussion focused, and to consider first and foremost the specific text of the article, which what this talk page exists to support. — Carl (CBM · talk) 17:11, 23 April 2016 (UTC)

Suggestion for addition to Gödel's_incompleteness_theorems#Criticisms

The following is suggested as an addition to Gödel's_incompleteness_theorems#Criticisms:

Gregory Chaitin criticized Gödel's approach to incompleteness theorems as follows[“Dangerous Knowledge” BBC4 documentary. 2007.]:

"[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) 21:00, 23 April 2016 (UTC)

This may be a helpful quote (I'm not yet convinced either way) but it must not be taken out of context like this. By itself, this quote could easily be misread as an argument against the theorem. What Chaitin was actually arguing against was the non-constructiveness of Gödel's argument. This point is expanded in the recent survey "A Brief on Short Descriptions" (Jason Teutsch and Marius Zimand, SIGACT News 47(1): 42–67, 2016) which states and proves a more concrete form of incompleteness according to which any recursively enumerable and true set of theorems can include the statement that a string is Kolmogorov-random for only finitely many strings. That is, Chaitin's incompleteness theorem gives a concrete class of mathematical statements (this string is random) many of which are true but unprovable, rather than asserting the mere existence of a true but unprovable statement. Of course, Gödel's proof could also be unwound to give a specific and concrete class of true but unprovable statements about integers, but not one of independent interest. —David Eppstein (talk) 21:27, 23 April 2016 (UTC)

Chaitin (above) said that incompleteness is fundamental but that Gödel’s argument (based on the sentence “I'm unprovable.”) was superficial, not serious, and provided no insight into the importance of incompleteness.Carl (talk) 21:39, 23 April 2016 (UTC)

Strikes me as a bit of typical Chaitin self-promotion. Chaitin has some very nice results, but he has a tendency to exaggerate how fundamental they are. This fits right in with that — Goedel proved incompleteness, sure, but with a "superficial" example, unlike Chaitin's, which of course must be much "deeper". But superficial or deep, it only takes one example to refute completeness.

By the way, the Goedel sentence is not "I'm unprovable". It is constructed in such a way that it is Platonically true if and only if it is unprovable in T, for whatever formal theory T is under consideration. But that isn't what it says. What it actually says is "there does not exist a natural number n such that P(n) holds", where P is some explicitly describable primitive recursive predicate. Claims that this is not a mathematical statement really cannot be taken seriously. --Trovatore (talk) 22:16, 23 April 2016 (UTC)

The above comments are both unfair and damaging to the reputation of Chaitin (who is still alive). Chaitin is recognized as one one of the world's foremost experts on Gödel's incompleteness theorems. Chaitin's considered judgment that Gödel's sentence is superficial and does not provide insight into incompleteness must be taken seriously. Gödel himself said that the Church/Turing proof of incompleteness using computational undecidability was deeper and provided more insight than Gödel's proof using "I'm unprovable."

BTW, "I'm unprovable." is a perfectly good and widely used mathematical gloss that is accurate and transparent for the Gödel sentence. It is not necessary to use the circumlocution. Carl (talk) 03:19, 24 April 2016 (UTC)

It's not a circumlocution. It's what the Goedel sentence literally says. "I'm unprovable" is not in fact what it literally says. But I understand why you would want to put it that way, because it is much more believable that "I'm unprovable" is not a mathematical statement per se, and in fact I agree that it's not a mathematical statement per se. The Goedel sentence, however, is one, quite obviously and unarguably, and claims to the contrary are not worth taking seriously. Note that I did not say that anything Chaitin said was not worth taking seriously, so your comment in that regard is misdirected. Trovatore (talk) 06:29, 24 April 2016 (UTC)

In any case, the idea that the Goedel sentence is "not mathematical" is held by such a small minority of writers - only Hewitt, as far as we have seen documented here - that per WP:DUE it should not be included in the article, correct or incorrect. There isn't any benefit to arguing over the correctness of the view. If it managed to get a significant minority of authors to support it, we would duly report on it here. But that has not happened at this moment in time. — Carl (CBM · talk) 12:21, 24 April 2016 (UTC)

The issue of whether Gödel's sentence is a valid sentence of mathematics was not addressed by Chaitin's quotation above.

Parenthetical remark in response to the above comment: Of course, Gödel's sentence is valid in Provability Logic. However, Provability Logic has been rejected as a foundation for mathematics of Computer Science in articles in Vol. 52 of Studies in Logic backed up by the published review by Professor Meyer. Security was the reason for the rejection of Provability Logic and Gödel's sentence "I'm unprovable."

Carl (talk) 14:07, 24 April 2016 (UTC)

It is not clear why Wikipedia should prefer untyped first-order theories (used by philosophers in previous work) over theories with strong parameterized types (preferred by many Computer Scientists). The incompleteness theorems come out differently depending on which is used.

Carl (talk) 14:31, 30 April 2016 (UTC)

First-order theories are simpler and have better-understood semantics. — Charles Stewart (talk) 06:19, 2 May 2016 (UTC)

Some very famous logicians have complained about first-order theories. For example, Barwise wrote

"The reasons for the widespread, often uncritical acceptance of the first-order thesis are numerous. The first-order thesis ... confuses the subject matter of logic with one of its tools. First-order language is just an artificial language structured to help investigate logic, much as a telescope is a tool constructed to help study heavenly bodies. From the perspective of the mathematics in the street, the first-order thesis is like the claim that astronomy is the study of the telescope."

Zermelo wrote that first-order theories are a fraud because that have complex and confused semantics since first-order theories cannot be categorical. For example, a first order theory cannot even axiomatize the integers up to model isomorphism.Carl (talk) 12:01, 2 May 2016 (UTC)

The quote of Barwise does not argue that we should abandon FOL as a tool in our toolbox. The issue with monsters in the semantics of first-order theories is well-understood and we have talked about this issue elsewhere. I don't think this article is the place for the controversy over FOL. — Charles Stewart (talk) 15:26, 2 May 2016 (UTC)

The quote by Barwise is a claim against the First-Order Thesis of some philosophers that first-order logic has primacy. In fact, working mathematicians and computer scientists do not use first-order logic. The relevance for improving this article is that incompleteness theorems come out differently using theories based on strong parameterized types used by Computer Scientists. Consequently, there is a division in the literature and it is not clear why Wikipedia should side with those in favor of the limitations of first-order logic.Carl (talk) 15:28, 3 May 2016 (UTC)

I don't see any significant "division in the literature", although it is true that your own papers use a different system. Can anyone give an example of any other well known source in computer science that discusses the incompleteness theorems in terms of theories involving "strongly parameterized types"? Moreover, can anyone give a general source about the incompleteness theorems that mentions "strongly parameterized types"? Textbook or general reference books would be most useful, because they would suggest a broader interest in the relationship between these topics. If the only sources on the relationship between the incompleteness theorems and theories with "strongly parameterized types" are in the work of Hewitt and his very close colleagues, my opinion is that there is not yet enough documented interest to warrant a mention in this article, much less any kind of significant revision. — Carl (CBM · talk) 16:54, 3 May 2016 (UTC)

There is now a strong division in the literature over first-order ZFC versus types for the foundations of mathematics (see the recent discussion in the Foundations of Mathematics BBoard). Computer Science is moving decisively in the direction of strong parameterized types with the standard programming languages pursuing this direction, for example, Java, C++, etc. The shift in foundations has consequences that are anathema to some very conservative senior philosophers who are determined to resist change as long as possible. Published literature on types has grown extensively in the last decade. However, terminology is not yet standardized. For example, sometimes parameterized types are called "generic" or "dependent". In any case, types are well on the way to becoming dominant in the foundations of mathematics and computer science.

CBM is proposing to dismiss a whole research community, symposia with publications, etc. until the results trickle down into textbooks. Adopting his recommendation could relegate Wikipedia to obsolesce, which would be a real disservice to Wikipedia users.

Carl (talk) 20:02, 3 May 2016 (UTC)

CBM is requesting that you provide objective evidence that there is a widespread acknowledgement, outside of your own personal circle, of the division you claim exists. Rather than provide them, you instead double down on the claim that "there exists" something, and engage in a straw-man argument. It's all nice and good for you to claim that something "is" happening, "is" being done, etc. If there is truly such a "strong division", such an apparently strong acceptance of the viewpoint, then it will not be a hard to exhibit support from beyond your personal circle. Support that does not rely on claims that videos are now the choice venue for publication of peer-reviewed scientific work, at any rate. Magidin (talk) 20:09, 3 May 2016 (UTC)

Some of the editors here don't seem to know the literature on types. There are many references in articles of Vol. 52 of Studies in Logic and too many other publications to mention here. Denying that the division is real is fruitless.

Video is now a publication medium of choice. In the case of CACM, a video is typically created to introduce and invite people to read the major article of an issue. Also, conference publications and electronic archives (for example HAL and ePrint) have become crucially important.

If Wikipedia does not keep up, then it will become increasingly obsolete.

Carl (talk) 21:21, 3 May 2016 (UTC)

"Please provide independent evidence" =/= "dismissing". "Please provide evidence" =/= "denial". Independent evidence =/= "You are clearly ignorant". Evidence =/= strawmen. Finally, if a video is an invitation "to read the major article of an issue", then how is video the main publication venue? It is the invitation to read the actual publication. Your own words here demonstrate that your earlier assertions were nonsense. Magidin (talk) 21:28, 3 May 2016 (UTC)

Science is not a popularity contest among articles with older articles and textbooks somehow carrying more weight. In active areas of Computer Science, older articles and textbooks are more likely to be inaccurate than more recent publications from prestigious sources. When a paradigm shift occurs, it takes textbooks a while to catch up with the consensus view.

Carl (talk) 23:39, 3 May 2016 (UTC)

Comment: User:Prof. Carl Hewitt, please provide specific suggested changes/additions, sourced according to guidelines mentioned in previous discussion, preferably with {{request edit}}. Baking Soda (talk) 00:19, 4 May 2016 (UTC)

{{request edit}}

I propose the following addition to the criticisms section:

Gregory Chaitin criticized Gödel's approach to incompleteness theorems as follows[“Dangerous Knowledge” BBC4 documentary. 2007.]:

"[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) 00:30, 4 May 2016 (UTC)

I think this is too popularized and glib to be informative here. —David Eppstein (talk) 01:24, 4 May 2016 (UTC)

Chaitin was totally serious. In fact, he was accusing Gödel of being too glib.Carl (talk) 02:18, 4 May 2016 (UTC)

the proof itself is valid and unambiguous. It says what it says and proves what it proves. if KG hadn't demonstrated it someone else eventually would have. the philosophical implications are debatable, fine...but what's the point of calling KG glib? I don't think anyone can understand what it is you're after/what your motivation is, mr. Hewitt....??68.48.241.158 (talk) 16:33, 4 May 2016 (UTC)

Even Gödel said that the Church/Turing proof of inferential incompleteness (using computational undecidability) was more fundamental.

Chaitin did not say that Gödel was personally glib; only that his proof is superficial and does not give any insight into how serious the problem is.

Independently of Chaitin comments pointing out the superficiality of Gödel's proof, the proof is valid in Provability Logic. But it is invalid in theories that use strong parameterized types because Gödel's sentence is not type correct.

Carl (talk) 18:09, 4 May 2016 (UTC)

Although the subject of the incompleteness theorems can be very motivating, I want to try to gently encourage everyone to focus on article content only, avoiding personal discussion and avoiding side topics about the incompleteness theorems. In the case of the proposed edit, I think it is clear there is no consensus to make it at the moment. The same edit had already been proposed and considered. I think that making the same request repeatedly, with no revision, is unlikely to lead to consensus. — Carl (CBM · talk) 17:00, 4 May 2016 (UTC)

Regarding the proposal above, I like the fact that it is concrete. I think that the article should mention Chaitin's work. Of course, we do have two paragraphs about Chaitin's work already. As for putting in the long quote above, I am not convinced that we should cite a video interview. Chaitin has never been hesitant to put his ideas into writing, so if this criticism is something he has seriously pursued, I am sure that it should be possible to find it in print. One among many concerns with trying to cite videos: how can one obtain a copy of this video to see what Chaitin actually meant? I am glad to obtain books from the library, but videos are much more difficult to obtain. So, unless there is some special reason why a video is the only possible source, I prefer to stick to ordinary sources. I have never seen a need to cite a video in other scientific papers on the incompleteness theorems. — Carl (CBM · talk) 12:21, 24 April 2016 (UTC)

Videos are increasingly becoming the scientific publication medium of choice. From the video, it is clear that Chaitin takes his video interview at least as seriously as any of his written publications. Also Chaitin chose these words for the interview because he believes that they go to the very heart of the matter of his critique of Gödel's sentence "I'm unprovable." Since the video is by BBC, it is readily available in many libraries, can be purchased from BBC, and can even be viewed online for free. Carl (talk) 14:07, 24 April 2016 (UTC)

More problematically, the documentary cited above is a work of popular science. Such sources have a tendency to over-simplify or over-exaggerate their statements. In so far a this article should discuss the views of Chaitin, it should do so based on proper scientific sources. —Ruud 14:14, 24 April 2016 (UTC)

Actually, “Dangerous Knowledge” is a serious documentary by a very well qualified scientist, which should not be dismissed as "popular science." It is highly recommended to better understand important historical and scientific issues. Carl (talk) 17:15, 24 April 2016 (UTC)

In "Thinking about Godel and Turing: Essays on Complexity 1970-2007", Chaitin wrote:

"You see, the real problem with Gödel's proof is that it gives no idea how serious incompleteness is."

Carl (talk) 20:38, 24 April 2016 (UTC)

This does appear to be potentially a usable quote. --Trovatore (talk) 21:48, 24 April 2016 (UTC)

While it is a quote from a book, that quote on its own, with zero surrounding text, is not a reasonable addition to the article. It would not make any sense to just put in a one-sentence quote with no context. What is the actual addition to the article that is being proposed? Also, what page number is the quote from? — Carl (CBM · talk) 10:00, 25 April 2016 (UTC)

Actually, the best Chaitin quotation that I have found for the article is the one from the video because it is fundamental, relatively self-contained, and directly on-point. Consequently, I propose the following addition to the criticisms section:

Gregory Chaitin criticized Gödel's approach to incompleteness theorems as follows[“Dangerous Knowledge” BBC4 documentary. 2007.]:

"[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) 12:17, 25 April 2016 (UTC)

I think the quote is both too long and not clear enough to be included, without further explanation. I would want to see more or the transcript, and to see which of "Godel's argument(s) for incompleteness" was intended. I don't see how it could possibly apply to the second incompleteness theorem or the arguments for that theorem, but I don't know what Chaitin intended. Also, this is only allowable if Chaitin is an expert on incompleteness theorems, which I consider not proven. BBC's selection of Chaitin as an interview subject only means he has interesting ideas on Godel's incompleteness theorems; the BBC's editorial boards are not commenting on whether they think Chaitin is an expert. It's a little more complicated than I thought at first. I had thought that a single sentence: "Gregory Chaitin stated that Godel's approach to incompleteness was superficial and glib," but even that presumes that we believe his opinion is important, which I'm not sure can be justified. — Arthur Rubin (talk) 22:13, 4 May 2016 (UTC)

the problem is he wants a quote inserted that lacks any context whatsoever...if he wants something included he needs to bother to also construct a context for it too...then people can determine whether the info is notable enough to be worth including...that quote out of context is totally meaningless..soo it's ridiculous to even entertain it...this needs to be explained to him...68.48.241.158 (talk) 22:46, 4 May 2016 (UTC)

Because Dr. Hewitt is active here, you could also explain your thoughts to him; someone could misunderstand your comment to suggest that he is not active here. I really want to encourage everyone to focus as much as possible on article content, rather than personal remarks, which too often only make conversation more difficult. If you think that the case for including the proposed material is not sufficiently strong yet, then you are certainly not alone. In the end, if Hewitt has a vision for some edits to the article, he will need to present a case that is convincing to the other editors here, and build consensus. There are quite a few expert editors here, so anything that is too unusual will be commented on by someone or the other, I am sure. — Carl (CBM · talk) 23:55, 4 May 2016 (UTC)

Re Arthur: Chaitin has published many books on his work on incompleteness, so I think we should not be worried about his credentials. But that same volume of publications - Chaitin is not known to be reluctant to write about his work - means there should be a book or paper that can be used as a source, instead of a video. The lack of context is also a significant issue, I agree - it would not make sense to just make a "coat rack" in the article from seemingly random quotes about the incompleteness theorems. I am not sure that the quote by Chaitin is really a "criticism" in the same way that, say, comments by Finsler or Zermelo could be called "criticisms". Chaitin's writings that I have read seek to emphasize the importance of incompleteness, rather than to argue that the incompleteness theorems are somehow incorrect. Without more significant context, it is hard to see exactly the point that Chaitin is making in the quote. — Carl (CBM · talk) 23:51, 4 May 2016 (UTC)

new paragraph in intro

"Soda" suggested to put this in TALK...I personally don't love the new paragraph that much in general (erasing it altogether would be fine probably)..but tried to improve it...the version it has been reverted back to now is both a bit wordy and vague at spots...and the phrasing just seems clumsy overall...I'd say what I had is better than it stands now...but what I had could also be improved, of course..68.48.241.158 (talk) 20:08, 2 May 2016 (UTC)

the "restrict what problems can be solved" phrase seems vague and odd to me for one..68.48.241.158 (talk) 20:10, 2 May 2016 (UTC)

Saying that theorems restrict things is common enough in math jargon, but it is certainly likely to be confusing to some readers. I edited the paragraph some. — Carl (CBM · talk) 20:22, 2 May 2016 (UTC)

I liked my try at it better because it avoided the brief attempts at explaining the other referenced results (as these kinds of brief explanations are doomed to fail)...right now it has that parenthetical "(to determine whether a statement follows from some axioms)"...this is so vague it can't possibly be considered accurate in regards to what it's supposedly explaining..I think those first two paragraphs are quite good and tight at this point so should be careful about adding new stuff right in the intro that isn't yet up to par..68.48.241.158 (talk) 22:11, 2 May 2016 (UTC)

I was waiting for the other editor to comment; I just made some small changes to the wording. — Carl (CBM · talk) 23:55, 2 May 2016 (UTC)

I am fine with 68's changes after last edit, just make it clear which problems belong to logic and which to computability. Church-Turing Thesis can also be mentioned (extent and limitations of what can be computed). Baking Soda (talk) 11:56, 3 May 2016 (UTC)

With preference for mentioning formal system instead of formal logic (comment in revert text).... Baking Soda (talk) 11:58, 3 May 2016 (UTC)

Paradigm shift and interviews

As CBM has noted, we do not accept a paradigm shift until it is accepted by scientists in general, nor do we notice an alleged paradigm shift until after it is noticed by scientists or the public, in general. Prof. Carl Hewitt, we have seen no evidence of that in regard your work.

As for video interviews, I would normally wait for the book (or transcript) to be published, and the interviewee to have time to explain his comments. Wikipedia does not demand peer-reviewed papers as sources, but a statement in interview may or may not have been well-thought-out. — Arthur Rubin (talk) 21:53, 4 May 2016 (UTC)

it's not clear what Hewitt even wants...can you explain what "paradigm shift" he's even advocating?? but, yes, his contributions are distracting and difficult to make any sense of (perhaps intentionally)..68.48.241.158 (talk) 22:07, 4 May 2016 (UTC)

Important Scientific Documentary

The following discussion is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

---

“Dangerous Knowledge” is an important scientific documentary that should be viewed by everyone who has an interest in the subject of this article. In the documentary, Chaitin (a world class authority) made a considered serious scientific judgment after long reflection about the merits and significance of Gödel's approach to the incompleteness theorems which are the subject of this article.

Wikipedia should not take sides in this dispute. Instead, Wikipedia should report faithfully and accurately.

I propose the following addition to the criticisms section: Gregory Chaitin criticized Gödel's approach to incompleteness theorems as follows[“Dangerous Knowledge” BBC4 documentary. 2007.]: "[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."

you're going to get yourself blocked again if you keep this up...if you want to continue like this you should hang out in the ARGUMENTS TALK...68.48.241.158 (talk) 13:51, 5 May 2016 (UTC)

Controversies vs. Paradigm Shifts

Wikipedia should report on published controversies in the literature. For example, controversies about human-caused global warming can be reported concerning evidence and arguments. Of course, Wikipedia should not take sides in the controversy. For example, Wikipedia should not take sides concerning Chaitin's characterization of Gödel's approach to the incompleteness theorems. Instead, Wikipedia should report the controversy fairly and accurately.

On the other hand, paradigm shifts can be reported after the fact when a new consensus is gained contrary to a previous consensus.

PS. I had to type the above more than once because of edit conflicts.

Carl (talk) 14:11, 5 May 2016 (UTC)

this is inappropriate for this talk page...calm down and try to read again what people have tried to explain to you about how Wikipedia works..it's nothing personal..68.48.241.158 (talk) 14:04, 5 May 2016 (UTC)

Unfortunately, there is considerable danger that once again Wikipedia is going to be caught out taking the wrong side of a published scientific controversy. But I freely admit that I am powerless over other editors. All I can do is present the best evidence and arguments that I can.Carl (talk) —Preceding undated comment added 14:32, 5 May 2016 (UTC)

if at the current time the supposed controversy is viewed by consensus as a fringe one then it will not be included in the article..this is how Wikipedia works...on the other hand, I don't believe you've been putting forth fully formed and coherent suggestions for additional content...but more or less asking the same out of context material be randomly asserted over and over again...things will go better if you modify this behavior..68.48.241.158 (talk) 14:37, 5 May 2016 (UTC)

Since Baking Soda has shut down discussion here of the proposed addition of Chaitin's critique to the article, it seems that discussion has moved instead to my talk page where I have proposed a fully formed suggestion for additional content. Suggestions for improve are greatly appreciated.Carl (talk) 15:10, 5 May 2016 (UTC)

he rightfully closed it and this thread should be closed too...you've just repeated the same request again and again...you're now repeating the same request on your talk page (where it shouldn't be)...come back when you have something new or fully formed...otherwise hang out in the ARGUMENTS TALK..68.48.241.158 (talk) 15:15, 5 May 2016 (UTC)

You could bring back the Chaitin' proposal from my talk page if you wish. It probably does not belong in the ARGUMENTS page because it is proposed wording for addition to the article and not about contents issues associated with the article.Carl (talk) 15:48, 5 May 2016 (UTC)

If anyone is interested at this point: I found the video where the quote Hewitt is so interested on youtube...it's toward the end where they transition from Gödel's work to Turings...it's from a pop documentary that's well/expensively produced but is also prone to a lot of pop goofiness/inaccuracies...https://www.youtube.com/watch?v=ezYdCU2nZbo....all Chaitin is basically saying is that Gödel's paper is quite abstract (which is true, I suppose) whereas Turing's work was aimed at a more practical application (which is true too, I suppose)...Chaitin is basically saying that he relates better to Turing's work...but so what? It's not encyclopedic that a particular person relates more to one thing than another...and the supposed "controversy" that Hewitt believes exists is no where in the record....68.48.241.158 (talk) 15:24, 6 May 2016 (UTC) at about 18:1068.48.241.158 (talk) 15:26, 6 May 2016 (UTC)

The crux of Chaitin's valid criticism was that Gödel's proof is superficial and does not give any insight; which IMHO has been amply borne out by subsequent developments.

The video "Dangerous Knowledge" is a serious scientific documentary that compares favorably with the current state of this Wikipedia article.

Carl (talk) 06:49, 7 May 2016 (UTC)

I've pretty much said all I can say on your talk page at this point..but what is this phrase, "and does not give any insight"?? It doesn't even seem to be a complete thought...doesn't give any insight into what?? the proofs demonstrate what they demonstrate. Turing's work demonstrates what it demonstrates. etc etc etc...Turing's work, for example, gives no insight into, say, the 2005 New York Yankees. I suppose, therefore, Turing's work "gives no insight." 68.48.241.158 (talk) 13:05, 7 May 2016 (UTC)

Unfortunately, you seem to have missed the point: The crux of Chaitin's criticism was that Gödel's proof is superficial and as Chaitin said "does not give any insight into how serious the problem [of incompleteness] is." Subsequent research in Computer Science (e.g. Vol. 52 of Studies in Logic) have borne out the correctness of Chaitin's criticism. Inferential undecidability (and it's stronger version incompleteness when models are available) are of crucial importance in classical mathematical theories. Carl (talk) 17:32, 7 May 2016 (UTC)

who cares if someone thinks that "incompleteness" (which isn't a term Gödel particularly ever used) is "serious" or not? and what on earth might they mean by saying it's "serious."?? these kinds of vague opinion statements aren't encyclopedic...if you've got stuff related to it's relevance to the Hilbert Program, stuff about how it relates to computability, then suggest it...otherwise...68.48.241.158 (talk) 13:29, 7 May 2016 (UTC)

According to Vol. 52 of Studies in Logic, Inferential undecidability (and its stronger form incompleteness) are far more important than the formal consistency proof (using proof by contradiction) of the Dedekind/Peano theory of natural numbers. A proof of constructive consistency would be interesting, fundamental, and helpful; but it looks very difficult. Carl (talk) 19:00, 7 May 2016 (UTC)

that's an opinion (and it may be a fine one)..but it can't be construed as a specific suggestion for new content to improve this article, so is inappropriate for this talk page...they created an "arguments" talk because people often have a strong desire to discuss this topic for fun etc...68.48.241.158 (talk) 18:30, 7 May 2016 (UTC)

The results in Vol. 52 of Studies in Logic, support the proposed addition of Chaitin's critique of Gödel's approach to the incompleteness theorem. Carl (talk) 19:00, 7 May 2016 (UTC)

No consensus at this point for quote addition as mentioned in close, however, you can go ahead add suggestion to wikiquote, a {{wikiquote}} may be added to related pages on Wikipedia afterwards... Baking Soda (talk) 19:29, 7 May 2016 (UTC)

There is a split between some senior conservative philosophers and some upstart Computer Scientists. The controversy made it difficult to come to a consensus here. It will be interesting to see what happens next. Carl (talk) 03:52, 9 May 2016 (UTC)

I don't believe there to exist any such controversy...and you haven't pointed to any third party sources to suggest such (and you haven't even been able to articulate what you to believe this "controversy" is)..and making once again the vague statement that the theorems "give no insight" and pointing to some journal doesn't count...68.48.241.158 (talk) 10:06, 9 May 2016 (UTC)

The controversy is between advocates of first-order ZFC and advocates of strong parameterized types for mathematical foundations. Advocates of strong parameterized types back up Chaitin's criticism of Gödel's sentence I'm unprovable because the sentence is not valid using strong parameterized types. Carl (talk) 00:05, 10 May 2016 (UTC)

The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

first sentence again

the change doesn't bother me very much and it's correct as far as things go...of course in this letter Gödel is speaking a little informally and not as precisely as he would otherwise...it was understood exactly what he meant...there's the slight problem "containing" could be interpreted as, indeed, containing...whereas the proof demonstrates that a formal system can't contain arithmetic...68.48.241.158 (talk) 14:24, 11 May 2016 (UTC)

Now you are being somewhat informal, using "contain" in a rather fuzzy sense (as in, being able to prove all true statements, perhaps?). And of course, it's not true that no formal system can do that: just that certain formal systems that satisfies the technical requirements of the proof cannot be both consistent and complete. Magidin (talk) 15:29, 11 May 2016 (UTC)

yeah, more or less...the point being the change is potentially misleading/confusing/inaccurate...if you look at the first discussion above on "first sentence" you'll see we first tried to get very precise (but had quite a hard time) so decided to go 'full vague' in a sense with "of a certain expressive power," which is what it was before this recent change...personally, I originally liked a phrase along the lines of, "capable of expressing the arithmetic of the natural numbers."..any ideas?68.48.241.158 (talk) 15:39, 11 May 2016 (UTC)

The lede cannot be too technical; it just scares people away. I think it's better that it convey the general sense, even if it may leave a wrong impression on someone who does not read beyond the lede; clarification and precise technical conditions should be left to the more expansive sections. I was okay with the prior version; I'm not overly worried about the current one (though perhaps I would change "containing arithmetic" to "that includes enough arithmetic" or some such wording to signal that there is some technical issue going on (the "enough" being the the signal here; the "certain" being the signal in the prior wording). Magidin (talk) 16:16, 11 May 2016 (UTC)

yeah, it can certainly remain as it is for now..something that is obviously better/improving might come up...I'm wary of phrasing along the lines of "enough arithmetic" as I think it sounds kind of odd and that in the context of this topic arithmetic was (is?) understood as all of arithmetic (ie addition/multiplication (and their inverses) of the natural numbers)..68.48.241.158 (talk) 16:51, 11 May 2016 (UTC)

--- A caveat about the wording as it stands: apparently the letter to Nagel was only a draft and never sent (at least no evidence exists of a sent letter). But the commentators Parsons and Sieg go on to reference Davis 1965 (The Undecidable) pp. 71-73 that I quote immediately below. Another version also appears in van Heijenoort.

In both cases (published as addenda, as opposed to in letters sent or unsent) Goedel wrote the notion "arithmetic" in a more-formal way as follows; but observe the word "containing" and "contains":

“. . . every consistent formal system containing a certain amount of finitary number theory.” (Postscriptum dated June 3, 1964 to his 1934 lecture-notes as recorded by Kleene and Rosser, found in the Undecidable on p. 71-73)

Goedel references these pages 71-73 in a letter to David F. Plummer (Volume V Correspondence H-Z:162). In a footnote in the [copy? of the] Plummer letter an annotation was added by Goedel that appears in footnote “a” on page 161 (Volume V):

"In addition to the footnotes there is an annotation saying “number theoretic statt arithmetic an 2 stellen” (“number-theoretic instead of arithmetic in 2 places”)".

A slightly earlier published version (but when was it written?) appears in van Heijenoort:

. . . it can be proved rigorously that in every consistent formal system that contains a certain amount of finitary number theory there exist undecidable arithmetic propositions and that, moreover, the consistency of any such system cannot be proved in the system.” (‘’Note added 28 August 1963’’ to his 1931 that appears in van Heijenoort. The “note” appears on page 616.

But we have to be very careful because in both instances Goedel is referencing Turing machines as his “formal system of choice”; this was where his later thinking had arrived: formal system = Turing machine:

“A. M. Turing’s work[footnote 69: In my opinion the term “formal system” or “formalism” should never be used for anything but this notion] . . .” (van Heijenoort: 616).

The full quote of the first quote’s wording would be too long. But in it he states point-blank that

"A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas. [He references his lecture-notes where he uses “finite procedure” p. 41 (The Undecidable) and says “finite procedure” should be “understood to mean ‘mechanical procedure’”.] This meaning, however, is required by the concept of formal system, whose essence it is that reasoning is completely replaced by mechanical operations on formulas.” (Undecidable:72).

So if we were to take Goedel's more formal words we have something like this:

". . . every consistent formal system (mechanical procedure for producing formulas) containing a certain amount of finitary number theory."

I don't like this last part (certain amount of finitary number theory) because the reader will wonder: what does "a certain amount of finitary number theory" mean? My reference being Hardy and Wright titled "An Introduction to the Theory of Numbers", I see on page viii and the first two pages (!) the elementary concepts of "number theory" introduced as the conventional symbols + and -, the symbols for implication →, "equivalent to" ≡, "integer", "divisor", "prime number", "product", "sum" and lastly what looks like Goedel numbers (a product of primes to various powers) at the bottom of page 2. And from what I gather that's about all the "arithmetic" (aka "number theory") we need -- the page viii and the first two pages of Hardy and Wright. So I'd stick with "arithmetic", but maybe add the word "consistent" and add, as a footnote, "mechanical procedure for producing formulas" and reference it as a direct quote. And to fortify the word "arithmetic" we could add Goedel's more formal words to the existing footnote, i.e.:

". . . every consistent formal system [footnote: direct quote from Goedel "mechanical procedure for producing formulas" with appropriate reference] containing arithmetic [Add to footnote, or add a second footnote, the direct quote from Goedel: "a certain amount of finitary number theory" plus the appropriate reference].

Wvbailey (talk) 18:52, 11 May 2016 (UTC)Bill

in the actual paper he doesn't really dwell on any of this at all but for briefly in the introductory section...he states, "..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." 68.48.241.158 (talk) 19:22, 11 May 2016 (UTC)

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) 19:35, 11 May 2016 (UTC)

[Raatikainen 2015] claim in article is incorrect

The article contains a claim from [Raatikainen 2015] that is incorrect, namely,

For any formal effectively generated system T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent.

The above claim is correct only for untyped theories that allow fixed points for sentences that allow the construction of Gödel's sentence "I'm unprovable." For example, the above claim does not hold for the theory ℕ.

Carl (talk) 20:22, 26 June 2016 (UTC)

Is the claim reported accurately? If your claim is that the quote is inaccurately reported, then please provide the correct quotation. If the article in question contain this quote as given, and your objection is that the claim is false, then your comment is out of order: the threshold for inclusion in Wikipedia is verifiability, not truth; see also the previous wording of the verifiability pillar. Magidin (talk) 22:04, 26 June 2016 (UTC)

Wikipedia articles should be accurate and this one contains an inaccuracy. The inaccuracy has been reported by other publications and the quotation should not be recommended as being factual in the Wikipedia article without mentioning that the quotation has been correctly reported as inaccurate in other publications.

One way to correct the article would be to remove the inaccurate quotation. Another way would be to amend the quotation to state that tohe effectively generated system T must have the statement "I'm unprovable."

Carl (talk) 22:48, 26 June 2016 (UTC)

(I deleted a previous comment that based on a misunderstanding.) The text mentioned above was not a direct quote. The article neither included quotation marks nor cited the text to Raatikainen. In my opinion, this sort of thing is one reason to look for direct quotes for these theorem summaries.

I have replaced the entire previous text with a direct quote by Raatikainen paraphrasing the second incompleteness theorem (and now including quotation marks and a citation). The new language does, also, include the assumption that the theory in question is able to state the consistency principle for the second incompleteness theorem. I was confused at first because the sentence "I am unprovable" is related to the first incompleteness theorem, but the quote in question is related to the second incompleteness theorem. — Carl (CBM · talk) 00:44, 27 June 2016 (UTC)

Unfortunately, the following quote is also incorrect:

"Assume F is a consistent formalized system which contains elementary arithmetic. Then $F\not \vdash {\text{Cons}}(F)$." (Raatikainen 2015)

An assumption is still needed that F has Gödel's sentence "I'm unprovable." For example, the formal system ℕ (which contains elementary arithmetic) proves its own consistency, which is OK becuase ℕ is strongly typed and consequently does not have the sentence "I'm unprovable."

Carl (talk) 00:57, 27 June 2016 (UTC)

Prof. Hewitt, I think it would facilitate discussion if you would translate your comments into standard terminology, or failing that, at least note the differences and explain them in such a way that they can be understood. As I'm sure you're aware, in usual math-logic nomenclature, ℕ is not a "formal system" at all, but rather a structure. --Trovatore (talk) 02:05, 27 June 2016 (UTC)

All of this goes back to the Dedekind/Peano theorem that ℕ is up to a unique isomorphism the only model for the Dedekind/Peano axioms for the natural numbers. For convenience, the strongly typed theory of the Dedekind/Peano axioms is also called ℕ, which is OK because there is only one model up to unique isomorphism. Of course, ℕ is not a first-order theory of the predicate calculus and in fact is much more powerful than first-order ZFC.

The incompleteness theorem can be proved for the theory ℕ even though "I'm unprovable." is not a valid proposition of ℕ. Instead there is a different proposition than "I'm unprovable." which is known to be true in the model ℕ but unprovable in the theory ℕ.

Carl (talk) 04:40, 27 June 2016 (UTC)

If there is only one model up to isomorphism, then the underlying logic is something stronger than first-order logic. Therefore the Goedel theorems do not apply. This is not really news. --Trovatore (talk) 04:31, 27 June 2016 (UTC)

Although it does not matter terribly in this case, please note that it is considered bad form to modify your remarks after someone has responded to them, at least without making it clear that you have done so. --Trovatore (talk) 04:45, 27 June 2016 (UTC)

The conflicting edit above was unfortunately made concurrently with yours. Gödel's incompleteness theorems were originally for Principia Mathematica, whose type system was unfortunately not up to modern standards. Subsequently, to save his results from Wittgenstein's devastating criticism, Gödel retreated to first-order provability logic, which is inadequate as a mathematical foundation for computer science. Computer scientists further developed strong parameterized typing, which is the basis of the theory ℕ. Carl (talk) 04:58, 27 June 2016 (UTC)

When there is an edit conflict after someone has responded to your remarks, it is nevertheless still good form to note that the remarks have been changed after the response.

The rest of your remarks are not on-topic; my request was simply either to use standard language, or to explain the differences when you use nonstandard language. --Trovatore (talk) 05:43, 27 June 2016 (UTC)

My edit was marked "edit conflict" and then I immediately responded above as follows "The conflicting edit above was unfortunately made concurrently with yours."

I respectfully disagree that my comments above were not on topic. It was entirely relevant to point out that Gödel's incompleteness theorems were originally for Principia Mathematica. It was also relevant to point out that Gödel retreated to first-order provability logic in the face of Wittgenstein's devastating criticism. Unfortunately, this history was lost and some conventional opinion became that the incompleteness theorems were just for first-order logic.

Also, I explained the current use of ℕ for the strongly typed theory of the original Dedekind/Peano axioms, which is much stronger than the cut-down first-order version of the axioms.

Carl (talk) 16:00, 27 June 2016 (UTC)

The term "contains" includes the assumption that the language of the theory F includes the language of arithmetic (or at least interprets it), and hence includes all sentences in that language, at which point the sentence Con(F) will be part of the language of F (perhaps via the interpretation). For example, Peano Arithmetic and ZFC both satisfy this assumption. The consistency statement for any effective theory is just a universal sentence ($\Pi _{1}^{0}$) in the language of arithmetic.

In any case, now that the article uses a direct quote, if you feel the quote is in error I recommend contacting the author of the SEP article. In my experience, SEP articles are updated from time to time and can be corrected. The quoted text is in agreement with many other reliable sources on the incompleteness theorems. Moreover, even if we try to add some kind of disclaimer here, the claim might still be incorrect in the SEP article! I am glad that this discussion helped improve the article by replacing the unquoted summary with a direct quote from a source that is clearly reliable. — Carl (CBM · talk) 01:20, 27 June 2016 (UTC)

Since more recent scientific publications are more authoritative than older ones, they typically are given greater weight. In this case, there are publications of the same 2015 vintage that differ and it seems fair to say that currently there is no settled consensus between some philosophers and computer scientists. I expect that the SEP article will soon be clarified to reflect that the quotation above needs the additional assumption "I'm unprovable." Of course, adding this assumption drastically narrows the applicability of the theorem in [Raatikainen 2015]. The narrowing of [Raatikainen 2015] explains why it is legitimate that ℕ proves its own formal consistency without itself immediately falling into inconsistency. Of course, proving the constructive consistency of ℕ (proof that no inconsistency can be derived from the strong type theory axioms of ℕ) is an important open problem.

One bone of contention between some philosophers and computer scientists is strong typing of expressions and propositions. Computer scientists want strong typing for clarity, efficiency, groundedness, and blocking known mathematical paradoxes including those resulting from allowing "I'm unprovable." Conservative philosophers want to stick to untyped first-order propositions allowing use of the Y fixed point construction to create the sentence "I'm unprovable." Many computer scientists do not see any practical benefit of allowing sentences like "I'm unprovable."

Carl (talk) 19:30, 27 June 2016 (UTC)

.... aaaaand, we're back to the same old drum being beaten yet again, with nothing new to add. Just harping on it again. Are you really hoping that waiting three months will change the consensus? Or is it really more a strategy of repeating the same thing until everyone but you is sick and tired of it? If you have nothing new to say or add, then stop. Magidin (talk) 06:10, 27 June 2016 (UTC)

@Magidin:Of course, you have the right to side with conservative philosophers in an ongoing scientific debate. However, the consensus claimed by some conservative philosophers has been steadily eroding. It is actually conservative philosophers who have nothing new to say while computer scientists have been making steady progress.

I will see Zalta on the 4^th and will see if the SEP article can be rapidly repaired.

Carl (talk) 16:14, 27 June 2016 (UTC)

I thank Prof Carl Hewitt for granting me a right that is not in his power to either grant or withhold. I also thank him for trying to change the discussion from the matter I actually addressed, which is his behavior on Wikipedia, to the one in which he prefers to dwell (the substance of his claims), thus demonstrating that he misses this point as he misses all others. I will further thank him if in the future he ceases from wasting his time trying to read my mind or wasting his breath pretending to have powers he lacks, such as those in which he grants me permission to do things. Meanwhile, he can stop wasting everyone's time by not bringing up the same thing over and over again when there has been no substantial change in the underlying matter, other than his own impatience with the lack of appreciation of his alleged genius. Magidin (talk) 16:25, 27 June 2016 (UTC)

@Magidin:It would be nice if the level of discourse here could rise above the level of personal insults.

For editors who are interested in following the scientific debate, I recommend the following: , , as well a numerous YouTube videos.

Carl (talk) 16:46, 27 June 2016 (UTC)

References

Absolutely: you can start by not insulting me or my intelligence with your condescending remarks about my rights, or with your continual insults towards those who disagree with you, which are of course carefully couched in ways that make them subtle, but insulting nonetheless. And you can continue by not insulting everyone here by beating the same drum over and over again when you have absolutely nothing new to provide, all the while making snide remarks about how you are on the forefront of things while others are stuck on the past (in your clearly never humble opinion). Perhaps then the discussion can rise to the levels you claim to aspire to. And with that, having received your blessing and permission to do as I see fit anyway, I will stop for now. Magidin (talk) 17:01, 27 June 2016 (UTC)

@Magidin:You are mistaken: computer scientists have made steady progress on the topics of this article. For example, there is a growing consensus that the theory ℕ (rather than first-order logic) is the proper mathematical foundation for computer science. Furthermore, there is a growing consensus that ℕ can indeed legitimately prove its formal consistency. This will require a revision of the SEP article and consequently a revision of the current Wikipedia article concerning the "2^nd incompleteness theorem." Also, the Wikipedia article will need amplification with respect to the "1^st incompleteness theorem" because I'm unprovable. is not a valid proposition of ℕ because of strong parameterized typing. Instead there is a different proposition (due to Church, namely, Proofs of ℕ are computationally enumerable.) that is unprovable in the theory ℕ but true in the up to unique isomorphism only model of the theory.

One of the great tragedies of Wikipedia is the lack of prestigious academic contributors, which is very different from the state of affairs that prevailed for traditional encyclopedias. A page that says Experts are scum. should definitely not be tolerated on Wikipedia. Insults and bullying should have no place on Wikipedia.

Carl (talk) 11:55, 28 June 2016 (UTC)

Are you an expert?

I see page up and page down here you trying to convince people that you are an expert at something (and the only expert at that something). Such behavior is almost always associated with crackpots and cranks. Expert? Crackpot? Crank? In between? YohanN7 (talk) 12:10, 28 June 2016 (UTC)

I should add that I don't say you are any of the above. I say that most people pushing points of view hard on talk pages do come across as cranky. Always. YohanN7 (talk) 14:28, 28 June 2016 (UTC)

Dr. Hewitt, it is perhaps worth remembering that you are interacting here with other experts on the subject of the incompleteness theorems. Of course, the incompleteness theorems are correct, so either the system $\mathbb {N}$ fails to meet one of the hypotheses of the incompleteness theorems, or it satisfies their conclusions. But, because the system $\mathbb {N}$ is not (yet, perhaps) of widespread scientific interest, there is no need to for us worry here about which of those options holds, and indeed this talk page is not the place to worry about such things in the first place. If the system $\mathbb {N}$ does not meet the hypotheses of the incompleteness theorems, which is what you appear to claim, then I see even less reason to give it significant attention in this article.

But the main concern I see is (still) a lack of independent sources to corroborate the claim that "there is a growing consensus that ℕ (rather than first-order logic) is the proper mathematical foundation for computer science". Until additional, independent sources are located, it would be inappropriate for us to make large changes to this article to accommodate the system $\mathbb {N}$. — Carl (CBM · talk) 12:15, 28 June 2016 (UTC)

A question of concern here is improving the accuracy of the article.

As explained above, incompleteness holds for the theory ℕ which is very old (being fundamentally due to Dedekind followed by Peano) although details of its axiomatization using strong parameterized types occurred more recently. The key problem that was solved by using strong parameterized types was to avoid inconsistencies in mathematics due to paradoxes, such as Berry and Girard. It is important to note that ℕ (as opposed to first-order logic) is a foundational theory in current use by almost all working mathematicians and consequently it is of fundamental importance.

Some philosophers attempted a retreat to first-order logic as the foundation for mathematics. The retreat was opposed by Zermelo and later by Barwise. Also, working mathematicians paid almost no attention to first-order logic. A turning point came when computer scientists realized that first-order logic is antithetical to their work on model checking because nonstandard models of first-order axioms have unwanted monsters like infinite integers and infinitesimals.

It is important to read the references above and to view YouTube videos in order to be scientifically up to date. As you know, work in this area can be highly technical and the exact wording of theorems and argumentation can be crucial. Fixing inaccuracies in the article is entirely appropriate given the publications that are available.

Carl (talk) 13:13, 28 June 2016 (UTC)

"It is important ... to view YouTube videos in order to be scientifically up to date": I have never heard any scientific progress being first published as a YouTube video. If, for applying to a position in my university, someone would present YouTube videos as research results, he would immediately be refused. I know that philosophy is not science, but mathematics is, and, here, we are talking of mathematics and mathematical logic. Using YouTube videos as arguments in a scientific debate is a strong indication of the weakness of the argumentation. D.Lazard (talk) 14:14, 28 June 2016 (UTC)

@D.Lazard:Of course, the following written publications (which you deleted) were prominent in my actual statement: ,

References

Videos are becoming increasing important scientific publications at top-ranked universities around the world. Even prominent old school philosophers of mathematical logic are now resorting to creating video series on YouTube :-) Universities that deprecate videos will not be competitive.

Carl (talk) 14:35, 28 June 2016 (UTC)

This particular issue can be addressed quite simply, I think. Prof Hewitt's complaint, boiled down, turns out to be that the informal statement does not apply outside of first-order logic, at least not without additional care. That is certainly true. I propose that the old, non-direct-quote be restored, and that it be made clear that it is talking about first-order logic.

(No one has to convince me, by the way, that first-order logic is not the be-all and end-all; I think the other participants are well aware of that. The point, though, is that the Goedel theorems, in their original and most direct form, are about first-order logic, and that's really all we have to say.) --Trovatore (talk) 18:09, 28 June 2016 (UTC)

Of course, Gödel's original results were for Principia Mathematica (and not first-order logic) as the foundation for the mathematics of its time including the Dedekind/Peano axiomatization of the natural numbers. Gödel later retreated to first-order logic in an attempt to salvage his results from Wittgenstein's devastating criticism.

First-order logic was invented later, but never adopted as foundational by working mathematicians. Theorems, which are of interest to some philosophers, can be proved about first-order logic theories that are not true in the actual foundations used by working mathematicians.

Carl (talk) 18:37, 28 June 2016 (UTC)

Your interpretation of the historical sequence is ... at variance with my understanding, but that's for the history section, not under discussion here. --Trovatore (talk) 19:27, 28 June 2016 (UTC)

The incompleteness theorems apply much more broadly than first-order logic (although this is rarely emphasized in modern introductions). For an easy example, they also apply to second-order systems such as second-order Peano arithmetic, which not able to prove its consistency under any effective deductive system (categoricity is irrelevant, because the incompleteness theorems are syntactic). More generally, the incompleteness theorems also apply to type theories and to other effective formal systems that are sufficiently strong to interpret an appropriate fragment of arithmetic. Of course, the Goedel sentences obtained will be in the image of the interpretation, but once we know that the language of arithmetic is interpretable, we can form a Goedel sentence as usual within arithmetic and then push it through via the interpretation (e.g. this is already necessary to apply the incompleteness theorems to ZFC). — Carl (CBM · talk) 19:39, 28 June 2016 (UTC)

Since the article is about Gödel's incompleteness results, it is important to point that they were for Principia Mathematica (and not first-order logic) as the foundation for the mathematics of its time including the Dedekind/Peano axiomatization of the natural numbers. Some references should be found for the later transition to first-order logic in the light of Wittgenstein's criticism.

Carl (talk) 19:54, 28 June 2016 (UTC)

Goedel had recognized by his 1934 Princeton lectures that the theorems easily applied to many other logical systems than just the system P from his paper; this is why he did not write/publish the second part of his paper that part 1 had promised. Wittgenstein's remarks seems to have come much later. Of course, the very terminology "first order logic" was not around in the 1930s, so it would not have been possible for Goedel to use it. But there was no real "change" from system P to first-order logic at any one moment. At the same time, it is standard in modern writing to use "Goedel's incompleteness theorems" to refer not only to Goedel's original results but also to the strengthening by Rosser and the generalization to arbitrary theories. This is also done, for example, in the SEP article. — Carl (CBM · talk) 20:01, 28 June 2016 (UTC)

When Gödel went to Princeton, he became aware that Church was proving that ℕ, etc. are computationally undecidable using the lambda calculus, which was published the next year. Of course, computational undecidabilty of ℕ has as the immediate consequence that there is a true but unprovable proposition for ℕ. However, Gödel was reluctant to embrace the lambda calculus as definitive for computational decidability. But the next year he embraced Turing machines (shown to have equivalent computational power to the lambda calculus) as definitive for computational decidability and consequently essentially every mathematical theory of practice (including Principia Mathematica) is incomplete.

Carl (talk) 20:35, 28 June 2016 (UTC)

The switch to first-order logic gathered steam in part because of Gödel's response to Wittgenstein's criticism and fear of other lurking paradoxes.

Also, there was the practical problem that philosophers couldn't prove anything much about ℕ because it is very powerful. So they decided to concentrate on first-order logic and turned it into a philosophical dogma.

Carl (talk) 20:45, 28 June 2016 (UTC)

Of course, there is a proposition that is unprovable in the Dedekind/Peano effective deductive system ℕ but true in the up to unique isomorphism only model of the theory. Also, the effective deductive system ℕ is very strong and can prove all known mathematical theorems for the integers. However, Gödel's I'm unprovable. is not a valid proposition of ℕ because propositions are strongly typed.

Carl (talk) 20:11, 28 June 2016 (UTC)

To editor Prof. Carl Hewitt: Fermat's Last Theorem is a "known mathematical theorem for the integers". Do you really know a proof of it in the deductive system ℕ, or, at least, have you a proof that such a proof exists? If yes, where do you have published this? D.Lazard (talk) 09:44, 29 June 2016 (UTC)

To editor D.Lazard:ℕ is very strong. See proof here: Proof of Fermat's Last Theorem in ℕ Carl (talk) 14:42, 29 June 2016 (UTC)

To editor Prof. Carl Hewitt: I know Wiles's article. He never mentions system ℕ, and thus there is not any assertion implying that his proof may be formalized in system ℕ. Thus your assertion that a proof exists in system ℕ is at most a conjecture. D.Lazard (talk) 15:45, 29 June 2016 (UTC)

To editor D.Lazard:It is well known that ℕ formalizes all "ordinary" mathematics. What do you think is special about Wiles's proof? Carl (talk) 16:47, 29 June 2016 (UTC)

To editor Prof. Carl Hewitt: If it is "well known", it should be proved somewhere. Give a source. Give also a source for a definition of "ordinary mathematics" (mathematicians do not know what it is). There is nothing special about Wiles's proof except it use highly sophisticated tools, such as scheme theory and étale cohomology. I know that for defining these concepts, Grothendieck needed an axiom of universes. I do not know wether this axiom is implicitly used, or not, in Wiles's proof, but deciding this is definitively not a trivial task. D.Lazard (talk) 17:55, 29 June 2016 (UTC)

It interesting that ordinary mathematics is discussed matter of factly in the Wikipedia article to which you linked above. Unfortunately, the current Wikipedia article does not discuss strong typing. Carl (talk) 02:22, 30 June 2016 (UTC)

For one reference on the question of what Wiles' proof uses, see "What does it take to prove Fermat's last theorem? Grothendieck and the logic of number theory", C. McLarty, Bulletin of Symbolic Logic 2010. Incidentally, this paper is very readable and also provides some interesting and more-on-topic discussion e.g. of why NBG can't prove the consistency of ZFC.—David Eppstein (talk) 18:11, 29 June 2016 (UTC)

Thanks David for the very interesting and useful reference! The desired property is roughly "Any type construction in the theory ℕ will give the same result whether it is interpreted inside of ℕ or in a larger mathematical system." (Technically, for type τ, τ:Type◅τ▻.)

I particularly like the following quotation:

The point of foundations is not to arbitrarily restrict inquiry but to provide a framework wherein one can legitimately perform those constructions and operations that are mathematically interesting and useful. [Herrlich and Strecker 1973]

Carl (talk) 20:39, 29 June 2016 (UTC)

I know that this discussion is out of scope here. I have started it to make clear that Prof. Carl Hewitt's comments lack of the accuracy that he ask for Wikipedia, and thus that his assertions are not reliable. D.Lazard (talk) 17:55, 29 June 2016 (UTC)

To editor D.Lazard:Please provide specific examples (with diffs) of your alleged examples of my lack of accuracy and reliability.

Of course, the matters discussed here can be highly technical and anyone can make mistakes.

Carl (talk) 19:35, 29 June 2016 (UTC)

The interesting thing is that by a very simple proof, ℕ proves its formal consistency. Of course, this would immediately mean that ℕ is inconsistent had computer scientists not made the axiomatization strongly typed so that I'm unprovable. is not a valid proposition of ℕ. Also, strong typing is needed to rule out other paradoxes such as Berry and Girard.

Carl (talk) 20:19, 28 June 2016 (UTC)

There are extensions, certainly. That's why I said "at least not without additional care". I think we should present the theorems as being about first-order logic, and address the extensions as extensions. --Trovatore (talk) 19:45, 28 June 2016 (UTC)

From the viewpoint of computer science, it was a mistake to retreat into first-order logic and create the first-order dogma that it is the foundation of mathematics. The retreat is causing many problems including distortions of history. Carl (talk) 15:42, 30 June 2016 (UTC)

Preachin' to the choir, buddy. Though I think you may overestimate the "retreat". Set theorists, at least, are well aware of the limitations of first-order logic.

But none of that matters here. The point is that first-order logic is a known, precise quantity side note: Here I mean first-order logic in the sense of Hilbert-style or Gentzen-style deduction or anything of equal strength; I'm not talking about the semantics with nice robustness properties that make it so that lots of different natural ways of formalizing it get you back to the same thing, and with completeness and soundness for first-order logic in the semantic sense. It's like the deductive parallel of Turing computability, in that sense. So it's useful to know its boundaries, and that's what the incompleteness theorems are about, and that should be the main focus of the article. --Trovatore (talk) 18:09, 30 June 2016 (UTC)

First-logic is very well-defined, but so is the theory ℕ, which is actually used by mathematicians in practice. Of course, there is a proposition in the theory ℕ that is unprovable in the theory ℕ but true in the model ℕ. However, this inferentially undecidable proposition is not the one Gödel invented because I'm unprovable. is not a valid proposition of ℕ.

There is also the matter that ℕ proves it's formal consistency, which is hard to square with what Gödel wrote.

Carl (talk) 19:22, 30 June 2016 (UTC)

"I'm unprovable" is a complete mischaracterization of the Goedel sentence. "I'm unprovable" is directly self-referential. The Goedel sentence is not self-referential. It allows coding up some of the properties of self-reference, but it does it without actually using self-reference in any way. It refers only to natural numbers. This is off-topic, of course, and I don't care to discuss it further on this page, but I can't let that go unchallenged. --Trovatore (talk) 19:25, 30 June 2016 (UTC)

As Chaitin pointed out, "I'm unprovable" is a perfectly good mathematical gloss for the Gödel proposition governed by the following: "I'm unprovable" ⇔ ⊬"I'm unprovable"

Carl (talk) 19:31, 30 June 2016 (UTC)

No it isn't. It's mystification. The Goedel sentence is about natural numbers in a perfectly ordinary mathematical way, not about itself in any way whatsoever. Talking about it as though it were about itself leads newcomers to think there's something strange about it, and that something just isn't there. --Trovatore (talk) 19:37, 30 June 2016 (UTC)

Chaitin did not say that there is something "strange" about the Gödel proposition. Instead, his point was that "I'm unprovable" is too trivial to be the basis for proving something as fundamental as incompleteness.

Carl (talk) 20:10, 30 June 2016 (UTC)

There is no "mystification" in the characterization "I'm unprovable" ⇔ ⊬"I'm unprovable"

Also, incompleteness is not just about the natural numbers. Every mathematical theory of practice is incomplete.

Carl (talk) 22:38, 30 June 2016 (UTC)

The Goedel sentence is about the natural numbers, even when the theory whose incompleteness it witnesses is about something else. For example, ZFC is about sets, but nevertheless G_ZFC is about the natural numbers — not about sets, and not about itself. --Trovatore (talk) 23:01, 30 June 2016 (UTC)

For some mathematical theories of practice (for example ℕ), "I'm unprovable" is not a valid proposition even though the theory ℕ is incomplete. First-order ZFC is not really a mathematical theory of practice for many working mathematicians in that they don't feel constrained by its limitations.

In practice, all it takes for incompleteness is that a theory be computationally undecidable. Having axioms for natural numbers is just one way among many to make a theory incomplete.

Carl (talk) 23:54, 30 June 2016 (UTC)

In no case is the Goedel sentence "I'm unprovable". --Trovatore (talk) 00:50, 1 July 2016 (UTC)

As a proposition of first-order logic, in what way is "I'm unprovable" special? It is the case that 1) the proposition is true in the model ℕ and that 2) it is not provable in the first-order axiomatization of the Dedekind/Peano axioms of the natural numbers. But there are lots of propositions that are known to have properties 1) and 2).

Carl (talk) 04:34, 1 July 2016 (UTC)

There is no such proposition of first-order logic as "I'm unprovable". The Goedel sentence does not say "I'm unprovable". It does not refer to itself at all. --Trovatore (talk) 05:45, 1 July 2016 (UTC)

To editor Trovatore:You can argue with Chaitin about the appropriateness of "I'm unprovable" for Gödel's proposition.

In the meantime, can anyone say what is special about the proposition?

Carl (talk) 14:47, 1 July 2016 (UTC)

More to the point, can anyone say what any of this has to do with concrete improvements to be made to our article? Because I don't see much of that and am tempted to archive the lot. —David Eppstein (talk) 16:17, 1 July 2016 (UTC)

You're right, David. Should probably be moved to the Arguments page if we have one. I keep getting sucked in; sorry about that. --Trovatore (talk) 17:35, 1 July 2016 (UTC)

Unfortunately, Wikipedia stands a good chance of falling into the same trap as happened to it with Climate Change and GammerGate :-(

Of course, there are are important properties of the natural numbers (such as Goodstein's theorem, Paris–Harrington theorem, etc.) that cannot be proved in the first-order version of the Dedekind/Peano axioms for natural numbers.

So what is special about "I'm unprovable"?

Carl (talk) 16:31, 1 July 2016 (UTC)

I agree to close this discussion, as it results in a clear consensus of all involved editors against a single editor, who never provides any reliable source for supporting his opinions, even when talking about logical systems that are nowhere cited in Wikipedia (last example, first-order or non-first-order versions of Peano axioms) D.Lazard (talk) 18:13, 1 July 2016 (UTC)

It's very unfortunate that Wikipedia cannot attract more capable editors in this area.

On Wikipedia, differences are extensively discussed between first-order and non first-order versions of the Dedekind/Peano axioms for natural numbers.

Carl (talk) 19:42, 1 July 2016 (UTC)