V\'{\i }t\v {e}zslav \v {S}vejdar
On sequent calculi for intuitionistic propositional logic

Comment.Math.Univ.Carolinae 47,1 (2006) 159-173.

Abstract:The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.

Keywords: intuitionistic logic, polynomial-space, sequent calculus, Kripke semantics
AMS Subject Classification: 03B20, 03B35, 03F05

PDF