Nested Sequents for First-Order Modal Logics via Reachability Rules

Talk by Tim Lyon

Location: APB room 3027
Start: 15. December 2022 at 11:00 am
End: 15. December 2022 at 12:00 pm
Event series: Research Seminar Logic and AI
iCal

In this talk, we present cut-free nested sequent calculi for first-order modal logics. We consider a diverse class of first-order modal logics obtained by imposing certain Horn conditions on the relational and domain structure of QK models. Labeled sequent calculi are then obtained via standard techniques from the semantics of these logics. We show how to derive nested calculi from labeled via the 'structural refinement' technique, which consists of eliminating structural rules, introducing reachability rules, and translating notation. The reachability rules obtained via this method possess a unique functionality, consisting of propagating and/or checking if data exists along certain paths within a nested sequent. We demonstrate how such rules operate and touch on the significance of the nested sequent formulation (in the first-order setting) which emerges naturally from the structural refinement methodology.