 Formalized intuitionistic logic is naturally motivated by the informal Brouwer-Heyting-Kolmogorov explanation of intuitionistic truth, outlined in the entries on  intuitionism in the philosophy of mathematics  and  the development of intuitionistic logic.  The constructive independence of the logical operations \(\oldand, \vee , \rightarrow , \neg , \forall , \exists\) contrasts with the classical situation, where e.g., \(A \vee B\) is equivalent to \(\neg(\neg A \oldand \neg B),\) and \(\exists xA(x)\) is equivalent to \(\neg \forall x \neg A(x).\) From the B-H-K viewpoint, a sentence of the form \(A \vee B\) asserts that either a proof of \(A,\) or a proof of \(B,\) has been constructed; while \(\neg(\neg A \oldand \neg B)\) asserts that an algorithm has been constructed which would effectively convert any pair of constructions proving \(\neg A\) and \(\neg B\) respectively, into a proof of a known contradiction.