Talk:Double negation

Merge proposal

The following discussion is closed. Please do not modify it. Subsequent comments should be made in a new section. A summary of the conclusions reached follows.

The result of this discussion was to merge Haruth (talk) 08:26, 27 February 2015 (UTC)

---

• I agree, these two are in fact very similar and should be merged. JMCF125 (discussion • contribs) 21:24, 15 May 2013 (UTC)
• I agree. Anyone available to implement this? Matthew C. Clarke 22:25, 14 May 2014 (UTC)
• 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)

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.

Principia Mathematica ref

The article currently states:

The principle was stated as a theorem of propositional logic by Russell and Whitehead in Principia Mathematica as:

$P\leftrightarrow \neg (\neg P)$

But it Does not. Its not a simple one liner like that and the notation is all wrong. I've never seen $\neg P$ used this way myself, mostly ${\overline {P}}$ or ${\dot {P}}$ and this specific book uses $\thicksim p$, primitives are always lower case (p, not P) and $\leftrightarrow$ would be $.=.$

Book 1, Page 106 states that "proposition *2•14 with *2•12. constitutes the principle of double negation."

Where the proposition are

$\mathbf {*2\cdot 12} .\ \ \vdash .\ p\ {\boldsymbol {\supset }}\ \thicksim (\thicksim p)$

$\mathbf {*2\cdot 14} .\ \ \vdash .\thicksim (\thicksim p)\ {\boldsymbol {\supset }}\ p$

As the Book is pre 1923, its public domain so I can upload an image if need be (with proofs)

remember to check your sourcesLarek (talk) 02:37, 14 April 2012 (UTC)

Talk about a foot in my mouth, I'm wrong in the "Its not a simple one liner" part, it is there, on page 121.

$\mathbf {*4\cdot 13} .\ \ \vdash .\ p\ \equiv \ \thicksim (\thicksim p)$

"This is the principle of double negation, i.e. a proposition is equivalent of the falsehood of its negation."

The Notation is still wrong thoughLarek (talk) 02:50, 14 April 2012 (UTC)

---

The article commits the double sin of not defining its symbols and then mixing its (undefined) symbols. I fiddled with it, added some references and sourcing. If the article is ever expanded, there is something more in Kleene 1967:15 footnote 17: "Following Church 1956 p. 73, *49 may be called more specifically the "complete law of double negative"; 8 [implicative formula page 16: 8^o. ⊧ ¬¬A ⊃ A ] the "law of double negation" simply; and the converse of 8 the "converse law of double negation".". In Kleene 1952:119 we see this converse law *49a. ⊦ A ⊃ ¬¬A, which is apparently not intuitionistically objectionable. In the years from 1952-1967 Kleene has changed his ⊦ to ⊧. BillWvbailey (talk) 16:01, 14 April 2012 (UTC)

I was pulling from the Freely available 1 ed (djvu format) but is also online at http://name.umdl.umich.edu/aat3201.0001.001 and the specific page is at http://quod.lib.umich.edu/u/umhistmath/aat3201.0001.001/143?view=image&size=100, which may be a better reference than a random reprinting of the second Edition. Larek (talk) 17:04, 14 April 2012 (UTC)

Actually the reprint is "official" and is of the 2nd edition first *52 sections. These are much different than in the first edition. I don't think folks realize this, and it takes careful scrutiny to figure out exactly what Russell changed. Entire sections are deleted and substitutions made for other sections, etc. Plus there's an important preface to the 2nd edition as well. I don't think the page number nor edition is terribly important. What is important was your complaint, which was valid and I hope I addressed. (Strangely, I could not find the 2nd quote, but it sounds familiar. I'm sure its in there somewhere.) BillWvbailey (talk) 20:51, 14 April 2012 (UTC)

Arithmetic Equivalent

Should we add a section with the arithmetic equivalent of a logic Not and then algebraically show that Not Not is the original? This would help anyone not well versed in logic as the can type it into their calculator.

The algebraic equivalent to $\thicksim p$ (Not P) is: (when using only 1,0 as possible values, equivalent to true and false)

$\thicksim p=(-1)*p+1$

Then double negation is:

$\thicksim {\Big (}\thicksim p{\Big )}=(-1)*{\Big (}(-1)*p+1{\Big )}+1$

Which reduces:

$\thicksim {\Big (}\thicksim p{\Big )}={\Big (}(-1)*(-1)*p+(-1)*1{\Big )}+1$

$\thicksim {\Big (}\thicksim p{\Big )}={\Big (}(1)*p+(-1){\Big )}+1$

$\thicksim {\Big (}\thicksim p{\Big )}={\Big (}p-1{\Big )}+1$

$\thicksim {\Big (}\thicksim p{\Big )}=p-1+1$

$\thicksim {\Big (}\thicksim p{\Big )}=p$

Its just a thought, to add some content to this tiny page Larek (talk) 15:53, 15 April 2012 (UTC)

A much simpler version comes directly out of "Boolean logic" (propositional calculus composed in Boolean algebra -- you can see this from Venn diagrams, as well):

~p =_def (1 - p)

~(q) =_def (1 - q), then q ≡ ~p, by substitution (1 - (~p)) => by arithmetic (1 - (1 - p)) = p

Did Boole himself use double-negation? Probably not -- see the quote below. (His Laws of thought is on-line, might be a bit tedious search). I looked through my Grattan-Guinness & Bornet 1997 "George Boole: Selected Mansucripts on Logic and its Philosophy" but didn't find anything specific to double negation; Boole was chiefly interested in, as two laws of thought: x(1-x)=0, i.e. the law of contradiction, and x + (1-x) = 1, the law of excluded middle (cf page xxix); they note " "-" represented the subtraction of a class from a one of which it was a part; however, since he never used a symbol for "not", his expression of that law was not complete (Ellis 1863a)" (cf page xxix).

(I'm not familiar with Ellis). On page 16 I find the quote: "Thus men being a term of affirmative quality, not-men will be a term of negative quality . . .Thus as all beings in the Universe are either men or not men, the two classes All men and All not men will make up that universe (p. 16, from Boole's ca 1849 Elementary Treatise on Logic not mathematical).

What I conclude here is: the historical provenance of double negation is unclear and would need research. Some possible names are Jevons and Venn (his diagrams) and in particular Hugh MacColl; G-G & B credit MacColl with what we think of as the propositional calculus written in "Boolean Algebra" (cf page xlvi). If I find anything I'll add it here. BillWvbailey (talk) 18:09, 15 April 2012 (UTC)

Double Negation Elimination Merge Issue

In the opening of the Double Negation page the following statement is made in which I believe is a false representation:

Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic,[2] but it is disallowed by intuitionistic logic.[3]

The issue here I believe comes from the merging of 'Double Negation Elimination' into 'Double Negation'. In Intuitionistic Logic Double Negation Elimination is disallowed but Double Negation Introduction is allowed. The article is implying that all types of Double Negation is disallowed in intuitionistic logic which is not the case.

I think the article needs to be changed to have a summary of double negation, and then break out elimination and introduction into their own sub categories. — Preceding unsigned comment added by Chrisomills (talk • contribs) 16:06, 15 January 2016 (UTC)

Really necessary to prove L2?

The article states that

(7) $\varphi _{0}\to ((\varphi _{0}\to p)\to p)$       (instance of (L2))

but isn't $\varphi _{0}\to ((\varphi _{0}\to p)\to p)$ actually instance of Modus Ponens, i.e. from $\varphi _{0}$ and $\varphi _{0}\to p$, infer $p$?

Mikko.nummelin (talk) 18:21, 5 September 2023 (UTC)