On an Intuitionistic Modal Logic

被引：61
作者：
G. M. Bierman
V. C. V. de Paiva
机构：
[1] University of Cambridge,Computer Laboratory
[2] University of Birmingham,School of Computer Science
来源：
Studia Logica | 2000年 / 65卷 / 3期
关键词：
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
相关论文
共 15 条
[1]  
Benevides M.(1992)A constructive presentation for the modal connective of necessity Journal of Logic and Computation 2 31-50
[2]  
Maibaum T.(1998)Computational types from a logical perspective Journal of Functional Programming 8 177-193
[3]  
Benton P.N.(1995)Yet another intuitionistic modal logic (abstract) Bulletin of Symbolic Logic 1 226-265
[4]  
Bierman G.M.(1957)The elimination theorem when modality is present Journal of Symbolic Logic 17 249-339
[5]  
de Paiva V.C.V.(1993)Constructive logics part I: A tutorial on proof systems and typed Theoretical Computer Science 110 249-101
[6]  
Bierman G.M.(1987)-calculi Theoretical Computer Science 50 1-231
[7]  
de Paiva V.C.V.(1998)Linear logic Studia Logica 60 209-426
[8]  
Curry H.B.(1998)Linear lambda-terms and natural deduction Archive for Mathematical Logic 37 415-92
[9]  
Gallier J.(1991)Normal deduction in the intuitionistic linear logic Information and Control 93 55-475
[10]  
Girard J.-Y.(1972)Notions of computation and monads Notre Dame Journal of Formal Logic 8 461-347
12