Talk:Gödel's incompleteness theorems

Please place discussions on the underlying mathematical issues on the Arguments page. Non-editorial comments on this talk page may be removed by other editors.

Disquotationally??

In the Note, it is asserted that the use "here" of "true" is disquotational. First, the link fails to provide any clear insight about wtf the editor is attempting to say. Second, my Shorter Oxford English dictionary has no entry for that word. Speak English, please! Third, the link is to the Redundancy Theory and no longer to Disquotationalism. Fourth, what does "here" mean? Does it mean the editor will on a minute by minute basis check that any future change in this article will comply with his (its gotta be a guy, I think) demands on how "true" must be used in all cases? Or does it mean "in this section"? paragraph? moment? Fifth, How does this "note" contribute to this article? It doesn't as far as I can see. Sixth, it would be nice for the various types of "truth" to be distinguished...I don't think its possible to have only one kind of "true" when discussing a theory of true statements - am I wrong? (There is true, meta-true, meta-meta-true, etc.). My general comment (and based on the arguments page, this is going to be lost on the fan-boys here) is that if a topic is presented in needlessly obfuscatory language, then most of its utility is lost. And this article is clearly needlessly obfuscatory. I suggest the editors, prior to starting their editing session, look in the mirror and repeat "Oh, what a clever, intelligent, witty boy I am!" until its out of their system. Then try to write clearly for the audience that Wikipedia is intended for. Like, by always distinguishing statements (propositions) IN a system from statements ABOUT a system and clearly indicating when a statement is one, the other, or both. Oh, what a smart boy I am!173.189.79.42 (talk) 22:31, 17 May 2015 (UTC)

Just taking one point: You say "I don't think its possible to have only one kind of "true" when discussing a theory of true statements - am I wrong? (There is true, meta-true, meta-meta-true, etc.)".

Answer: Yes, you are wrong. Hope this helps. --Trovatore (talk) 18:09, 18 May 2015 (UTC)

Severely underreferenced

Unfreakingbelievable! Such a fundemental concept with footnotes close to none. Am I supposed to believe every utterance of an anonymous Wikipedian At Large? - üser:Altenmann >t 15:16, 31 August 2015 (UTC)

I see what happened here. You came to this article thinking that sourcing is always done with footnotes. That is not so. This article uses Harvard-style parenthetical referencing. Look for parentheses with a name and a date, like this: (Goodauthor, 2027). --Trovatore (talk) 19:02, 31 August 2015 (UTC)

Don't patronize me and show me Harvard, e.g., in section "Background". If are you telling me that "(simply)" is a Harvard-style ref, then it is malformed (year missing). - üser:Altenmann >t 03:05, 1 September 2015 (UTC)

OK, look, you made a mistake in not noticing it was Harvard. Admit that and quit asking for "footnotes" or complaining about "patronizing".

That said, looking over it, there aren't very many Harvard refs either, and that probably does need to change. But with more Harvard refs.

Some of them are probably malformed, but they're there. Search for "(Hellman 1981, p. 451–468)" for example. --Trovatore (talk) 03:33, 1 September 2015 (UTC)

My mistake was my insufficient English language discrimination. I meant no say "citations close to none". Admit that the article is severely underreferenced and quit nitpicking on technicalities. - üser:Altenmann >t 15:12, 1 September 2015 (UTC)

