Sematics based proof-search methods for non-classical logics

LoCo Introductoryweek 3

each day

Lecturer:
Camillo Fiorentini (University of Milano)

Website: TBA

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.