In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Although it is quite freely used in mathematical proofs, not every school of mathematical thought accepts this kind of nonconstructive proof as universally valid. More broadly, proof by contradiction is any form of argument that establishes a statement by arriving at a contradiction, even when the initial assumption is not the negation of the statement to be proved. In this general sense, proof by contradiction is also known as indirect proof, proof by assuming the opposite, and reductio ad impossibile. A mathematical proof employing proof by contradiction usually proceeds as follows: The proposition to be proved is P. We assume P to be false, i.e., we assume ¬P. It is then shown that ¬P implies falsehood. This is typically accomplished by deriving two mutually contradictory assertions, Q and ¬Q, and appealing to the law of noncontradiction. Since assuming P to be false leads to a contradiction, it is concluded that P is in fact true. An important special case is the existence proof by contradiction: in order to demonstrate that an object with a given property exists, we derive a contradiction from the assumption that all objects satisfy the negation of the property. Formalization The principle may be formally expressed as the propositional formula ¬¬P ⇒ P, equivalently (¬P ⇒ ⊥) ⇒ P, which reads: "If assuming P to be false implies falsehood, then P is true." In natural deduction the principle takes the form of the rule of inference which reads: "If is proved, then may be concluded." In sequent calculus the principle is expressed by the sequent which reads: "Hypotheses and entail the conclusion or ." Justification In classical logic the principle may be justified by the examination of the truth table of the proposition ¬¬P ⇒ P, which demonstrates it to be a tautology: Another way to justify the principle is to derive it from the Law of the excluded middle, as follows. We assume ¬¬P and seek to prove P. By the law of excluded middle P either holds or it does not: if P holds, then of course P holds. if ¬P holds, then we derive falsehood by applying the law of noncontradiction to ¬P and ¬¬P, after which the principle of