  Up to now we have tacitly assumed our background logic to be the usual classical logic. But the true depth of the connection between AC and logic emerges only when intuitionistic or constructive logic is brought into the picture. It is a remarkable fact that, assuming only the framework of intuitionistic logic together with certain mild further presuppositions, the Axiom of Choice can be shown to entail the cardinal rule of classical logic, the law of excluded  middle—the assertion that \(A \vee \neg A\) for any proposition \(A\). To be precise, using the rules of intuitionistic logic within our augmented language \(L\), we shall  derive[15]  the law of excluded middle from AC1L conjoined with the following additional principles: