View source for Talk:Consistency

{{Talk header}}
{{WikiProject banner shell|class=Start|
{{WikiProject Mathematics|importance = mid}}
}}
{{annual readership|scale=log}}

==Gödel's incompleteness theorems==
The info on the page about [[Gödel's incompleteness theorems]] is good, but I think it would be good to define consistency in its own right, and explicate it in more detail here. What I put here right now is pretty weak, though. <small>—Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[Special:Contributions/140.142.182.182|140.142.182.182]] ([[User talk:140.142.182.182|talk]]) {{{2|}}}</small><!-- Template:UnsignedIP -->

==Whole lot of problems==

The list starting "systems proved to be consistent" is simply bad and evidence of confusion.  If it was changed to: systems that are complete wrt. a model (in the sense of maximal complete set) this would work, but then wouldn't fit in the category.  The leading paragraph isn't great either.  I've shifted the page from Consistency to Consistency proof, changed Consistency into a disambig page, and rewritten it.  The previous text was:

-----
In [[mathematics]], a [[formal system]] is said to be '''consistent''' if none of its proven [[theorem]]s can also be disproven within that system. Or, alternatively, if the formal system does not assign both true and false as the semantics of one given statement. These are definitions in negative terms - they speak about the absence of '''inconsistency'''. Formal systems that do admit [[contradiction]]s suffer a semantic collapse, in the sense that deductions in them cannot truly be assigned any significant content, by schemes that apply across the whole system. 

To add:

* Systems proved to be consistent
**[[Presburger arithmetic]]
* Systems not proved consistent
**First order [[Peano arithmetic]] (from a system no stronger than Peano arithmetic)
* Systems that cannot be proved consistent
-----

I'm adding:
* Intro to [[Gödel's incompleteness theorem|incompleteness theorems]]
* Disccussion of relative consistency proofs
* Complete systems
* Self-verifying systems
* Essentially incomplete theories

I plan to add later:
* [[Pi-0-1]] nature of consistency statements and relevance to Hilbert's program (see [[Proof theory]] for an outline)
* Shared potential of essentially incomplete theories
* Discussion of [[provability logic]]

== Alternate senses of Consistency ==

The title of this entry should perhaps be not just "Consistency" but "Classical deductive consistency." See the remarks below regarding "classical consistency." As for "deductive consistency," this article pertains only to deductive logic, not logic broadly construed as a study of inference in general (including, e.g., [[statistical inference]], or [[Charles Sanders Peirce|Peirce's]] and [[Norwood Russell Hanson|Hanson's]] [[Abductive reasoning|abductive inference]]). --[[User:BurkeFT|BurkeFT]] ([[User talk:BurkeFT|talk]]) 21:08, 28 July 2013 (UTC)

The only sense of "Consistancy" given in the article is the lack of explicit contradiction.  This applies only to Classical Logic systems.  (They this doesn't work, for example, for Graham Priest's Paraconsistant logics.)

This sense also fails to work at all in systems without an explict negation. (Since by that definition any such system can't generate a contradiction, since they have no negation).

However, senses that are functionally equivalent to the standard one in systems with negation, and still work in positive propositional logics, have been around for more than 70 years...   Hilbert (about the time he was playing with positive propositional logics) gave a number of definitions that worked for his use.

His "Absolute Consistancy" (for example) just says that if a system can prove anything, it is inconsistant.  If there are Well Formed Formula in a system that the system can <b>not</b> prove then it is consistant.  (For traditional systems, if the system contains a contradiction then it can prove anything. And if there are WFF's in the system that it can't prove then it must not have a contradiction, since a [traditional] system with a contradiction can prove anything.)

As an example, Feys, in his 1965 book "Modal Logic" (published posthumously) established the consistancy of a number of Modal Logic systems by showing that there were WFF's in those systems that those systems could not prove. [Really short slick proofs, by the way].

I would personally find it a better if a more general sense of consistancy were used that applied to more than just classical logics.
(Note that Wikipedia has a [[Paraconsistent logics]] page, so this page doesn't cover a notion that even applies to all the logics on the Wikipedia pages, much less the logics in the literature.)

[[User:Nahaj|Nahaj]] 02:55, 31 October 2006 (UTC)

:Yes, this applies only to classical logic. But most mathematicians and scientists assume classical logic unless one explicitly specifies another kind. Virtually all serious work on mathematics is done in classical logic. Classical logic is what is needed to deal with the real world. Other forms of logic are just games or fantasies. [[User:JRSpriggs|JRSpriggs]] 10:38, 31 October 2006 (UTC)

:: And when one specifies another kind, this definition doeesn't work.  All others being "Games or fantasies" is not a nice thing to say. I have to wonder if you are familiar with the others. But fortunately, there are others on wikipedia that don't agree with you that have put up pages on these other logics.  Too bad this page will have (without a statement to that effect) narrow information that doesn't apply to them. [[User:Nahaj|Nahaj]] 01:44, 1 November 2006 (UTC)

== What is this article about? ==

I proposed [[Talk:Hilbert's problems#Second problem and consistency proof|here]] that Hilbert's second problem should be covered in its own article, separate from this one.  Please discuss it there. [[User:CMummert|CMummert]] 14:36, 5 January 2007 (UTC)
== WikiProject class rating==
This article was automatically assessed because at least one WikiProject had rated the article as start, and the rating on other projects was brought up to start class. [[User:BetacommandBot|BetacommandBot]] 03:52, 10 November 2007 (UTC)

== Bunch of links ==

Just so that everyone knows, Gregbard recently linked hundreds of occurrences of the word "constistent" to this page.  Many of the links had nothing to do with mathematical logic.  I am in the process of removing those links which do not fit this context.  Another avenue might be to expand the scope of this article to give a more notional definition of consistency, applicable outside the domain of mathematical logic.  The current page can then be moved over to [[consistency (logic)]] or the like.  At any rate, it seems fairly clear to me that, unless there is a [[formal system]] close at hand, then linking to an article on consistency in logic flies in the face of [[WP:CONTEXT]].  [[User:Silly rabbit|<span style="color:#c00000;">silly rabbit</span>]] ([[User talk:Silly rabbit|<span style="color:#FF823D;font-family:Monotype Corsiva;cursor:help"><span style="color:#c00000;">talk</span></span>]]) 14:27, 1 May 2008 (UTC)
:Where does your idea come from that the world revolves around mathematical logic, and every other link needs to go? Consistency means something does it not? Is there some other concept that is being meant? NO. It's the same concept rigorously defined. It happens to be a very important concept in philosophy. Furthermore, this article has almost none of the philosophical account of consistency even though it belongs in this article, not separated out. This is why it was moved to "consistency" rather than the narrower "consistency proof". I have done the same thing for many other articles in logic, but I have never had this problem. You seem to believe that only mathematicians need concern themselves here, and anything else should be split out. This is called [[Wikipedia:WikiProject Integration|disintegration]], and it causes there to be two crappy articles, rather than one comprehensive article. The motivation seems to be that the mathematicians simply can't work well with others interdisciplinarily. Please relent from  the narrow view. Be well, [[User:Gregbard|Pontiff Greg Bard]] ([[User talk:Gregbard|talk]]) 19:41, 1 May 2008 (UTC)
::If it is a very important concept in philosophy, why does the [[Stanford Encyclopedia of Philosophy]] not have an entry for it? &nbsp;--[[User talk:Lambiam|Lambiam]] 22:50, 2 May 2008 (UTC)
:::You'll have to ask them. [[The Cambridge Dictionary of Philosophy]] has a full page entry. Hmm, Stanford v. Cambridge. The Stanford website also has plenty of material on consistency in other articles. [[User:Gregbard|Pontiff Greg Bard]] ([[User talk:Gregbard|talk]]) 23:03, 2 May 2008 (UTC)
::::The CDP entry starts with a single brief sentence on the notion of consistency in philosophical logic, and then spends the rest of the article on the (different) notion of consistency in mathematical logic. &nbsp;--[[User talk:Lambiam|Lambiam]] 15:40, 3 May 2008 (UTC)
:To respond to Gregbard's original reply, it is fine if you link occurrences of the bare word [[consistency]], as long as it really will benefit the target reader to have the term linked to a technical article on mathematical logic.  Many of the links '''were not''' used in this sense, and linking them here creates the misleading impression that the word is being employed in a technical, rather than ordinary language, manner.  This has '''absolutely nothing to do with disintegration'''.  I have left all links alone where the context was appropriate.  Perhaps we should bring this issue to the attention of [[Wikipedia:Wikiproject Integration]] so that members of that project can weight in on this dispute.  [[User:Silly rabbit|<span style="color:#c00000;">silly rabbit</span>]] ([[User talk:Silly rabbit|<span style="color:#FF823D;font-family:Monotype Corsiva;cursor:help"><span style="color:#c00000;">talk</span></span>]]) 01:35, 3 May 2008 (UTC)

::I am fine with many of those reverts. We have covered many (but not all) of the strictly technical references to that term. No, this link issue is not about disintegration. However, the article may evolve to cover more ordinary aspects of it. For one thing I presume that people mean what they say on the WP, so it is more reasonable to interpret many of those "ordinary" uses as identical to this topic at least. Then whether or not it is believed that it rises to the level to where it should have a wikilink is a matter of priority. 

::Shocker:I have been making links to all kinds of terms for quite a while now, and I have never had such a strong response. I think any term that is included in the [[template:logic]] at least should be incorporated as wikilinks wherever it is appropriate. There are reasonable cases such as "ordinary" uses of the word [[theorem]]; and more unreasonable cases such as [[relation (mathematics)]] where is would be unreasonable to wikilink every relationship in the wikipedia. I have been using my judgment on those, and I think I have been doing just fine and you are over-reacting about it. We disagree about the priorities, but not the principles in wp:overlink. [[User:Gregbard|Pontiff Greg Bard]] ([[User talk:Gregbard|talk]]) 03:59, 3 May 2008 (UTC)

::: You may notice that I have left intact all links on notional references to "[[logically consistent]]", despite the inappropriateness (in my opinion) of many of these.  I agree with your sentiment that an author should be prepared to ''mean what she says''.  [[User:Silly rabbit|<span style="color:#c00000;">silly rabbit</span>]] ([[User talk:Silly rabbit|<span style="color:#FF823D;font-family:Monotype Corsiva;cursor:help"><span style="color:#c00000;">talk</span></span>]]) 18:38, 3 May 2008 (UTC)

First use of the term 'self-consistent' on [[fictional universe]] links to this page, and this is similar to what's discussed above. Although it was a nice surprise to see an article on consistency in a formal context, most people probably expect the ordinary concept of consistency (which, I suppose, is very similar - e.g., "Bob's story about last night was consistent" means that Bob's story didn't entail a contradiction? Probably..) [[Special:Contributions/71.202.36.15|71.202.36.15]] ([[User talk:71.202.36.15|talk]]) 07:42, 7 July 2011 (UTC)

== Incorrect statement about completeness ==
The statement in item no. 2, "Since these theories are satisfactorily described by the model we obtain from the completeness theorem, such systems are complete" is incorrect. Usually, a theory is called complete if for any <math>p</math>, either <math>p</math> or <math>\neg p</math> can be proved from it. This indeed holds
for Presburger arithmetic, but it certainly does not hold for any theory that cannot talk about its own provability relation. Take Euclidean geometry without parallel axiom, for example: it is not complete.
--[[User:Tillmo|Tillmo]] ([[User talk:Tillmo|talk]]) 12:54, 18 January 2009 (UTC)
:That's far from the only problem with that section. It's a mess, really. I may rewrite it here in a few minutes. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 01:44, 19 January 2009 (UTC)
::Thanks, much better now. However, you have deleted the classification into four or five different types of theories. Do you think that it cannot be corrected? --[[User:Tillmo|Tillmo]] ([[User talk:Tillmo|talk]]) 05:38, 23 January 2009 (UTC)
:::The previous text had some strange claims - such as, any theory that cannot define its own provability predicate is complete. And it had the meaningless phrase "complete with respect to a model". Since I wasn't sure what the goal of the previous "classification" was, and since the text was so flawed, I thought deleting it and starting fresh was better. We can always continue to add additional correct material to the section in the future. Really, I'd like to double check a couple references to see how they handle this classification. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 11:20, 23 January 2009 (UTC)

== Why was this moved? ==

I have read the talk page, and I don't understand why an article that was almost completely about consistency proofs was moved to here, and made to serve as a general article about consistency.  I think it does both the general concept of consistency, and the technical notion of consistency proof, a disservice. &mdash; ''Charles Stewart'' <small>[[User_talk:Chalst|(talk)]]</small> 13:13, 6 May 2009 (UTC)

== Error in Post consistency ==

The article says:

:A set of [[formulas]] <math>\Phi</math> in first-order logic is … said to be '''absolutely consistent''' or '''Post consistent''' if and only if at least one formula of <math>\Phi</math> is not a theorem of <math>\Phi</math>. 

This seems clearly nonsense, because supposing that "φ is a theorem of Φ" (which is not defined in the article) is intended to mean "Φ ⊢ φ", every formula in the set Φ is trivially a theorem of Φ.  I think what was meant here was that Φ is absolutely consistent iff  there is ''any'' formula that is not a theorem of Φ.  In conventional logics this is equivalent to the definition of "simply consistent" given previously, by the [[explosion principle]].  But I thought I would bring the matter up here since I am not actually familiar with the term "absolutely consistent".  If nobody corrects me soon, I will fix the article.  —[[User:Dominus|Mark Dominus]] ([[User talk:Dominus|talk]]) 17:21, 30 January 2011 (UTC)

:In Post's 1921 ''Introduction to a general theory of elementary propositions'', found in van Heijenoort 1967:264ff with introductory comments by van Heijenoort. (Hang in there with me: I'm going to cc the quote in context, then carry it onto the next paragraph):  " . . . completeness in the sense of Post: a system is complete in that sense if every well-formed formula becomes provable once we adjoin to the axioms any well-formed formula that is not provable. What Post himself calls a 'complete' system is one in which every truth function can be written in terms of the primitive truth functions, and he shows that the calculus under study, in which the connectives are ~ and V, is complete in that sense. A consistency proof of the calculus is given. A new definition of consistency, sometimes called consitency in the sense of Post, is presented; a calculus that contains propositional variables is consistent in that sense if no well-formed formula consisting of a single propositional variable is provable. Consistency in that sense, too, is established." (p. 264). 

:In Nagel and Newman 1958 ''Goedel's Proof'' there's an entire chapter on "Absolute Proofs of Consistency" (pp. 26-36) (if I understand this correctly, they are eschewing model theory completely). They follow up with another chapter "An Example of a Successful Absolute Proof of Consistency" (pp. 45-56). In this example, on p. 54, there's an important footnote. They flesh out the notion of "absolute consistency" with a definition of tautologous that is "absolute": "The property of being a tautology has been defined in notions of truth and falsity. Yet these notions obviously involve a reference to something ''outside'' the formal calculus. Therefore, the procedure mentioned in the text in effect offers an ''interpretation'' of the calculus, by supplying a model for the system. This being so, the authors have not done what they promised, namely, to define a property of formulas in term so fpurely structural features of the formulas themselves" (p. 109)It turns out that this construction/treatment is one and the same that is found in the very same Post 1921. 

:Hope this helps. Bill [[User:Wvbailey|Wvbailey]] ([[User talk:Wvbailey|talk]]) 20:43, 30 January 2011 (UTC)

== Dubious statement about completeness ==

The article contains the following claim:
:"If these semantic and syntactic definitions [of completeness] are equivalent for a particular logic, the logic is '''[[Completeness#Logical completeness|complete]]'''.<sup>{{plainlink|http://en.wikipedia.org/wiki/Consistency#cite_note-1|[2]}}</sup>"
There are different notions of logical completeness; the footnote to Tarski's definition shows that here syntactic completeness is intended.

Now consider the following deductive system. Its formulas are formed from two variables ''A'' and ''B'', and the unary operator ¬. It has one axiom, ''A'', and one inference schema, "from Φ, infer ¬¬Φ". So the theory of the system consists of ''A'', ¬¬''A'', ¬¬¬¬''A'', and so on.

Is this theory semantically consistent? Under an [[interpretation (logic)|interpretation]] that assigns true to ''A'', with the standard interpretation of the logical constant ¬, all formulas of the theory are true.

Is this theory syntactically consistent? Clearly, there is no formula Φ such that both Φ and ¬Φ are members of the theory.

Is this theory complete? No, since neither ''B'' nor ¬''B'' is in the theory.
&nbsp;--[[User talk:Lambiam|Lambiam]] 01:50, 29 May 2012 (UTC)

:The text is correct, but the footnote shouldn't be there. The difference is that the footnote is talking about completeness of a theory, while the text is talking about completeness of a logic (i.e. that the derivable sentences are exactly the valid ones). The logic you describe is indeed complete, but even in first-order logic which is complete there are many theories that are not complete. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 02:36, 29 May 2012 (UTC)
::If the derivable sentences are exactly the valid ones, doesn't that mean the logic is <u>sound</u> and complete? The article does not define the notion of consistency for a logic, but only for a theory. To apply it to a logic, do we take the theory consisting of the theorems of the logic? But then, it seems that (as defined in the article) semantic consistency implies syntactic consistency. For suppose we have a logic that is semantically but not syntactically consistent. Let ''P'' be some formula such that both ''P'' and its negation are provable. So both are theorems of that logic. Because it is semantically consistent, then both ''P'' and its negation are true in some model. Contradiction. &nbsp;--[[User talk:Lambiam|Lambiam]] 17:48, 29 May 2012 (UTC)
:::Yes, I think that soundness is being taken for granted there, it could be made explicit. The usual statement of completeness for first-order logic quantifies over all theories, not just over the theory of derivable statements. In a particular phrasing it says that an arbitrary first-order theory is semantically inconsistent if and only if it is syntactically inconsistent (which is the same as saying that a theory is semantically consistent if and only if it is syntactically consistent). &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 18:12, 29 May 2012 (UTC)
::::Based on the above discussion, perhaps we should make the statement in the article clearer. Is the following improvement of the first sentence of the second paragraph correct? 
:::::"If these semantic and syntactic definitions are equivalent for '''any theory formulated using''' a particular deductive logic, the logic is '''called''' complete." 
::::If no one objects to this improvement, I'll add it to the article tomorrow. [[User:Natsirtguy|Natsirtguy]] ([[User talk:Natsirtguy|talk]]) 00:27, 13 June 2014 (UTC)

what is soil  <span style="font-size: smaller;" class="autosigned">— Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[Special:Contributions/220.227.97.146|220.227.97.146]] ([[User talk:220.227.97.146|talk]]) 04:38, 19 September 2012 (UTC)</span><!-- Template:Unsigned IP --> <!--Autosigned by SineBot-->

== Coatrack, etc. ==

Why do we need the detailed paragraph about completeness in the lead? It seems to violate [[WP:LEAD]], because the history of various completeness results/proofs is not the topic of this article. [[User:Tijfo098|Tijfo098]] ([[User talk:Tijfo098|talk]]) 09:27, 8 November 2012 (UTC)

I would have expected instead something like [[Russell's paradox]] to be mentioned because it's classic example of inconsistency. [[User:Tijfo098|Tijfo098]] ([[User talk:Tijfo098|talk]]) 09:29, 8 November 2012 (UTC)

Also most of the section on FOL initially titled "Formulas" is just the [[completeness theorem]] for FOL ([[sequent calculus]]) using Henkin's proof method instead of Gödel's cf. [http://books.google.com/books?id=rAy-NliGEPMC&pg=PA75]. [[User:Tijfo098|Tijfo098]] ([[User talk:Tijfo098|talk]]) 09:37, 8 November 2012 (UTC)

== Stepien-family theorem ==
I'm deleting the following for the same reason Travatore deleted it from[[Gödel's incompleteness theorems]]:

:However, on the other hand, Teodor Stepien and Lukasz Stepien delivered a talk at the Conference "2009 European Summer Meeting of Association for Symbolic Logic, Logic Colloquium'09" (July 31 - August 5, 2009, Sofia, Bulgaria). In this talk, entitled "On consistency of Peano's Arithmetic System", they presented a sketch of the proof of the consistency of Peano's Arithmetic System (of course, the full proof was constructed by Teodor Stepien and Lukasz Stepien before the Conference "Logic Colloquium 2009"). There in this proof are used only the axioms of first-order logic and the axioms of Peano's Arithmetic System. Thus, this proof is absolutely elementary. Hence, from the construction of this proof, it follows that Gödel's Second Incompleteness Theorem is ''invalid''. <ref>http://ultra.ap.krakow.pl/~lstepien/</ref> The asbtract of this talk was published in "The Bulletin of Symbolic Logic": <ref>T. J. Stepien and L. T. Stepien, ''Bull. Symb. Logic'' '''16''', 132 (2010).</ref>

This is just the professional equivalent of spamming. Bill [[User:Wvbailey|Wvbailey]] ([[User talk:Wvbailey|talk]]) 22:13, 23 November 2012 (UTC)

{{reflist-talk}}

== Consonancy ==

Why does consonancy redirect here? Two alternative places it would be better redirected to are Consonance and dissonance and Literary consonance. --[[Special:Contributions/184.23.18.191|184.23.18.191]] ([[User talk:184.23.18.191|talk]]) 17:38, 10 February 2016 (UTC)

== Semantic Definition ==

In the opening sentences (emphasis mine):

:The semantic definition states that a theory is consistent if and only if it has a model, i.e., there exists an interpretation under which ''all'' formulas in the theory are true.

Surely that can't be right. All formulas would include negation pairs. Perhaps "all tautologies" was intended?

--[[User:Smithph|phil]] ([[User talk:Smithph|talk]]) 06:34, 28 February 2017 (UTC)

:A theory that includes negation pairs isn't consistent; in general a "theory" is just some set of formulas in a particular language. A consistent theory cannot contain ''all' the formulas in a language. &mdash;&nbsp;Carl <small>([[User:CBM|CBM]]&nbsp;·&nbsp;[[User talk:CBM|talk]])</small> 12:33, 28 February 2017 (UTC)

== Internal logic ==

Internal logic redirects to this article. 

However, internal logic as an abstract concept refers to a whole range of things we experience in the real world such as the laws that govern everyday life: don't cross that light at red or the cop will give you a ticket! -- or the most basic instructions of a computer chip: Windows ''will'' crash because only an omnipotent being can completely understand all the possible outcomes in a set of instructions in chip architecture -- or interpersonal relationships: your life partner ''will be'' seriously ticked off if you forget to buy the cat's favourite food ''yet again'' when shopping. That plus astrophysics.

Then there is internal logic in fiction, such as Asimov's Three Laws, that a robot (1) may not injure a human... (2) must obey the orders given it by human beings except where such orders would conflict with the First Law (3) must protect its own existence as long as such protection does not conflict with the First or Second Laws. Essentially, all fiction from ''Gilgamesh'' to ''Groundhog Day'' follows some kind of internal logic. Yet Wikipedia doesn't seem to cover this concept other than in maths. As I'm a gnome, I don't dare touch this other than on a talk page. == [[User:Peter NYC|Peter NYC]] ([[User talk:Peter NYC|talk]]) 09:51, 28 March 2021 (UTC)

:The examples you give are everyday experience (except for Asimov's laws, which I'd subsume under behavioral policy in a wide sense). I don't have an idea what could be said about that in an article or where to find citations about that; but if you do, just be bold and start writing. 
:However, I have a strong feeling that your issue shouldn't be mixed into the mathematical stuff here. Instead, I'd suggest to turn [[Internal logic]] from a redirect into a proper article (started by you), which could have a hat note (<nowiki>{{distinguish}}</nowiki> or similar) saying that the mathematical notion is dealt with at [[Consistency]]. - [[User:Jochen Burghardt|Jochen Burghardt]] ([[User talk:Jochen Burghardt|talk]]) 10:32, 28 March 2021 (UTC)
::As I wrote, I'm a gnome, simply (and not humbly, 'cause gnomes don't ''have'' to be humble) pointing out that a philosophical, sociological and literary concept redirects to a, whatchamacallit, ''hard science''. == [[User:Peter NYC|Peter NYC]] ([[User talk:Peter NYC|talk]]) 11:56, 28 March 2021 (UTC)