 Despite the differences in interpretation, there is an important connection between intuitionistic and classical propositional logic. For we know that a formula \(A\) is a theorem of classical propositional logic if, and only if, \(\neg \neg A\) is a theorem of intuitionistic propositional logic. Thus while \((A \vee \neg A)\) is obviously not a theorem of intuitionistic propositional logic, \(\neg \neg (A \vee \neg A)\) is in fact intuitionistically provable. This fact is at the core of a familiar translation from classical into intuitionistic propositional logic due to Kurt Gödel and Gerhard Gentzen. For a summary of this and related facts, the reader may consult the entry on  intuitionistic logic.