This series of tutorials is based on [2, 3, 1] (one paper by day). An improved version of these papers is currently under revision, but should (normally) appear in the Journal of Applied Non-Classical Logics this year.

1. Calculi for Basic Atomic Logics

Atomic logics are based on Dunn’s Gaggle theory and generalize modal logic and the Lambek calculus. Sound and complete Hilbert, display and sequent calculi for basic atomic logics with a Kripke-style relational semantics are introduced. These calculi can be automatically computed from the definition of the connectives defining a basic atomic logic. Sufficient conditions for the cut admissibility of these calculi are given based on the shape of the connectives considered. We also show that there is a very tight connection between the monotonicity of a connective and the Kripke-style relational semantics. Finally, we prove that basic atomic logics are all compact, decidable and in NExpTime and that their model checking problem is in PTime.

2. Correspondence Theory for Atomic Logics

The correspondence theory for the framework of atomic and molecular logics is developed on the basis of the work of Goranko & Vakarelov. Using an embedding of modal polyadic logics into atomic logics, we reformulate the notion of inductive formulas introduced by Goranko & Vakarelov into our framework. This allows us to prove correspondence theorems for atomic logics by adapting their results. We apply our general results to FDE, the family of relevance logics, intuitionistic logic and intermediate logics. We obtain novel axiomatizations of these logics that include Boolean connectives.

3. A Characterization of Properly Displayable Atomic Logics

The general results of Ciabattoni & Ramanayake about display calculi are applied to the framework of atomic logics. We obtain an instantiation of their “I2 acyclic” formulas in this framework. Then, we show that our versions of I2 acyclic formulas are inductive formulas in the sense of Goranko & Vakarelov, again adapted to this framework. This allows us to provide a characterization of displayable calculi extending basic atomic logics in terms of these formulas : a calculus is properly displayable iff it is sound and complete w.r.t. a class of frames defined by I2 acyclic formulas. As corollary of the admissibility of the cut rule in display calculi, we obtain sufficient conditions for obtaining conservative extensions of logics. Then, we give examples of correspondences between structural inference rules and first-order frame properties and we detail some of the computations that enable to transform one to the other. Finally, we apply our characterization theorem to propositional logic, FDE, the family of relevance logics, intuitionistic and intermediate logics and obtain novel calculi and conservativity results for these logics. In particular, we show how classical and standard inference rules reappear as simplifications of more general and abstract rules that stem from the display calculi of our atomic logics.

References

 [1] Guillaume Aucher. A Characterization of Properly Displayable Atomic Logics. Research report, Université de Rennes 1, 2024. URL : https://hal.inria.fr/hal-03800070.

[2] Guillaume Aucher. Calculi for Basic Atomic Logics. Research report, Université de Rennes 1, 2024. URL : https://hal.inria.fr/hal-03800002.

[3] Guillaume Aucher. Correspondence Theory of Atomic Logics. Research report, Université de  Rennes, 2024. URL : https://hal.inria.fr/hal-03800044.