Title: What is the (potential) role of proof theory for normative reasoning? Abstract: Normative reasoning is reasoning with and about norms. Its formal corresponding field---i.e., deontic logic---has been largely investigated from a semantic perspective (and its proof systems are mainly axiomatic). Recently, these logics have been gradually receiving more attention from the proof theoretic community (in particular w.r.t. sequent-style systems). A natural question that arises is: what is exactly the potential contribution of proof theoretic approaches to the study of normative reasoning? In this conceptual talk, I will discuss a collection of features of normative reasoning for which proof-theoretic approaches are seemingly suitable. To illustrate one of these features, I will discuss a recent work by Tim Lyon and myself (DEON2021) which uses labelled sequent systems to draw philosophical conclusions about meta-ethical principles in the spirit of `ought-implies-can’.
Agata Ciabattoni (TU Wien)
Tiziano Dalmonte (Aix-Marseille University)
Title: Proof-theory of agency logics of bringing-it-about Abstract: The logic of Bringing-it-About was introduced by Elgesem to formalise the notions of agency and capability. It contains two families of
modalities indexed by agents, the first one expressing what an agent brings about (does), and the second expressing what she can bring about (can do). In this talk I will first present a bi-neighbourhood semantics for this logic, which is more suited for countermodel construction than the semantics defined in the literature. Then I will present a hypersequent calculus for this logic, which leads to a decision procedure allowing for a practical procedure of countermodel extraction. In the last part I will show an extension of both the semantics and the calculus to a coalitional version of Elgesem logic proposed by Troquard. This talk is based on a joint work with Charles Grellois and Nicola Olivetti.
Didier Galmiche (LORIA - Université de Lorraine)
Iris van der Giessen (Utrecht University)
Title: Proving uniform interpolation via nested sequents Abstract: Proof-theoretic methods proving uniform interpolation have been successfully applied to logics described by terminating sequent calculi. In this
talk we turn to nested sequents. A modular method was recently developed to prove the (weaker) Craig interpolation property for modal and intermediate logics based on
multisequent calculi (e.g. nested sequents, hypersequents, and labelled sequents). We expand these ideas to reprove the uniform interpolation property for normal modal
logics K, D, and T via terminating nested sequents. While our method of defining the interpolants is proof-theoretic, we use semantic notions including bisimulation
modulo propositional variables to prove their correctness. We are also able to adjust our method to provide a direct proof of uniform interpolation for S5 using hypersequents.
This is joint work with Raheleh Jalali and Roman Kuznets.
Charles Grellois (Aix-Marseille University)
Alessio Guglielmi (University of Bath)
Title: Concerto pour une Voix Abstract: Subatomic proof systems in deep inference exploit the idea that atoms can be seen as superpositions of values, for example, true and false. Adopting this point of view leads to some dramatic simplifications of proof systems and their proof theory, and this talk provides an example. A single, simple, linear inference shape, together with a certain notion of saturation, generates a proof system for a language of standard boolean operators augmented by decision trees. We prove cut-elimination and several other proof-theoretic results for this proof system. Moreover, the proof system provides cut-free proofs of Statman tautologies that are polynomial in the size of the tautologies, while standard proof systems only yield exponential cut-free proofs. The ideas are natural, simple, and mostly rely on two notions that appear to have very general applicability: projecting proofs around atoms and eversion of formulae. More information about deep inference is at: http://alessio.guglielmi.name/res/cos. Joint work with Chris Barrett and Victoria Barrett.
Roman Kuznets (TU Wien)
Dominique Larchey-Wendling (CNRS and LORIA)
Title: Synthetic Undecidability of MSELL via FRACTRAN mechanised in Coq Abstract: We present an alternate undecidability proof for entailment in (intuitionistic) multiplicative subexponential linear logic (MSELL). We contribute the result and its mechanised proof to the Coq library of synthetic undecidability. The result crucially relies on the undecidability of the halting problem for two counters Minsky machines, which we also hand out to the library. As a seed of undecidability, we start from FRACTRAN halting which we (many-one) reduce to Minsky machines termination by implementing Euclidean division using two counters only. We then give an alternate presentation of those two counters machines as sequent rules, where computation is performed by proof-search, and halting reduced to provability. We use this system called non-deterministic two counters Minsky machines to describe and compare both the legacy reduction to linear logic, and the more recent reduction to MSELL. In contrast with that former MSELL undecidability proof, our correctness argument for the reduction uses trivial phase semantics in place of a focused calculus.
Tim Lyon (TU Dresden)
Title: Nested Sequents for Intuitionistic Modal Logics via Structural Refinement Abstract: We employ a recently developed methodology---called "structural refinement"---to provide nested sequent systems for a sizable class
of intuitionistic modal logics. The methodology consists of transforming labelled sequent systems into nested systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. Our propagation rules are parameterized with formal grammars that allow for certain frame conditions expressible as first-order Horn formulae and which correspond to a subclass of the Scott-Lemmon axioms to be encoded into our nested systems. The nested sequent systems we provide are sound, cut-free complete, and admit hp-admissibility of typical structural rules.
Daniel Méry (LORIA - Université de Lorraine)
Dale Miller (Inria Saclay - Île-de-France and the Laboratoire d'Informatique (LIX))
Title: Contexts in sequents as indexed storage Abstract: By examining focused proof systems for classical and intuitionistic
logics, it is natural to see the contexts used to build sequents as
indexed storage devices. More precisely, a context is a relation
between formulas and indexes. Depending on the nature of such
indexes, sequent calculus proofs can be used to accommodate structures
such as Tseitin constants, De Bruijn indexes, subformula occurrences,
etc. I will cover the motivations for this approach to contexts as
well as illustrate several applications of it.
Nicola Olivetti (Aix-Marseille University)
Title: Proof theory of constructive modal logics Abstract: We present a framework of intuitionistic logics with non-normal modalities that extend the family of constructive modal logics studied in the literature. For these logics we provide both sequent calculi and a semantic characterisation in terms of neighbourhood models. In the second part of the talk we present some sequent calculi for constructive modal logics which terminate without need of loop-checking and directly construct countermodels of non-valid formulas. Joint talk with Tiziano Dalmonte.
Valeria de Paiva (Topos Institute)
Title: Constructive Modalities Abstract: Modalities (temporal, epistemic, deontic, etc) have proved themselves extremely useful in theoretical computer science, multi-agent systems and AI, usually in the setting of classical logic. Recently there seems to be a renewed interest in the notions of *constructive* (or intuitionistic) modal type theory and linear type theory, in part because of the interest in homotopy type theory. Since I have been working on modal extensions of the Curry-Howard correspondence to logical systems since the 90s,
it seems a good idea to recap some of the old ideas associated with modal type theory. Especially because it seems to me that there are plenty of old problems that have not been solved, yet.
Elaine Pimentel (University of Rio Grande de Norte)
Title: Hypersequent calculi for non-normal modal and deontic logics Abstract: In this talk, we will present a gentle introduction to hypersequents for systems of the classical cube and some extensions. Such
calculi are internal, as they only employ the language of the logic, plus additional structural connectives. By showing a translation
between hypersequent rule applications and derivations in a labelled system, we will explain the differences and similarities between
internal and external calculi for the classical cube. Finally, we will show a terminating proof search strategy in the hypersequent
calculi, where from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel out of it.
This is a joint work with Tiziano Dalmonte, Nicola Olivetti and Björn Lellmann.
Revantha Ramanayake (University of Groningen)
Title: Step back from the subformula property Abstract: A sequent calculus with the subformula property implies a highly restricted space of proofs. A restriction on the space of proofs is key to studying the properties of a logic via proof theory. Unfortunately, the sequent calculus does not support the subformula property for most non-classical logics of interest. This has led to the formulation of new proof formalisms such as the hypersequent calculus, nested sequent calculus and so on which extend the structural language to gain the subformula property. I will discuss how we might take into account both the structural and logical language in order to assess the actual restriction on the space of proofs in these formalisms. Based on joint work with A. Ciabattoni and T. Lang.
