Talk:Double negative elimination

issue

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

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)