🚀 go-pugleaf

A few months ago I posted a query for articles and books about
Gentzen-style sequent proof systems for modal logics. 
I thank the following people for their responses:

Craig Boutilier         <cebly@cs.ubc.ca>
Hilfred (Hiu Fai) Chau  <hfc@doc.imperial.ac.uk> 
Juan Vicente Echague    <jve@cassiopee.imag.fr>
Senanu Etrey            <sen@cogsci.edinburgh.ac.uk>
Rajeev Gore'            <rpg@cs.man.ac.uk> 
Neil Leslie             <neil@caad.edinburgh.ac.uk>
David Pym               <dpym@dcs.edinburgh.ac.uk>
Jonathan Seldin         <seldin@alcor.concordia.ca>
Steffo Weber            <steffo@kibosh.informatik.uni-dortmund.de>

Below is a list of references compiled from their reactions:

[I apologize for the delayed posting of this summary. It is due 
 to problems with posting combined with the absence of our 
 systems operator, and a subsequent long holiday of myself]

--

Fitting, M. Proof Methods for Modal and Intuitionistic Logics.

Wallen, L. Automated Deduction in Non-classical Logics. MIT Press.

--

@article{dosen,
	author = "K. Dosen",
	title = "Sequent-Systems for Modal Logic"
	journal = jsl,
	year = 1985,
	volume = 50,
	number = 1,
	month = mar
	}

@techreport{echague91,
	author = "J. V. Echag{\"u}e",
	title = "A {Gentzen}-System for {CTL}",
	institution = "LIFIA-IMAG",
	year = 1991,
	type = RR,
	number = "865-I",
	month = nov,
	address = "Grenoble"
	}

@article{fitting,
	author = "M. C. Fitting",
	title = "Many-Valued Modal Logics"
	journal = "Fundamenta Informaticae",
	year = 1991,
	volume = 15
	}

@inproceedings{paech88,
	author = "B. Paech",
	title = "{Gentzen}-Systems for Propositional Temporal Logics",
	booktitle = lncs385,
	year = 1988,
	pages = "240--253",
	publisher = SV,
	month = oct
	}

@techreport{paech88b,
	author = "B. Paech",
	title = "{Gentzen}-Systems for Propositional Temporal Logics",
	institution = "Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen,
		 Institut f{\"u}r Informatik",
	year = 1988,
	type = RR,
	number = "88/01",
	address = "Theresientr.39, D-8000 M{\"u}nchen 2, West-Germany",
	month = feb
	}

--

While it may not be exactly what you're after, there is an
interesting article by Bruce Kapron in the Journal of
Symbolic Logic, JSL 52:3, pp.756--762 entitled 
``Modal Sequents and Definability.''

--

Chapter 8 of ``Foundations of Mathematical Logic'' by H. B. Curry
(McGraw-Hill, 1963; Dover, 1977 and 1984) gives such a
presentation for S4.  It includes a survey of the literature up
to 1963.  The presentation is revised in his later paper ``A
Deduction Theorem for Inferential Predicate Calculus'', in
``Contributions to Mathematical Logic'', ed. K. Schuette
(North-Holland, Amsterdam, 1968), pp. 91-108.

Some additional references I have seen (but not all of which I
have checked myself, and which include natural deduction
formulations, which are clearly related) are as follows:

Robert W. Beard, ``A natural deduction variant of systems T, S4,
S5, and the Bowerian System'', Logique et Analyse (ns) 16 (1973)
311-314.

Denise Becchio, ``Calcul des sequents ed deduction naturelle pour
la logique trivalente de Lukasiewicz'', Ann. Sci. Univ. clermont,
Set. Math. 13 (1976) 55-73.

Nuel D. Belnap, Jr., Anil Gupta, and J. Michael Dunn, ``A
consecutive calculus for positive relevant implication with
necessity'', J. Philos. Logic 9 (1980) 343-362.

Kosta Dosen, ``Higher-level sequent-systems for intuitionistic
modal logic'' (Abstract), JSL 52 (1987) 1088.

Kosta Dosen, ``Sequent-systems for modal logic'', JSL 50 (1985)
149-168.  (Abstract:  JSL 49 (1984) 689.)

F. B. Fitch, ``Natural deduction rules for obligation'', Am.
Phil. Quarterly 3 (1966) 27-38.

Louis F. Goble, ``Gentzen systems for modal logic'', Notre Dame
J. Formal Logic 15 (1974) 455-461.

Hubert J. Marraud Gonzalez, ``Analytic tableau calculi and
natural deduction for prositional modal systems using subindexed
formulas'' (Abstract), JSL 52 (1987) 330-331.

G. E. Minc, ``On some calculi of modal logic'', in ``The Calculi
of Symbolic Logic, I:  Proceedings of the Steklov Institute of
Mathematics 98, 1968'', ed. V. P. Orevkov (AMS, Providence,
1971), pp. 97-124.

Hirokazu Nishimura, ``Hauptsatz for higher-order modal logic'',
JSL 48 (1983) 744-751.

Masao Ohnishi and Kazuo Matsumoto, ``A system for strict
implication'', Ann. Japan. Assoc. Phil. Sci. 2 (1964) 183-188.

Garrel Pottinger, ``Uniform cut-free formulations of T, S4, and
S5'' (Abstract), JSL 48 (1983) 900.

O. A. Robinson, ``a modal natural deduction system for S4'',
Notre Dame J. Formal Logic 20 (1979) 625-627.

Masahiko Sato, ``A cut-free Gentzen-type system for the modal
logic of S5'', JSL 45 (1980) 67-84.

Bangs L. Tapscott, ``A simplified natural deduction approach to
certain modal systems'', Notre Dame J. Formal Logic 28 (1987)
371-384.  (Abstract:  JSL 50 (1985) 284)

Silvio Valentini, ``A sequent calculus for the modal logic of
provability'' (Abstract), JSL 49 (1984) 707-708.

Atsuko Yamamoto, ``Cut-elimination theorem for multi-modal
logics'', J. Tsuda College 10 (1978) 21-34.

--

See: M.R.F. Benevides and T.S.E. Maibaum "A contructive presentation for
     the modal connective of necessity" in: Journal of Logic and computation
     Vol 2, Nr 1, March 1992, Oxford univerity press.

--

I think that the book by Chellas (AUTHOR: Chellas, Brian
F., TITLE: Modal logic : an introduction / Brian F. Chellas, IMPRINT:
Cambridge Cambridge University Press 1980) presents sequent systems.
There is also a small section in Hughes and Cresswell on natural
deduction. And of course Prawitz' book on Proof Theory presents various
natural deduction systems for s4 and s5. (I am assuming that natural
deduction presentations are close enough to sequent calculi to be of
use.) 

--

1) M. Sato, A study of Kripke-type model
for some modal logics by Gentzen's Sequential Methods,
Publ. RIMS, Kyoto Univ. 13, (1977) pg 381-468
(this is referenced in Wallen's book)

2) Kurt Schutte's old paper on Proof Theory for Modal
and Intuitionistic Logic (1960 ish)

