- Francesca Poggiolesi

IHPST

One of the big open problems of modal logic is to find an appropriate proof-
theoretic framewwork, within which proof systems for several modal logics,
such as K, KD, KT, K4, KB, S4, S5 and GL (Godel-Lob logic), can be
constructed.

There have been efforts in this direction since the 60s, the most important of
them (if we consider only the kind of result which can be applied to a large
class of systems of modal logic and not only to one or two systems) are those
of A. Avron (1996), A. Indrezejczak (1997), K. Matsumoto and M. Ohnishi
(1957), M. Sato (1977), and H. Wansing (1994).

Unfortunately each of these solutions present some difficulties: for exam-
ple, Sato's system does not have the subformula property, and is unnatural;
Indrezejczak's system lacks a cut elimination proof.

More recently two logicians and philosophers, S. Negri (2005) and G. Restall(2005),
have shown interest for the subject and have proposed two new results,
certainly better than previous ones but still affected by some problems.
Restall's solution seems to be applicable only to S5, and Negri's solution
explicitly includes the semantics of possible words.

What we would like to propose in this paper is a new sequent calculus which
is inspired by these latter results but which is able to improve on them.
This calculus uses a new notion of hypersequent – new with respect to the
one created by A. Avron in 1996 – which allows us to solve the problem in a
quite natural and intuitive way.

The calculus satisfies the subformula property, the separation property, the
symmetry property, the explicit property, the modularity property. Moreover,
it satisfies the Dosen principle (except for GL), is general and purely
syntactic.

- Avron A., ”The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logic.” En W. Hodges, M. Hyland, C. Steinhorn et J. Strauss, editors, Logic: from foundations to applica- tions, p. 1-32. Oxford University Press, 1996. 2.
- Indrezejczak A., Generalised Sequent Calculus for Propositional Modal Logics. Logica Trianguli, volume 1, p. 15-31, 1997. 3.
- Matsumoto K. et Ohnishi M., Gentzen Method in Modal Calculi. Os- aka Mathematical Journal, volume 9, p. 113-130, 1957, et volume 11, p. 115-120, 1959.
- Negri S., Proof Analysis in Modal Logic, Journal of Philosophical Logic 34, p. 507-534, 2005.
- Restall G., Sequents and Circuits for Modal Logic, http://consequently.org/writing/S5nets 2005.
- Sato M., A Study of Kripke-type Models for Some Modal Logics by Gentzen’s Sequential Method. Publications of the Research Institute for Mathematical Sciences, Kyoto University, volume 13, p. 381-468, 1977
- Wansing H., Sequent Calculi for Normal Modal Propositional Logics, Journal of Logic and Computation 2, volume 4, p. 125-142, 1994.