Talk:Double negative elimination
This redirect does not require a rating on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | |||||||||||||||||||||||
|
The contents of the Double negative elimination page were merged into Double negation on 27 February 2015 and it now redirects there. For the contribution history and old versions of the merged article please see its history. |
This article was nominated for merging with Double negation on March 2012. The result of the discussion was Merge. |
issue
[edit]The article states:
The rule of double negative introduction states the converse, that double negatives can be added without changing the meaning of a proposition.
This seems to be wrong. If we have only double negative introduction but not double negative elimination, then adding a double negative weakens the proposition. To me, this seems like changing the meaning.Punainen Nörtti 17:50, 18 May 2007 (UTC)
- Yes, I think the proper wording would be "truth value", not "meaning". Otherwise double negative introduction would imply double negative elimination by equating the two propositions. — brighterorange (talk) 18:44, 18 May 2007 (UTC)
- Actually, I think that's not right either, since (A v ~A) is not provable in intuitionistic ("has no truth value"?) whereas its double negation does. I think there is a more global confusion in the article about whether A = ~~A or whether A ==> ~~A and/or ~~A ==> A as theorems of the logic. The latter seems to be the only sensible way to phrase it if we're going to talk about intuitionistic logic too. — brighterorange (talk) 18:46, 18 May 2007 (UTC)
Merge proposal
[edit]I think the two articles conflate three distinct concepts—double negation, double negation elimination, and double negation introduction—so I would be in favor of merging Double negation into Double negative elimination and working to fix the confusion. There is a universally accepted meaning for the term "double negation", as referring to a certain kind of unary operation on propositions (although the precise character of this operation is not universally agreed upon), in the same way that "conjunction" refers to a certain kind of binary operation on propositions. I take it from the Double negation article that in some historical texts, the "principle of double-negation" refers to an equivalence between a proposition (A) and its double negation (~~A). However, as discussed in the comments above, because this principle fails in some situations, there is a well-established convention in proof theory of distinguishing double negation elimination from double negation introduction. (Similarly, "the law of conjunction" is sometimes used to refer to the inference either [from the truth of a conjunction to the truth of the two conjuncts], or [vice versa], while in proof theory this law is more precisely decomposed into "conjunction elimination" and "conjunction introduction".) I think this is actually explained okay in the Double negative elimination article beginning at the line "Formally, [...]", but I think the material before that is incorrectly using the terminology from proof theory. Noamz (talk) 20:37, 20 February 2012 (UTC)