A new introduction rule for disjunction

Alejandro Díaz-Caro, Gilles Dowek

We extend Natural Deduction for intuitionistic logic with a third introduction rule for the disjunction, $\vee$-i3, with a conclusion $\hat{I}“⊢A\vee B$, but both premises $Γ\vdas…