## The Proof Theory and Semantics of Intuitionistic Modal
Logic

**Alex Simpson**
*Abstract:* Possible world semantics underlies many of the
applications of modal logic in computer science and philosophy. The
standard theory arises from interpreting the semantic definitions
in the ordinary meta-theory of informal classical mathematics. If,
however, the same semantic definitions are interpreted in an
intuitionistic meta-theory then the induced modal logics no longer
satisfy certain intuitionistically invalid principles. This thesis
investigates the *intuitionistic modal logics* that arise in
this way.

Natural deduction systems for various intuitionistic modal
logics are presented. From one point of view, these systems are
self-justifying in that a possible world interpretation of the
modalities can be read off directly from the inference rules. A
technical justification is given by the faithfulness of
translations into intuitionistic first-order logic. It is also
established that, in many cases, the natural deduction systems
induce well-known intuitionistic modal logics, previously given by
Hilbert-style axiomatizations.

The main benefit of the natural deduction systems over
axiomatizations is their susceptibility to proof-theoretic
techniques. Strong normalization (and confluence) results are
proved for all of the systems. Normalization is then used to
establish the completeness of cut-free sequent calculi for all of
the systems, and decidability for some of the systems.

Lastly, techniques developed throughout the thesis are used to
establish that those intuitionistic modal logics proved decidable
also satisfy the finite model property. For the logics considered,
decidability and the finite model property presented open
problems.

**PhD Thesis - Price £8.50**

This is a 210 page PhD thesis which is available as a DVI file (0.7Mb) and as a PostScript file (1.2Mb).

*LFCS report ECS-LFCS-94-308 (also published as CST-114-94),
August 1994.*

Previous |

Index |

Next