Nordic Online Logic Seminar

In this talk, our main goal is to show how to provide a uniform, purely syntactic, and proof-theoretic treatment of a wide range of logics: starting from S5, we then move to its multi-agent version, reach Public Announcement Logic (PAL), and finally conclude (by hinting how to treat the case of) Dynamic Epistemic Logic (DEL). To achieve our goal, we will use hypersequents – generalizations of classical Gentzen-style calculus – which will first be extended to cover the multi-agent case, and then become dynamic hypersequents to capture the dynamism inherent to PAL and DEL. We will show how each calculus can be obtained through changes to the logical rules while structural rules always remain admissible, including contraction rules. Every calculus is sound and complete, and satisfies the cut-elimination theorem. We will conclude the talk with some general observations and indications of future paths of research. The talk is partly based on a joint work with C. Lerouvillois

Two agents with the same information and awareness may hold different beliefs because of inattention. Attention differs from awareness: while awareness determines what is available for reasoning, attention determines what is actually taken into account. Existing epistemic logics do not typically address this distinction explicitly.

In this talk, I will discuss how attention and awareness can be represented in epistemic logic, what distinguishes them, and how they shape belief.

I will introduce the basic framework and look at some of the applications to 1philosophy and linguistics.

Dependence logic extends first-order logic with dependence atoms, which express that the value of a variable is functionally determined by other variables. Team semantics gives dependence logic a second-order flavour, and even quantifier-free dependence logic formulas can have an NP-complete model-checking problem. This motivates the study of syntactic conditions under which model checking becomes tractable.

The talk starts with a brief introduction to team semantics and dependence logic, and then focuses on coherence, a notion introduced by Jarmo Kontinen to capture when the satisfaction of a formula can be determined by satisfaction by its small subteams. We show that, for quantifier-free formulas, coherence is precisely equivalent to first-order rewritability. We also study the complexity of deciding coherence, obtaining strong undecidability results for dependence logic and a precise complexity classification for propositional dependence logic.

The talk is based on joint work with Timon Barlag, Nicolas Fröhlich, Miika Hannula, Phokion G. Kolaitis, Arne Meier, and Jouko Väänänen: https://arxiv.org/abs/2605.31269