A significant problem, here, seems to be that the references appear manually at the end of the article, disconnected from their citations, so I'm thinking a solution to this might be to, for each manual citation, move the matching manual reference to the manual citation's location, formatting its contained information as an equivalent "ref" tag, then suffix a "ref-list" so as to auto-generate the references (hope I've explained that clearly enough :-). It'll be a big change. but should (IMHO :-) greatly improve the article. Before I try to make such a change, however: what does everybody think?

Rpot2 (talk) 07:49, 10 March 2016 (UTC)

In any case, there is no lack of experts who have edited this article, or who have this article on their watchlist. I see Trovatore and David Eppstein in the recent edit history, who both have PhDs in mathematics; Wvbailey has done a lot of reading on the subject and knows quite a bit; and if you count Carl Hewitt through his sockpuppets that is another. I have some experience with the incompleteness theorems, as well. As always, my advice for those who want to see more sources is to add them – just adding templates will not lead to the outcome you are looking for, based on experience with many articles on Wikipedia. — Carl (CBM · talk) 02:06, 2 September 2015 (UTC)

One correction: I have a BS in mathematics but my PhD is in CS. —David Eppstein (talk) 04:14, 2 September 2015 (UTC)

May be you have PhD but it seems you cannot read plain English. The template says "This article needs attention from an expert in mathematics". And it is lack of attention to the state of the article I am complaining about. Please don't delete the template until the explained issue is resolved, i.e, until experts in maths take seriously the wikipedia rule about references. CBM: your advice to add them myself is ridiculous. How in freaking hell I can add them if I am not familiar with the subject? This is not a pokemon or pornstar article, it is MATHEMATICS, for God's sake! So, either you start adding references, or I start deleting original exegesis. - üser:Altenmann >t 14:56, 2 September 2015 (UTC)

You should read Wikipedia:Scientific citation guidelines as well, if you are interested in the Wikipedia policies that apply. Remember that there is no rule that requires a citation for each sentence. There are some unreferened sections, which do need some improvement, but remember WP:DEADLINE. I also want to warn you about the three revert rule, which you are in danger of violating. — Carl (CBM · talk) 16:49, 2 September 2015 (UTC)

I have no problems with uncontroversial knowledge. Fact is, I have issues with the text of the article. I am not going to read 15 books listed at the bottom to verify the article. I need citations in situ. - üser:Altenmann >t 02:37, 3 September 2015 (UTC)

In regard the "expert" tag; there is a potential reason for inclusion, as an expert in whatever field Hewitt is expert in might have a different take on the article. We do not have agreement as to whether the theorems are in that field, so I'm not sure consensus could be reached for inclusion. — Arthur Rubin (talk) 18:22, 2 September 2015 (UTC)

remove "background" section or move it to later in article if found to be meaningful...

that first "background" section is all over the place/not sure coherent in whatever it's trying to say/but certain doesn't fit the role of "background" for this topic...article would flow far better if just went right into the following "first incompleteness theorem" section....and whatever is in that 'background' section could be moved to later on, if it's deemed relevant or coherent... 68.48.241.158 (talk) 22:22, 29 February 2016 (UTC)

"meaning of first incompleteness theorem" section would better fit as "background" imo....as it's more general in nature....that first section is trying to get too technical too fast or something...it just feels very, very odd as the first thing you start reading for this topic in article proper...68.48.241.158 (talk) 22:33, 29 February 2016 (UTC)

The background section introduces the terminology that is required for the theorem. On the other hand, the section on "meaning" shouldn't come before the section that actually states the theorem whose meaning is being discussed. — Carl (CBM · talk) 21:27, 10 March 2016 (UTC)

"formal axiomatic system"/"formal system" vs "formal theory"

terminology is inconsistent in the article and jumps back and forth abruptly....most accurately, I think "formal axiomatic system" should be used but could be shortened in places to "formal system"....I've never really heard "formal theory" used in place of the former in this context...but there are many times throughout where "system" and "theory" are used to mean the same thing, and this is very confusing, particularly to someone new to the topic...Hilbert, Russell, Gödel, etc would refer to Principia Mathematica as a formal axiomatic system (or formal system) for arithmetic, I think, and not as a formal theory for arithmetic...(or even more confusing just "theory for arithmetic"...which pops up in this article...).. 68.48.241.158 (talk) 14:39, 14 March 2016 (UTC)

"Formal system" everywhere is fine with me, although "theory" would be the more common word in contemporary logic. They are essentially synonymous. — Carl (CBM · talk) 17:01, 14 March 2016 (UTC)

I would prefer "theory" everywhere. "System" is kind of vague; "theory" is the precise technical term. It does have the disadvantage that its meaning in this context is quite different from its ordinary-English meaning, but that happens a lot in math. --Trovatore (talk) 18:29, 14 March 2016 (UTC)

idk as long as consistent throughout though to avoid confusion..think 'theory' causes more problems in the context of this topic though...as there's usage of 'deductive system' and 'axiomatic system' and would be odd to say 'deductive theory' or 'axiomatic theory'.... 68.48.241.158 (talk) 19:18, 14 March 2016 (UTC)

It's a difference in emphasis. Roughly, a deductive system is axioms plus rules, whereas a theory is axioms plus consequences. --Trovatore (talk) 19:49, 14 March 2016 (UTC)

first sentence..

"Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic." this is a tricky topic in general that requires very precise wording to be accurate...anyway, think "establish" should be replaced with "demonstrate" as establish kind of suggests Gödel invented the truths of the theorems as opposed to discovered/demonstrated them (ie their truths are independent of Gödel discovering them).. think "all but most trivial" is confusing/not necessary...think reference to a proof of the completeness and consistency of a system capable of addition/subtraction but not multiplication/division...but arithmetic in the context of this topic has to include (Hilbert's program)addition/subtraction/multiplication/division...so the trivial system referenced isn't capable of arithmetic at all but something else..and not sure this 'trivial system' is referenced/explained later in piece so why go off on the tangent at all..particularly in the very first sentence..and since the incompleteness theorems don't address this kind of 'trivial' system anyway?? how's this: Gödel's incompleteness theorems are two proofs in mathematical logic that demonstrate inherent limitations of any formal axiomatic system capable of (expressing) arithmetic. ...don't like the 'doing' either...just sounds funny...maybe 'expressing...' and did away with the repetition of 'theorems' right of the bat.. 68.48.241.158 (talk) 16:49, 14 March 2016 (UTC)

Try just making the change. I will not revert blindly, but I will try to improve on edits (can't speak for others, but hopefully they will do the same). I don't like calling the theorems "proofs". I edited the first sentence with something like what you suggested. — Carl (CBM · talk) 17:09, 14 March 2016 (UTC)

No serious objections to the changes so far (currently, it says Gödel's incompleteness theorems are two theorems of mathematical logic that demonstrate inherent limitations of any formal axiomatic system capable of expressing basic arithmetic). I think the "all but the most trivial" part was meant to emphasize that you don't even need all that much of arithmetic (Robinson arithmetic suffices), but we probably don't need to cut things that fine in the opening sentence anyway.

I understand 68's objection to saying "...theorems are two theorems..." but I don't think we have a lot of choice in this case; see Fowler on elegant variation here. When there's a single word that's the most precise, it does not aid understanding to avoid it simply in the name of avoiding repetition. I suppose it wouldn't be totally implausible to replace the second "theorems" by "results", but on the whole I would vote no. --Trovatore (talk) 20:49, 14 March 2016 (UTC)

Ah, I actually do have one issue to raise. There was a change from "capable of doing arithmetic" to "capable of expressing arithmetic". But expressive power lies in the language (and intended interpretation), not the theory or deductive system. I do kind of see the point; it's not clear that "doing" really captures the idea we want. Any thoughts on a better word? --Trovatore (talk) 23:16, 14 March 2016 (UTC)

yeah, if the system is symbolically or typographically complex enough to 'represent' or 'express' or 'do' or 'mirror' whole number arithmetic than it is subject to the theorems...don't know exactly how to best state that in a brief introduction...one solution is to drop it and just state "system capable of arithmetic" or "system capable of whole number arithmetic." 68.48.241.158 (talk) 00:40, 15 March 2016 (UTC)

The use of "arithmetic" to mean the theory of the natural numbers -- rather than just "arithmetic" in the normal sense of addition and multiplication facts -- is confusing for a first sentence in a general article whose readers are not likely to read the term as jargon. I have changed it to "basic properties of the natural numbers" which is less likely to be misinterpreted. — Carl (CBM · talk) 13:53, 15 March 2016 (UTC)

think 'basic properties of natural numbers' is too vague and probably inaccurate...as some systems are capable of expressing basic properties of the natural numbers (addition/subtraction) and have been proven complete and consistent...these theorems specifically relate to systems capable of natural number arithmetic in the classic sense (add/sub/mult/div)...this was crucial to Hilbert's program as every relationship between the natural numbers can in theory be built up from these basic operations....so think the word arithmetic (or what the word technically means in the context of these theorems) must be used somehow....perhaps something like "capable of expressing the arithmetic of the natural numbers."68.48.241.158 (talk) 14:57, 15 March 2016 (UTC)

in that second paragraph the phrase, " is capable of proving all truths about the relations of the natural numbers (arithmetic). " is excellent imo with the parenthetical (arithmetic) as this is exactly what arithmetic meant in the context of these theorems...ie the relations of the natural numbers...to the big brains working on this stuff back then arithmetic technically meant the study of the relationships between the natural numbers...and they understood that the tools needed to study any conceivable relationship were the 4 basic operations... 68.48.241.158 (talk) 15:28, 15 March 2016 (UTC)

The four operations are not enough, though. For the second theorem, a significant amount of strength is required for the theory to prove the Hilbert-Bernays condition, and of course this strength goes well beyond the axioms of $PA^{-}$ that determine the basic operations. Separately, comments about the "big brains" in the past won't help us improve the article. — Carl (CBM · talk) 10:35, 18 March 2016 (UTC)

In particular Robinson arithmetic Q proves every true quantifier-free sentence in the language of PA, including every true fact about the arithmetical operations on standard numbers, but Q is not strong enough for the second incompleteness theorem. The article arithmetic seems to be written in a way that will not be very helpful for clarifying this. Because of most people's association of the term with the four basic operations only, I think it is more likely to confuse a naive reader than to clarify matters, in the first sentence. — Carl (CBM · talk) 10:40, 18 March 2016 (UTC)

"capable of expressing sufficient facts about the natural numbers" this may not be wrong but it's so vague that it's sort of meaningless so think not how we'd ultimately want to leave the fist sentence..all that is actually explicitly necessary of a formal system to qualify is addition and multiplication as their inverses (subtraction/division) are derivable from these..B Meltzer in the Dover preface writes, "any formal logical system that disposes of sufficient means to compass the addition and multiplication of positive integers and zero is subject to this limitation."

the second incompleteness theorem is inseperable from the first (naming it 'second' is sort of artificial..Gödel certainly never did) and it relates to the exact same systems as the first...so not sure what you're getting at....

so that last clause might be best if just got quite specific with something like ..system capable of compassing the addition and multiplication of the natural numbers

a to do type thing too is to better explain the requirements of the system in the article proper/explain what arithmetic meant in the context of this topic...68.48.241.158 (talk) 13:31, 18 March 2016 (UTC)

The first incompleteness theorem (rather, its proof) applies to every true theory of arithmetic - no matter how weak - along with theories that may have false axioms but are able to represent all the computable functions. The second incompleteness theorem, in its explicit hypotheses, requires the system to be able to prove various facts about the Provability predicate (these are the so-called Hilbert-Bernays conditions). So, for example, the first incompleteness theorem applies to Robinson's Q, and shows that Q does not prove the Gödel sentence of Q, but Robinson's Q does not satisfy the hypotheses of the second incompleteness theorem, and the second incompleteness theorem cannot be used to show that Q does not prove Con(Q). So it is not the case that the two theorems apply to exactly the same theories.

Now, Q is indeed able to prove every true sentence of the form $n + m =k$ and every true sentence of the form $n * m = k$, but it does not satisfy the hypotheses of the second incompleteness theorem, so I am not especially content with a claim that "capable of compassing the addition and multiplication of the natural numbers" is sufficient for the two theorems. I think it is better to just say "enough facts" or "is sufficiently strong" than to try to detail the Hilbert-Bernays conditions in the first sentence of the article.

Finally, please see the section of this article "Translations, during his lifetime, of Gödel's paper into English" for sourced commentary on the quality of the Meltzer translation. We should cite it, but we should not use it for many serious purposes when there are much better sources available. — Carl (CBM · talk) 13:35, 18 March 2016 (UTC)

perhaps, but the statement I quote is uncontroversial and well put by him...what you're speaking of is beyond me technically but my main concern is vague language within an encyclopedia...like vague technical jargon is a big danger in an article like this...like above when you say "every true theory of arithmetic -no matter how weak..." this is vague and confusing as exactly how weak/strong the system must be is easily and specifically defined...and that Presburger system is too weak for these theorems to apply.. (this is just an example of how vagueness (especially masked in technical jargon) potentially misleads...) 68.48.241.158 (talk) 14:13, 18 March 2016 (UTC)

or to clarify..I've never seen or read anything anywhere to suggest there's any controversy about what kind of systems are subject to the theorems or that defining such is of any difficulty...you seem to be suggesting otherwise in technical jargon that is beyond me personally..so others would have to weigh in...68.48.241.158 (talk) 14:25, 18 March 2016 (UTC)

I think the first sentence will need to be somewhat vague - the one you proposed was at least as vague, but I thought it gave an incorrect impression.

Avoiding any jargon: the first incompleteness theorem applies to Robinson's Q, but the second incompleteness theorem does not, because Q is strong enough to satisfy the hypotheses of the first theorem but not strong enough to satisfy the hypotheses of the second theorem. — Carl (CBM · talk) 15:33, 18 March 2016 (UTC)

this is getting off topic and probably better for the arguments page that was created for this topic but..are you absolutely certain of this?? my clear understanding is if a system is incomplete in this realm then it is by definition subject to what the 'second theorem' states about consistency because the second theorem is entirely demonstrated via what is demonstrated in the 'first theorem.' so if this Q indeed falls prey to the 'first theorem' it will automatically fall prey to the 'second theorem,' no matter what... 68.48.241.158 (talk) 16:21, 18 March 2016 (UTC)

but back to first sentence..perhaps best to go full vague in a sense then, like: ...demonstrate the inherent limitations of any formal axiomatic system of a certain expressive power. and just get out of the arithmetic/number/facts/etc etc business altogether in that first sentence as this will all be explained later on (beginning in the second paragraph of the intro)....68.48.241.158 (talk) 16:37, 18 March 2016 (UTC)

I think that "certain expressive power" is fine, and I made that change. For Q, the first thing I recommend is getting a copy of Peter Smith's "An introduction to Gödel's theorems". Then see Chapter 26. Now, if you won't take my word for anything, I don't know why you would take anyone else's, but you could see e.g. [1] or [2] also. The specific hypotheses needed for both the canonical proofs of the first and second incompleteness theorems (with Rosser's method incorporated) have been thoroughly studied, and the second requires more than the first. Some low-level books either never say clearly what is needed, or just assume the stronger hypotheses throughout. — Carl (CBM · talk) 17:53, 18 March 2016 (UTC)

that's interesting..question though: is Q a kind of "weakened system" for arithmetic not unlike Presburger Arithmetic (though less weakened) that just happens to be susceptible to the first incompleteness theorem..and would therefore not be considered sufficient to potentially satisfy what is known as Hilbert's Program? (ie not fully capable of what was meant by "arithmetic" and therefore of "trivial" interest to Hilbert's program..?)..and not the kind of system addressed by KG...? 68.48.241.158 (talk) 18:27, 18 March 2016 (UTC)

Sections

just thinking the article has a bit too much of the everything but the kitchen sink feel to it (too much clutter)... SECTIONS: PROOF VIA BERRY'S PARADOX: probably delete or briefly mention in liar paradox section...?? FORMALIZED PROOFS: delete or expand (but probably delete) what does this actually mean?? or actually add to the article?? probably vanity thing for the guy... UNDECIDABLE STATEMENTS PROVABLE IN LARGER SYSTEMS: planted right in middle of the section...seems distracting from actual topic and largely tangential.. EXAMPLES UNDECIDABLE STATEMENTS: same thoughts more or less as previous (at least made more aimed specifically at topic at hand in some way).. PARACONSISTIC LOGIC: idk seems way tangential to merit own section ROLE OF SELF-REFERENCE: I think clearly delete or briefly mention in other section... PROOF SKETCH SECOND THEOREM: seems thrown in at a random place..and not sure qualifies as a proof sketch or adds anything not already discussed..??

obviously these things could be worked on slowly and carefully...but if get rid of some of the clutter would make easier to work on accuracy of what should definitely be included in the article...68.48.241.158 (talk) 20:22, 17 March 2016 (UTC)

The article should be comprehensive, within reasonable space limits. I don't favor removing large parts of the article. Also, it might help discussion if you avoid using the word "accuracy" as if the article is patently inaccurate. Everyone has a preferred way of saying things, but the overall the article is quite accurate as it stands. — Carl (CBM · talk) 10:31, 18 March 2016 (UTC)

the article isn't largely inaccurate but there are a lot of assertions throughout that are vague to the point of being unhelpful/potentially misleading imo..but it would take much time to tighten them all up...not an overnight thing...but a couple sections should be dropped as they stand now, like FORMALIZED PROOFS...simply not worthy of own section within such an important topic...simply vanity reference for the professors...like if every professor who did something to do with Darwin's theory of natural selection created their own three sentence section in that article.....(comprehensive good though...some sections should be expanded..like the HISTORY section and others).. 68.48.241.158 (talk) 12:51, 18 March 2016 (UTC)

I don't see mention of formalized proofs as vanity references - in fact I suspect I added at least a majority of those references, and I am not one of the authors. The point of that text is that, even if someone has doubts about the informal proofs, there are also two fully formalized proofs, which may provide some reassurance to skeptics. This is particularly relevant for the second incompleteness theorem . Moreover, the number of nontrivial theorems for which a fully formalized proof has been produced is very small - I can think of only the prime number theorem, the Kepler conjecture/Hales' theorem, and the incompleteness theorems off the top of my head, and I try to pay attention to such things when they are announced. So the fact that there is a fully formalized proof of the incompleteness theorem also worth noting because it can only be said of a small number of results. — Carl (CBM · talk) 13:18, 18 March 2016 (UTC)

okay perhaps what you just explained above should be explained in the section to make it more worthy of a stand alone section..again, none of this has to be done overnight....68.48.241.158 (talk) 13:38, 18 March 2016 (UTC)

The trouble, of course, is that when we want to add (correct) explanation, someone else will come along and complain that the explanation is not directly quoted from a cited source. So, to limit the amount of commentary that we include in the article, sometimes it is better to say less than we know. If we do find a good source discussing the formalized proofs, then adding some additional, sourced commentary would be great. — Carl (CBM · talk) 13:41, 18 March 2016 (UTC)

"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 [3] 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)

Controversy about Gödel's incompleteness results in Computer Science

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)

References

Discussion

What about theorem proofs, from page you can see they have been also formally verified. Baking Soda (talk) 16:38, 20 April 2016 (UTC)

• This is already adequately addressed in the section "Limitations of Gödel's theorems". Do you have any specific issues with that section? —Ruud 17:05, 20 April 2016 (UTC)