4.5 Differences between the various logics
Classical logic we see as an extension of intuitionistic logic, which is in turn an extension of minimal logic.
Minimal logic lacks the rule ÏE (Absurdity Elimination, alias "ex falso quodlibet") of intuitionistic logic.
Classical logic replaces this rule by DN, that of double negation (from which ÏE is derivable).
The modal rules can be added to each of the three basic kinds of logic: they are formulated to be independent of a classical or intuitionistic bias.
In constructing proofs, the main difference is that in intuitionistic logic, one has to prove a formula of the form AÎB directly by choosing (perhaps after all other approaches have failed) one of A, B and proving it: in classical logic you can use DN, and try proving ÒÒ(AÎB) instead. Similarly, in intuitionistic logic you must prove (x)A(x) by (if other approaches fail) choosing a term t for which you can find a proof of A(t): but in classical logic, you can try proving ÒÒ(Ex)A(x) instead. This makes the search for natural deduction proofs in intuitionistic logic more straightforward, in that the tactic for double negation is not available.
On the other hand, the mechanical check of validity in classical logic can be done much faster (especially for complex problems) than for the other two logics. However, the Gentzen calculus LK used for this purpose in classical logic is rather different from the one in which proofs are traditionally presented: it corresponds to the semantic tableaux of Beth, Smullyan and Fitting.