stylistic:style_transfer, structural:summarization
Double negation and implication

Akin to the above, from modus ponens in the form ψ → ((ψ → φ) → φ) {\displaystyle \psi \to ((\psi \to \varphi)\to \varphi)} follows ψ → ¬ ¬ ψ {\displaystyle \psi \to \neg \neg \psi }. 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 (¬ ¬ ψ) → ϕ {\displaystyle (\neg \neg \psi)\to \phi } holds, then so does ψ → ϕ {\displaystyle \psi \to \phi }, 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 ψ → ¬ ϕ {\displaystyle \psi \to \neg \phi } can be proven to be equivalent to ¬ ¬ ψ → ¬ ϕ {\displaystyle \neg \neg \psi \to \neg \phi }, whatever the propositions. As a special case, it follows that propositions of negated form (ψ = ¬ ϕ {\displaystyle \psi =\neg \phi } here) are stable, i.e. ¬ ¬ ¬ ϕ → ¬ ϕ {\displaystyle \neg \neg \neg \phi \to \neg \phi } is always valid.

In general, ¬ ¬ ψ → ϕ {\displaystyle \neg \neg \psi \to \phi } is stronger than ψ → ϕ {\displaystyle \psi \to \phi }, which is stronger than ¬ ¬ (ψ → ϕ) {\displaystyle \neg \neg (\psi \to \phi)}, which itself implies the three equivalent statements ψ → (¬ ¬ ϕ) {\displaystyle \psi \to (\neg \neg \phi)}, (¬ ¬ ψ) → (¬ ¬ ϕ) {\displaystyle (\neg \neg \psi)\to (\neg \neg \phi)} and ¬ ϕ → ¬ ψ {\displaystyle \neg \phi \to \neg \psi }. Using the disjunctive syllogism, the previous four are indeed equivalent. This also gives an intuitionistically valid derivation of ¬ ¬ (¬ ¬ ϕ → ϕ) {\displaystyle \neg \neg (\neg \neg \phi \to \phi)}, as it is thus equivalent to an identity.

When ψ {\displaystyle \psi } expresses a claim, then its double-negation ¬ ¬ ψ {\displaystyle \neg \neg \psi } merely expresses the claim that a refutation of ψ {\displaystyle \psi } would be inconsistent. Having proven such a mere double-negation also still aids in negating other statements through negation introduction, as then (ϕ → ¬ ψ) → ¬ ϕ {\displaystyle (\phi \to \neg \psi)\to \neg \phi }. 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.