
Authors:
Yuichi KOMORI
Title:λρCalculus: A Natural Deduction for Classical Logic
Pages:6570
File:bibtex
Abstract ( + )
In this note, we will pose a new system, named λρcalculus. While the type assignment system TAλ gives a natural deduction for intuitionistic implicational logic, the type assignment system TAλρ gives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem α there exists a proof of α in TAλρ enjoying the subformula property. Ryo Kashima has posed a natural deduction system for the classical implicational logic. His system has three rules, the elimination of the implication, the introduction of the implication and the case rule. The author noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system TAμ from Kashima's system by replacing the introduction of implication by the weakening. Then we have discovered the λρcalculus, introduced in the present paper.

Authors:
Bakhadyr KHOUSSAINOV
Title:On Some Games Played on Finite Graphs
Pages:7179
File:bibtex
Abstract ( + )
Our aim is to study reactive finite state systems (e.g., communication networks, banking systems) by means of gametheoretic methods. A reactive system acts upon the inputs from environment by changing its states. The goal of the system is to satisfy given specifications no matter how environment behaves. Informally, an interaction between the system and environment (which is assumed to be a finite state system) is a sequence, called "run", π = s0, a0, s1, a1, ... of states of the system and the environment. The success of the run depends upon whether or not the system satisfies a given specification. Since both systems are finite, some states in the run appear infinitely often. Denote the set of these states by Inf(π). An idea suggested by this observation is that specifications can be expressed in terms of sets Inf(π). The run π = s0, a0, s1, a1, ... can be thought as a play between two players, Survivor and Adversary. Survivor moves to ai from si, and Adversary responds by moving to s(i+1) from ai for i belons to ω. The goal of Survivor is to satisfy the specification given while the goal of Adversary is not to allow the specification to be satisfied. The definition below, given by McNaughton, formalizes these considerations.

Authors:
Motohiko MOURI
Title:Constructing CounterModels for Modal Logic K4 from Refutation Trees
Pages:8190
File:bibtex
Abstract ( + )
Logic K4 from Refutation Trees In the present paper, we will introduce a system which gives an efficient way of constructing countermodels for arbitrary formulae which are unprovable in modal logic K4. Our system is obtained by modifying the method in [7], which gives us an efficient decision procedure for K4. Therefore, as a whole, our system can decide first whether a given formula A is provable in K4 or not, and then gives us a countermodel for A when it is not provable. Since our system can avoid loopchecking as far as possible, the above procedure can be carried out efficiently.

Authors:
Katsumi SASAKI
Title:On Sequent Systems for Bimodal Provability Logics MOS and PRL1
Pages:91101
File:bibtex
Abstract ( + )
Provability Logics MOS and PRL1 We treat two bimodal provability logics MOS and PRL1 described by Smory\'{n}ski. We give cutfree sequent systems for these two logics by modifying a system of Avron for unimodal provability logic GL.

Authors:
Yasusi HASIMOTO
Title:Products of Infinitely Many Modal Logics
Pages:103110
File:bibtex
Abstract ( + )
In this paper, we will consider products of infinitely many modal logics, whose definition is based on the standard way of introducing ``products'' in probability theory and topology. For extensions of logic D, our products of modal logics can be defined either by means of {\em normal products of general frames} or by means of normal products of modal algebras}. It also enables us to develop a duality theory between these two.

Authors:
Tatsuya SHIMURA
Title:Kripke Incompleteness of Predicate Extentions of GabbaydeJongh's Logic of the Finite binary trees
Pages:111118
File:bibtex
Abstract ( + )
Extentions of GabbaydeJongh's Logic of the Finite binary trees In the previous papers, the author gave several completeness and incompleteness results on some predicate extensions with the constant domain of intermediate and modal propositional logics by means of the theory of canonical formulas. However, these results are on subframe and cofinal subframe logics, and little is known for non cofinal subframe logics. In this note, we show the Kripke incompleteness of the intermediate predicate logic H*+Tr2+K+D, where Tr is the axiom of GabbaydeJongh's logic of the finite binary trees.