Games, modalities and analytic proofs in nonclassical logics

Abstract

The present thesis deals with three different topics in the proof theory of nonclassical logics. We first investigate logics which are presented as analytic hypersequent calculi. Using a projection of cutfree hypersequent proofs onto proofs in the sequent calculus, we obtain various strengthenings of the deduction theorem. In the second part we develop a sequent calculus with a game-theoretic underpinning. By stipulating that the use of certain rules triggers costs, we gain expressivity which in turn can be captured by a suitable labelling of the proof rules. We show some syntactic results about the thus obtained labelled sequent calculus. The concluding third part employs the method of provability-preserving syntactic translations to study a deontic modal logic which extends classical modal logic. Our main result is that a substantial fragment of the deontic logic can be reduced to the underlying classical modal logic.