On an Intuitionistic Modal Logic

被引:58
|
作者
G. M. Bierman
V. C. V. de Paiva
机构
[1] University of Cambridge,Computer Laboratory
[2] University of Birmingham,School of Computer Science
关键词
intuitionistic logic; modal logic; proof theory; categorical models;
D O I
10.1023/A:1005291931660
中图分类号
学科分类号
摘要
In this paper we consider an intuitionistic variant of the modal logic S4 (which we call IS4). The novelty of this paper is that we place particular importance on the natural deduction formulation of IS4— our formulation has several important metatheoretic properties. In addition, we study models of IS4— not in the framework of Kirpke semantics, but in the more general framework of category theory. This allows not only a more abstract definition of a whole class of models but also a means of modelling proofs as well as provability.
引用
收藏
页码:383 / 416
页数:33
相关论文
共 50 条