Dear all,

We will have our next LIRa session on Thursday, 8 June 16:30.

This will be a hybrid session. If you want to attend online, please use our recurring zoom link: https://uva-live.zoom.us/j/89230639823?pwd=YWJuSnJmTDhXcWhmd1ZkeG5zb0o5UT09 (Meeting ID: 892 3063 9823, Passcode: 421723)

You can find the details of the talk below.

Speaker: Jan Rooduijn (ILLC)

Date and Time: Thursday, June 8th 2023, 16:30-18:00

Venue: KdVI seminar room F3.20 in Science Park 107 and online

Title: An analytic proof system for common knowledge logic over S5

Abstract. Common knowledge logic (CKL) extends multi-agent epistemic logic by a common knowledge operator. This operator is interpreted as an infinitary conjunction expressing that a statement is true, all agents know that it is true, all agents know that all agents know that it is true, and so forth. Hilbert-style proof systems typically axiomatise the common knowledge operator using an induction axiom. However, the natural adaptation of this axiom to a Gentzen-style rule requires cut. Even worse, it requires cut formulas outside the context of the proof's conclusion, i.e. non-analytic applications of the cut rule. One solution for still obtaining a nice Gentzen-style system is to turn to cyclic proofs, which replace the explicit induction rule by a more implicit mechanism involving infinite branches.

Most existing cyclic proof systems are for logics on which no frame conditions are imposed. This is unnatural for CKL, as one usually assumes certain epistemic principles. One popular frame condition, related to the indistinguishability interpretation of knowledge, requires all accessibility relations to be equivalence relations. In other words, one takes a version of CKL based on the modal logic S5. We will call this logic S5-CKL.

In this talk, I will present joint work with Lukas Zenger, in which we construct a cyclic proof system for S5-CKL. Because S5 itself already requires analytic applications of the cut rule, our system does as well. However, unlike for the system with an explicit induction rule, analytic applications suffice for our approach. As a consequence, we show that our system admits an optimal procedure for proof search, and therefore for the validity problem of S5-CKL.

In the final part of my talk, I will compare our proof system to various other systems, and I will provide some ideas for applications and future work.

This talk is based on a paper accepted at AiML 2022. A preprint can be found here: https://staff.fnwi.uva.nl/j.m.w.rooduijn/papers/S5_aiml22.pdf

Hope to see you there!

The LIRa team