 as the only rule of inference. Intuitionistic logic has been an object of investigation ever since Heyting formulated it. Already at the propositional level it has many properties that sets it apart from classical logic, such as the Disjunction Property: 