Semantics based proof-search methods for non-classical logics
Introductory course at ESSLLI 2021,
32nd European Summer School
in Logic, Language and information.
26 July - 13 August 2021, Held virtually.
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.
Schedule
Week 3, from Monday 9 to Friday 13 August (5 lectures), 9.45-11.15.
Material
Lecture notes (updated 10 August).
Questions, comments, ... are welcome.
In the course I have presented the topics in Chapters 1-4.