The Design of Modal Proof Theories: the case of S5
The Design of Modal Proof Theories: the case of S5
Master's thesis by Phiniki Stouppa
- Supervisor Steffen Hölldobler
- Wissensverarbeitung
- 20 Oktober 2004 – 20 Oktober 2004
- Download
formulations for S5. Through a survey on existing cut-admissible systems for this logic,
we investigate the solutions proposed to overcome this defect. Accordingly, the systems
can be divided into two categories: in those which allow semantic-oriented formulae
and those which allow formulae in positions not reachable by the usual systems in the
sequent calculus. The first solution is not desirable because it is conceptually impure,
that is, these systems express concepts of frame semantics in the language of the logic.
Consequently, we focus on the systems of the second group for which we define
notions related to deep inference - the ability to apply rules deep inside structures
- as well as other desirable properties good systems should enjoy. We classify these
systems accordingly and examine how these properties are affected in the presence
of deep inference. Finally, we present a cut-admissible system for S5 in a formalism
which makes explicit use of deep inference, the calculus of structures, and give reasons
for its effectiveness in providing good modal formulations.
