Editing Intuitionistic logic (section)

==== 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.