title: Double negation
text: # Double negation
  
  In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (not-A), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.
  
  Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic, but it is disallowed by intuitionistic logic. The principle was stated as a theorem of propositional logic by Russell and Whitehead in Principia Mathematica as:
  
         $\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."
  
  ## Elimination and introduction
  
  Double negation elimination and double negation introduction are two valid rules of replacement. They are the inferences that, if not not-A is true, then A is true, and its converse, that, if A is true, then not not-A is true, respectively. The rule allows one to introduce or eliminate a negation from a formal proof. The rule is based on the equivalence of, for example, It is false that it is not raining. and It is raining.
  
  The double negation introduction rule is:
  
      P $\Rightarrow$ $\neg$$\neg$P
  
  and the double negation elimination rule is:
  
      $\neg$$\neg$P $\Rightarrow$ P
  
  Where "$\Rightarrow$" is a metalogical symbol representing "can be replaced in a proof with."
  
  In logics that have both rules, negation is an involution.
  
  ### Formal notation
  
  The double negation introduction rule may be written in sequent notation:
  
      $P\vdash \neg \neg P$
  
  The double negation elimination rule may be written as:
  
      $\neg \neg P\vdash P$
  
  In rule form:
  
      ${\frac {P}{\neg \neg P}}$
  
  and
  
      ${\frac {\neg \neg P}{P}}$
  
  or as a tautology (plain propositional calculus sentence):
  
      $P\to \neg \neg P$
  
  and
  
      $\neg \neg P\to P$
  
  These can be combined into a single biconditional formula:
  
      $\neg \neg P\leftrightarrow P$.
  
  Since biconditionality is an equivalence relation, any instance of ¬¬A in a well-formed formula can be replaced by A, leaving unchanged the truth-value of the well-formed formula.
  
  Double negative elimination is a theorem of classical logic, but not of weaker logics such as intuitionistic logic and minimal logic. Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is $\neg \neg \neg A\vdash \neg A$.
  
  Because of their constructive character, a statement such as It's not the case that it's not raining is weaker than It's raining. The latter requires a proof of rain, whereas the former merely requires a proof that rain would not be contradictory. This distinction also arises in natural language in the form of litotes.
  
  ## Proofs
  
  ### In classical propositional calculus system
  
  In Hilbert-style deductive systems for propositional logic, double negation is not always taken as an axiom (see list of Hilbert systems), and is rather a theorem. We describe a proof of this theorem in the system of three axioms proposed by Jan Łukasiewicz:
  
      A1. $\phi \to \left(\psi \to \phi \right)$
      A2. $\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$
      A3. $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$
  
  We use the lemma $p\to p$ proved here, which we refer to as (L1), and use the following additional lemma, proved here:
  
      (L2) $p\to ((p\to q)\to q)$
  
  We first prove $\neg \neg p\to p$. For shortness, we denote $q\to (r\to q)$ by $φ_0.$ We also use repeatedly the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.
  
      (1) $\varphi _{0}$   (instance of (A1))
      (2) $(\neg \neg \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})$   (instance of (A3))
      (3) $(\neg p\to \neg \varphi _{0})\to (\varphi _{0}\to p)$   (instance of (A3))
      (4) $(\neg \neg \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)$   (from (2) and (3) by the hypothetical syllogism metatheorem)
      (5) $\neg \neg p\to (\neg \neg \varphi _{0}\to \neg \neg p)$   (instance of (A1))
      (6) $\neg \neg p\to (\varphi _{0}\to p)$   (from (4) and (5) by the hypothetical syllogism metatheorem)
      (7) $\varphi _{0}\to ((\varphi _{0}\to p)\to p)$   (instance of (L2))
      (8) $(\varphi _{0}\to p)\to p$   (from (1) and (7) by modus ponens)
      (9) $\neg \neg p\to p$   (from (6) and (8) by the hypothetical syllogism metatheorem)
  
  We now prove $p\to \neg \neg p$.
  
      (1) $\neg \neg \neg p\to \neg p$   (instance of the first part of the theorem we have just proven)
      (2) $(\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)$   (instance of (A3))
      (3) $p\to \neg \neg p$   (from (1) and (2) by modus ponens)
  
  And the proof is complete.
  
  