Rosalie Iemhoff

Among the numerous logics that are studied and applied nowadays, many can be described via a proof system, which captures the valid reasoning that can be carried out in the logic, and there are many examples of well-known concrete proof systems that occur in various areas in logic and beyond.

As is well-known, a single logic has many different proof systems, and not every system is as useful as another. Given the goal of the proof-theoretic formalization, be it philosophical or mathematical or of a different nature, one can often distinguish among the proof systems of the logic a class of good proof systems, proof systems with properties that makes them useful in the investigation of the logic. A well-known example are analytic sequent calculi and their use in proving properties of the logic such as decidability or interpolation. But there are many other examples, some of which will be discussed during the talk.

Given a class of such useful proof systems the questions naturally arise whether a certain logic has such a good proof system or not, and what it means for a logic to have such proof systems. These are no easy questions to answer and stated in such generality they may not always have a reasonable answer. But for concrete classes of logics and proof systems something insightful can be said. In this talk the aim is to do so for intermediate and (intuitionistic) modal logics, where the proof systems that are considered are sequent calculi. And although no full answer is obtained, some small steps in that direction are taken.

---