Camillo Fiorentini (University of Milano)
Abstract: Proof theory for non-classical logics has been deeply investigated. Standard techniques to prove the completeness of a calculus are based on syntactic methods, mostly relying on cut-elimination. The main drawback is that, from a failed proof-search, no information about the non-validity of a formula is gained.
An alternative way is to exploit semantics: to prove that a calculus is complete, one has to show that, whenever a formula is not provable in the calculus, a countermodel for it can be built. A countermodel can be viewed as a certificate of the non-validity of a formula; moreover, from an inspection of the completeness proof, one can design efficient proof-search strategies for the calculus at hand.
In the course we present efficient proof-search strategies supporting countermodel generation, focusing on Intuitionistic Propositional Logic. We present the main ideas beyond the technique and some significant examples.