Schütte Countermodels and Sequent Calculi

Abstract

In this thesis the Schütte style completeness proof is used as a tool to compare different sequent calculi. The Schütte style countermodel construction is the most important part of this kind of completeness proof. This countermodel construction method is used to compare three different sequent systems for the modal logics K, T, K4, and S4: A basic modal sequent calculus system, a tree-hypersequent system and a labeled sequent system. In the first part of the thesis we define what is meant with a Schütte countermodel and the question is answered whether the possible Schütte style countermodels produced using these sequents calculi are exactly the same sets of countermodels for each type calculus or whether it depends on the sequent system what models can be constructed. It is proven that each Schütte countermodel that can be constructed in one sequent system can also be constructed in the other types of systems. This shows that the set of constructable Schütte countermodels for these calculi are the same. As an additional part of the thesis, we explore Schütte countermodel construction for the intuitionistic modal logic DYK.