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.
|
|
|