"Construction of Counter-models for Intuitionistic Propositional Logic"

Abstract

It is well-known that Intuitionistic Propositional Logic (IPL) is decidable. Dyckhoff's contraction-free sequent calculus LJT, having the termination property (i.e. every development of a partial derivation terminates), provides a good basis for an effective decision procedure for IPL. The calculus CRIP, introduced by Dyckhoff and Pinto, captures unprovability for IPL (i.e. any sequent is either derivable in LJT or in CRIP) and is also terminating. Out of derivations in CRIP one can build counter-models for IPL. Dyckhoff and Pinto showed how to do it for Kripke semantics and, along the same lines, Negri and von Plato showed how to witness non-theoremhood of IPL based on Heyting algebras. In this seminar talk we review all these ideas.