Proof Methods for Modal and Intuitionistic Logics

Abstract

Tableau, natural deduction, gentzen sequent and axiomatic proof procedures are given for most well-known modal logics, both normal and regular non-normal, in both propositional and quantified versions. also intuitionistic logic is covered. completeness proofs relative to kripke models are made uniform by introducing "consistency properties." constructive proofs of interpolation theorems are given. modal consequence is discussed; modal deduction theorems are proved. the tableau systems are generalizations of those of smullyan ("first order logic", springer).