 is replaced by LEM), a formal system \(\mathbf{H–CPC}\) for classical propositional logic or \(\mathbf{H–CQC}\) for classical predicate logic results. Since ex falso and the law of contradiction are classical theorems, intuitionistic logic is contained in classical logic. In a sense, classical logic is also contained in intuitionistic logic; see Section 4.1 below.