Editing Intuitionistic logic (section)

===Double negations===
A double negation  does not affirm the law of the excluded middle ([[Principle of excluded middle|PEM]]); while it is not necessarily the case that PEM is upheld in any context, no counterexample can be given either. Such a counterexample would be an inference (inferring the negation of the law for a certain proposition) disallowed under classical logic and thus PEM is not allowed in a strict weakening like intuitionistic logic. Formally, it is a simple theorem that <math>\big((\psi\lor(\psi\to\varphi))\to\varphi\big) \leftrightarrow \varphi</math> for any two  propositions. By considering any <math>\varphi</math> established to be false this indeed shows that the double negation of the law <math>\neg\neg(\psi\lor\neg\psi)</math> is retained as a tautology already in [[minimal logic]]. This means any <math>\neg(\psi\lor\neg\psi)</math> is established to be inconsistent and the propositional calculus is in turn always compatible with classical logic.

When assuming the law of excluded middle implies a proposition, then by applying contraposition twice and using the double-negated excluded middle, one may prove double-negated variants of various strictly classical tautologies. The situation is more intricate for predicate logic formulas, when some quantified expressions are being negated.

==== Double negation and implication====
Akin to the above, from modus ponens in the form <math>\psi\to((\psi\to\varphi)\to\varphi)</math> follows <math>\psi\to\neg\neg\psi</math>. The relation between them may always be used to obtain new formulas: A weakened premise makes for a strong implication, and vice versa. For example, note that if <math>(\neg\neg \psi) \to \phi</math> holds, then so does <math>\psi \to \phi</math>, but the schema in the other direction would imply the double-negation elimination principle. Propositions for which double-negation elimination is possible are also called '''stable'''. Intuitionistic logic proves stability only for restricted types of propositions. A formula for which excluded middle holds can be proven stable using the [[disjunctive syllogism]], which is discussed more thoroughly below. The converse does however not hold in general, unless the excluded middle statement at hand is stable itself.

An implication <math>\psi \to \neg\phi</math> can be proven to be equivalent to <math>\neg\neg\psi \to \neg\phi</math>, whatever the propositions. As a special case, it follows that propositions of negated form (<math>\psi=\neg\phi</math> here) are stable, i.e. <math>\neg\neg\neg\phi \to \neg\phi</math> is always valid.

In general, <math>\neg\neg \psi \to \phi</math> is stronger than <math>\psi \to \phi</math>, which is stronger than <math>\neg\neg (\psi \to \phi)</math>, which itself implies the three equivalent statements <math>\psi \to (\neg\neg \phi)</math>, <math>(\neg\neg \psi) \to (\neg\neg \phi)</math> and <math>\neg\phi\to\neg\psi</math> . Using the disjunctive syllogism, the previous four are indeed equivalent. This also gives an intuitionistically valid derivation of <math>\neg\neg(\neg\neg\phi\to\phi)</math>, as it is thus equivalent to an [[law of identity|identity]].

When <math>\psi</math> expresses a claim, then its double-negation <math>\neg\neg\psi</math> merely expresses the claim that a refutation of <math>\psi</math> would be inconsistent. Having proven such a mere double-negation also still aids in negating other statements through [[negation introduction]], as then <math>(\phi\to\neg\psi)\to\neg\phi</math>. A double-negated existential statement does not denote existence of an entity with a property, but rather the absurdity of assumed non-existence of any such entity. Also all the principles in the next section involving quantifiers explain use of implications with hypothetical existence as premise.

====Formula translation====
Weakening statements by adding two negations before existential quantifiers (and atoms) is also the core step in the [[Gödel-Gentzen translation|double-negation translation]]. It constitutes an [[embedding]] of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. For example, any theorem of classical propositional logic of the form  <math>\psi\to\phi</math> has a proof consisting of an intuitionistic proof of <math>\psi\to\neg\neg\phi</math> followed by one application of double-negation elimination. Intuitionistic logic can thus be seen as a means of extending classical logic with constructive semantics.