Editing Intuitionistic logic (section)

====Disjunction vs. conjunction====
There are finite variations of the quantifier formulas, with just two propositions:
* <math>(\neg \phi \lor \neg \psi) \to \neg (\phi \land \psi)</math>
* <math>(\neg \phi \land \neg \psi) \leftrightarrow \neg (\phi \lor \psi)</math>
The first principle cannot be reversed: Considering <math>\neg \psi</math> for <math>\phi</math> would imply the weak excluded middle, i.e. the statement <math>\neg \psi \lor \neg \neg \psi</math>. But intuitionistic logic alone does not even prove <math>\neg \psi \lor \neg \neg \psi\lor (\neg \neg \psi\to \psi)</math>. So in particular, there is no distributivity principle for negations deriving the claim <math>\neg \phi \lor \neg \psi</math> from <math>\neg(\phi \land \psi)</math>. For an informal example of the constructive reading, consider the following: From conclusive evidence it not to be the case that ''both'' Alice and Bob showed up to their date, one cannot derive conclusive evidence, ''tied to either'' of the two persons, that this person did not show up. Negated propositions are comparably weak, in that the classically valid [[De_Morgan%27s_laws#In_intuitionistic_logic|De Morgan's law]], granting a disjunction from a single negative hypothetical, does not automatically hold constructively. The intuitionistic propositional calculus and some of its extensions exhibit the [[disjunction property]] instead, implying one of the disjuncts of any disjunction individually would have to be derivable as well.

The converse variants of those two, and the equivalent variants with double-negated antecedents, had already been mentioned above. Implications towards the negation of a conjunction can often be proven directly from the non-contradiction principle. In this way one may also obtain the mixed form of the implications, e.g. <math>(\neg \phi \lor \psi) \to \neg (\phi \land \neg \psi)</math>. Concatenating the theorems, we also find
* <math>(\neg \neg \phi \lor \neg \neg \psi) \to \neg \neg (\phi \lor \psi)</math>
The reverse cannot be provable, as it would prove weak excluded middle.

In predicate logic, the constant domain principle is not valid: <math>\forall x \big(\varphi \lor \psi(x)\big)</math> does not imply the stronger <math>\varphi\lor \forall x\,\psi(x)</math>. The [[Distributive_property#Propositional_logic|distributive properties]] does however hold for any finite number of propositions. For a variant of the De Morgan law concerning two existentially closed [[Decidability (logic)|decidable]] predicates, see [[Limited principle of omniscience|LLPO]].