 Intuitionistic logic can be described as classical logic without LEM (or the principle of double negation \((\neg \neg \phi \to \phi)\)), but with the classical law of contradiction \(((\phi \to \psi) \to ((\phi \to \neg \psi) \to \neg \phi))\) and ex falso quodlibet \((\neg \phi \to (\phi \to \psi))\). Related to its rejection of LEM, intuitionistic logic satisfies the disjunction property (Gödel 1932). A logic is said to have the disjunction property if whenever \((\phi \vee \psi)\) is provable in the logic, so is at least one of \(\phi\) and \(\psi\). Classical logic does not have such property (\(\vdash_{CL} (p \vee \neg p)\), without \(\vdash_{CL} p \) or \(\vdash_{CL} \neg p\)) but has a weaker property called Halldén-completeness: every provable disjunction whose disjuncts don’t share any propositional variables has at least one of those disjuncts provable.