3) A more recent paper by Wijesekra on Constructive
Modal Logics , appeared in Annals of Pure & Applied
Logic, 1990

4) Stig Kanger's old thesis (Provability in Logic) (1957)

5) Kosta Dosen, Sequent-Systems for modal logics, JSL, 1985
(His uses two level sequences to distinguish between S4 and S5
, if I understand it correctly. The method is highly 
original but the paper is quite hard to understand.) 

With regard to recent approach to Natural Deduction style
presentation for Modal logic, try:

  M Benevides and T Maibaum 's paper in J. of Logic & Computation 1991

Some Dana Scott's old papers "On engendering ...."
and "Rules and Derived Rules' discuss some problems 
in Gentzen presenation of Modal Logic too.

--

@techreport{gore-phd-tech,
AUTHOR = "Rajeev Gor{\'e}",
TITLE= "Cut-free sequent and tableau systems for propositional normal modal
logics",
SCHOOL = "Computer Laboratory",
INSTITUTION = "University of Cambridge, England",
NUMBER = "257",
YEAR = "May, 1992"
}

Abstract:

We present a unified treatment of tableau, sequent and axiomatic
formulations for many propositional normal modal logics, thus unifying and
extending the work of Hanson, Segerberg, Zeman, Mints, Fitting, Rautenberg
and Shvarts. The primary emphasis is on tableau systems as the completeness
proofs are easier in this setting. Each tableau system has a natural
sequent analogue defining a finitary provability relation for
each axiomatically formulated logic L. Consequently, any tableau proof
can be converted into a sequent proof which can be read downwards to obtain
an axiomatic proof. In particular, we present cut-free sequent systems for
the logics S4.3, S4.3.1 and S4.14. These three logics have
important temporal interpretations and the sequent systems appear to be
new.

All systems are sound and (weakly) complete with respect to their known
finite frame Kripke semantics.  By concentrating almost exclusively
on finite tree frames we obtain finer characterisation results,
particularly for the logics with natural temporal interpretations.  
In particular, all proofs of tableau completeness are constructive.

Most of these systems are cut-free giving a Gentzen cut-elimination theorem
for the logic in question. But even when the cut rule is required, all uses
of it remain analytic. Some systems do not possess the subformula property.
But in all such cases, the class of ``superformulae'' remains bounded,
giving an analytic superformula property. Thus, all systems remain totally
amenable to computer implementation and immediately serve as
nondeterministic decision procedures for the logics they formulate.
Furthermore, the constructive completeness proofs yield deterministic
decision procedures for all the logics concerned.

In obtaining these systems, we demonstrate that the subformula property can
be broken in a systematic and analytic way while still retaining
decidability. This should not be surprising since it is known that modal
logic is a form of second order logic and that the subformula property does
not hold for higher order logics.

--

Koen Versmissen, OTS, RU Utrecht, Trans 10, 3512 JK  Utrecht, NL
E-mail: Koen.Versmissen@let.ruu.nl..........Tel: (+31) 30-536057