Editing Intuitionistic logic (section)

====Disjunction vs. implication====
Already minimal logic proves excluded middle equivalent to [[consequentia mirabilis]], an instance of [[Peirce's law]]. 
Now akin to modus ponens, clearly <math>(\phi \lor \psi)\to((\phi\to\psi)\to \psi)</math> already in minimal logic, which is a theorem that does not even involve negations. In classical logic, this implication is in fact an equivalence. With taking <math>\phi</math> to be of the form <math>\psi\to\varphi</math>, excluded middle together with explosion is seen to entail Peirce's law.

In intuitionistic logic, one obtains variants of the stated theorem involving <math>\bot</math>, as follows. Firstly, note that two different formulas for <math>\neg (\phi \land \psi)</math> mentioned above can be used to imply <math>(\neg \phi \vee \neg \psi) \to (\phi \to \neg \psi)</math>. It also followed from direct case-analysis, as do variants where the negations are moved around, such as the theorems <math>(\neg \phi \lor \psi) \to (\phi \to \neg \neg \psi)</math> or <math>(\phi \lor \psi) \to (\neg \phi \to \neg \neg \psi)</math>, the latter being mentioned in the introduction to non-interdefinability. These are forms of the disjunctive [[syllogism]] involving negated propositions <math>\neg\psi</math>. Strengthened forms still holds in intuitionistic logic, say
* <math>(\neg \phi \lor \psi) \to (\phi \to \psi)</math>
The implication cannot generally be reversed, as that would immediately imply excluded middle. So, intuitionistically, "Either <math>P</math> or <math>Q</math>" is generally also a stronger propositional formula than "If not <math>P</math>, then <math>Q</math>", whereas in classical logic these are interchangeable.

Non-contradiction and explosion together actually also prove the stronger variant <math>(\neg \phi \lor \psi) \to (\neg\neg\phi \to \psi)</math>. And this shows how excluded middle for <math>\psi</math> implies double-negation elimination for it. For a fixed <math>\psi</math>, this implication also cannot generally be reversed. However, as <math>\neg\neg(\psi\lor\neg \psi)</math> is always constructively valid, it follows that assuming double-negation elimination for all such disjunctions implies classical logic also.

Of course the formulas established here may be combined to obtain yet more variations. For example, the disjunctive syllogism as presented generalizes to
:<math>\Big(\big(\exists x \ \neg\phi(x)\big)\lor\varphi\Big)\,\,\to\,\,\Big(\big(\forall x \ \phi(x)\big)\to\varphi\Big)</math>
If some term exists at all, the antecedent here even implies <math>\exists x \big(\phi(x)\to\varphi\big)</math>, which in turn itself also implies the conclusion here (this is again the very first formula mentioned in this section).

The bulk of the discussion in these sections applies just as well to just minimal logic. But as for the disjunctive syllogism with general <math>\psi</math> and in its form as a single proposition, minimal logic can at most prove <math>(\neg\phi \lor \psi) \to (\neg\neg \phi \to \psi')</math> where <math>\psi'</math> denotes <math>\neg\neg\psi\land(\psi\lor\neg\psi)</math>. The conclusion here can only be simplified to <math>\psi</math> using explosion.