Double negative elimination

In propositional logic, the inference rules double negative elimination (also called double negation elimination, double negative introduction, double negation introduction, or simply double negation) allow deriving the double negative equivalent by adding (for double negative introduction) or removing (for double negative elimination) a pair of negation signs. This is based on the equivalence of, for example,

It is false that it is not raining.

and

It is raining.

Formally, the rule of double negative elimination is

$\frac{\neg\neg A}{\therefore A}.$

The rule of double negative introduction states the converse, that double negatives can be added without changing the meaning of a proposition. Formally, the rule of double negative introduction is

$\frac A{\therefore\neg\neg A}.$

These two rules — double negative elimination and introduction — can be restated as follows (in sequent notation):

$\neg \neg A \vdash A$,

$A \vdash \neg \neg A$.

Applying the deduction theorem to each of these two inference rules produces the pair of valid conditional formulas

$\vdash \neg \neg A \rightarrow A$,

$\vdash A \rightarrow \neg \neg A$,

which can be combined together into a single biconditional formula

$\neg \neg A \leftrightarrow A$.

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. Because of their constructive flavor, 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.) Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is $\neg \neg \neg A \vdash \neg A$.

In set theory also we have the negation operation of the complement which obeys this property: a set A and a set (A^C)^C (where A^C represents the complement of A) are the same.

See also

• Negation
• Gödel–Gentzen negative translation

This logic-related article is a stub. You can help Wikipedia by expanding it.v · Categories: Rules of inference Logic stubs Wikimedia Foundation. 2010. Игры ⚽ Нужно решить контрольную? Neopaganism NTSC Look at other dictionaries: Double Negative — may refer to: Double negative, concept in linguistics Double negative elimination, logic theory Double negation, logic theory p = p; when extended to infinite collections it is disallowed in intuitionistic logic; also considered by some to be one …   Wikipedia Double negation — This article is about the logical concept. For the linguistic concept, see Double negative. In the theory of logic, double negation is expressed by saying that a proposition A is identical to (equivalent to) not (not A), or by the formula A = A.… …   Wikipedia Elimination Chamber (2010) — Promotional poster featuring Batista …   Wikipedia Negation — For other uses, see Negation (disambiguation). In logic and mathematics, negation, also called logical complement, is an operation on propositions, truth values, or semantic values more generally. Intuitively, the negation of a proposition is… …   Wikipedia Outline of logic — The following outline is provided as an overview of and topical guide to logic: Logic – formal science of using reason, considered a branch of both philosophy and mathematics. Logic investigates and classifies the structure of statements and… …   Wikipedia Propositional calculus — In mathematical logic, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules… …   Wikipedia List of topics in logic — This is a list of topics in logic.See also: List of mathematical logic topicsAlphabetical listAAbacus logic Abduction (logic) Abductive validation Affine logic Affirming the antecedent Affirming the consequent Antecedent Antinomy Argument form… …   Wikipedia List of mathematics articles (D) — NOTOC D D distribution D module D D Agostino s K squared test D Alembert Euler condition D Alembert operator D Alembert s formula D Alembert s paradox D Alembert s principle Dagger category Dagger compact category Dagger symmetric monoidal… …   Wikipedia Classical logic — identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well.[1][2] They are characterised by a number of properties:[3] Law of the excluded middle and… …   Wikipedia List of basic topics in logic — For a more comprehensive list, see the List of logic topics. Logic, a branch of both philosophy and mathematics, is the study of criteria for the evaluation of arguments. The task of the logician is to advance an account of valid and fallacious… …   Wikipedia 18+ © Academic, 2000-2024 Contact us: Technical Support, Advertising Dictionaries export, created on PHP, Joomla, Drupal, WordPress, MODx. Mark and share Search through all dictionaries Translate… Search Internet Share the article and excerpts Direct link … Do a right-click on the link above and select “Copy Link”