Dep. de Matemática
Universidade do Minho, Braga
Thursday, 4 December 2003, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
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.