Title: A generalized version of van Benthem's theorem for non-classical logics

 

Speaker: Dr. Guillaume Aucher ( University of Rennes 1, Homepage)

 

Time: Jan. 11 16:00-18:00

 

Location: Room 106, Department of Philosophy, PKU

 

Abstract: Most of non-classical logics used in artificial intelligence are fragments of first-order logic (FOL). A non-classical logic is often characterized with respect to FOL by a specific notion of invariance which relates models satisfying the same formulas of the non-classical logic. For example, bisimulation is the notion of invariance of modal logic: any formula of FOL whose truth value is always the same in any two bisimilar models is equivalent to the standard translation of a formula of modal logic into FOL. We define and investigate notions of invariance for the class of non-classical logics whose connectives are defined by formulas of FOL. We introduce specific normal form formulas for FOL such that any formula of FOL can be decomposed into a conjunction or a disjunction of such normal form formulas. These normal form formulas for FOL are such that a notion of invariance can be automatically obtained from the connective to which they are associated. Then, we obtain the notion of invariance of a given non-classical logic by decomposing each of its connectives into our ‘normal form connectives’. Using methods and results from model theory, we then prove a theorem which allows us to obtain automatically the expressive completeness of some non-classical logics with respect to FOL. In particular, we obtain the famous van Benthem’s theorem for modal logic as a specific instance of our generic theorem. Our unified approach and techniques allow us as well to obtain automatically cut-free display calculi for some non-classical logics. We will also briefly address these other proof-theroretical results in this talk.