explosion allows us to conclude P. In either case, we established P. It turns out that, conversely, proof by contradiction can be used to derive the law of excluded middle. In classical sequent calculus LK proof by contradiction is derivable from the inference rules for negation: Relationship with other proof techniques Refutation by contradiction Proof by contradiction is similar to refutation by contradiction, also known as proof of negation, which states that ¬P is proved as follows: The proposition to be proved is ¬P. Assume P. Derive falsehood. Conclude ¬P. In contrast, proof by contradiction proceeds as follows: The proposition to be proved is P. Assume ¬P. Derive falsehood. Conclude P. Formally these are not the same, as refutation by contradiction applies only when the proposition to be proved is negated, whereas proof by contradiction may be applied to any proposition whatsoever. In classical logic, where and may be freely interchanged, the distinction is largely obscured. Thus in mathematical practice, both principles are referred to as "proof by contradiction". Law of the excluded middle Proof by contradiction is equivalent to the law of the excluded middle, first formulated by Aristotle, which states that either an assertion or its negation is true, P ∨ ¬P. Law of non-contradiction The law of noncontradiction was first stated as a metaphysical principle by Aristotle. It posits that a proposition and its negation cannot both be true, or equivalently, that a proposition cannot be both true and false. Formally the law of non-contradiction is written as ¬(P ∧ ¬P) and read as "it is not the case that a proposition is both true and false". The law of non-contradiction neither follows nor is implied by the principle of Proof by contradiction. The laws of excluded middle and non-contradiction together mean that exactly one of P and ¬P is true. Proof by contradiction in intuitionistic logic In intuitionistic logic proof by contradiction is not generally valid, although some particular instances can be derived. In contrast, proof of negation and principle of noncontradiction are both intuitionistically valid. Brouwer–Heyting–Kolmogorov interpretation of proof by contradiction gives the following intuitionistic validity condition: "If there is no method for establishing that a proposition is false, then there is a method for establishing that the proposition is true." If we take "method" to mean algorithm, then the condition is not acceptable, as it would allow us to solve the Halting problem. To