Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic modal logics

Shehtman and Skvortsov introduced Kripke bundles as semantics of non-classical first-order predicate logics. We show the structural equivalence between Kripke bundles for intermediate predicate logics and Kripke-type frames for intuitionistic modal prepositional logics. This equivalence enables us to develop the semantical study of relations between intermediate predicate logics and intuitionistic modal propositional logics. New examples of modal counterparts of intermediate predicate logics are given.The author would like to express his gratitude to Professor Hiroakira Ono for his comments, and to Professor Tadashi Kuroda for his encouragement.The author wishes to express his gratitude to Professors V. B. Shehtman, D. P. Skvortsov and M. Takano for their comments.     

An application of Rieger-Nishimura formulas to the intuitionistic modal logics

The main results of the paper are the following: For each monadic prepositional formula which is classically true but not intuitionistically so, there is a continuum of intuitionistic monotone modal logics L such that L+ is inconsistent.There exists a consistent intuitionistic monotone modal logic L such that for any formula of the kind mentioned above the logic L+ is inconsistent.There exist at least countably many maximal intuitionistic monotone modal logics.The author appreciates very much referees' suggestions which helped to improve the exposition.     

On maximal intermediate predicate constructive logics

We extend to the predicate frame a previous characterization of the maximal intermediate propositional constructive logics. This provides a technique to get maximal intermediate predicate constructive logics starting from suitable sets of classically valid predicate formulae we call maximal nonstandard predicate constructive logics. As an example of this technique, we exhibit two maximal intermediate predicate constructive logics, yet leaving open the problem of stating whether the two logics are distinct. Further properties of these logics will be also investigated.Presented by H. Ono     

Models for normal intuitionistic modal logics

Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given for analogues of the modal systemK based on Heyting's prepositional logic. It is shown that these two relations can combine with each other in various ways. Soundness and completeness are proved for systems with only the necessity operator, or only the possibility operator, or both. Embeddings in modal systems with several modal operators, based on classical propositional logic, are also considered. This paper lays the ground for an investigation of intuitionistic analogues of systems stronger thanK. A brief survey is given of the existing literature on intuitionistic modal logic.     

On finite linear intermediate predicate logics

An intermediate predicate logicS ₊ ⁿ (n>0) is introduced and investigated. First, a sequent calculusGS _n is introduced, which is shown to be equivalent toS ₊ ⁿ and for which the cut elimination theorem holds. In § 2, it will be shown thatS ₊ ⁿ is characterized by the class of all linear Kripke frames of the heightn.To the memory of the late Professor Iwao Nishimura     

Models for stronger normal intuitionistic modal logics

This paper, a sequel to Models for normal intuitionistic modal logics by M. Boi and the author, which dealt with intuitionistic analogues of the modal system K, deals similarly with intuitionistic analogues of systems stronger than K, and, in particular, analogues of S4 and S5. For these prepositional logics Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given, and soundness and completeness are proved with respect to these models. It is shown how the holding of formulae characteristic for particular logics is equivalent to conditions for the relations of the models. Modalities in these logics are also investigated.This paper presents results of an investigation of intuitionistic modal logic conducted in collaboration with Dr Milan Boi.     

A uniform tableau method for intuitionistic modal logics I

We present tableau systems and sequent calculi for the intuitionistic analoguesIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IKD5, IK45, IKD45 andIS5 of the normal classical modal logics. We provide soundness and completeness theorems with respect to the models of intuitionistic logic enriched by a modal accessibility relation, as proposed by G. Fischer Servi. We then show the disjunction property forIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IK45 andIS5. We also investigate the relationship of these logics with some other intuitionistic modal logics proposed in the literature.Work carried out in the framework of the agreement between the Italian PT Administration and the Fondazione Ugo Bordoni.Presented byDov Gabbay     

A general method for proving decidability of intuitionistic modal logics

We generalise the result of [H. Ganzinger, C. Meyer, M. Veanes, The two-variable guarded fragment with transitive relations, in: Proc. 14th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1999, pp. 24–34] on decidability of the two variable monadic guarded fragment of first order logic with constraints on the guard relations expressible in monadic second order logic. In [H. Ganzinger, C. Meyer, M. Veanes, The two-variable guarded fragment with transitive relations, in: Proc. 14th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1999, pp. 24–34], such constraints apply to one relation at a time. We modify their proof to obtain decidability for constraints involving several relations. Now we can use this result to prove decidability of multi-modal modal logics where conditions on accessibility relations involve more than one relation. Our main application is intuitionistic modal logic, where the intuitionistic and modal accessibility relations usually interact in a non-trivial way.     

On modal logic with an intuitionistic base

A definition of the concept of Intuitionist Modal Analogue is presented and motivated through the existence of a theorem preserving translation fromMIPC (see [2]) to a bimodalS ⁴–S⁵ calculus.Allatum est die 9 Septembris 1975     

Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas

For each intermediate propositional logicJ, J _* denotes the least predicate extension ofJ. By the method of canonical models, the strongly Kripke completeness ofJ _*+D(=x(p(x)q)xp(x)q) is shown in some cases including:

Intermediate logics with the same disjunctionless fragment as intuitionistic logic

Given an intermediate prepositional logic L, denote by L ^–d its disjuctionless fragment. We introduce an infinite sequence {J _n}_n1 of propositional formulas, and prove:(1)For any L: L ^–d =I ^–d (I=intuitionistic logic) if and only if J _n L for every n 1.Since it turns out that L{J _{n} n}1 = Ø for any L having the disjunction property, we obtain as a corollary that L ^–d = I ^–d for every L with d.p. (cf. open problem 7.19 of [5]). Algebraic semantic is used in the proof of the if part of (1). In the last section of the paper we provide a characterization in Kripke's semantic for the logics J _n =I+ +J _n (n 1).     

On detachment-substitutional formalization in normal modal logics

The aim of this paper is to propose a criterion of finite detachment-substitutional formalization for normal modal systems. The criterion will comprise only those normal modal systems which are finitely axiomatizable by means of the substitution, detachment for material implication and Gödel rules.Some results of this paper were announced in the abstract [2].Allatum est die 10 Junii 1976     

Amalgamation and interpolation in normal modal logics

This is a survey of results on interpolation in propositional normal modal logics. Interpolation properties of these logics are closely connected with amalgamation properties of varieties of modal algebras. Therefore, the results on interpolation are also reformulated in terms of amalgamation.     

Chang's modal operators in algebraic logic

Chang algebras as algebraic models for Chang's modal logics [1] are defined. The main result of the paper is a representation theorem for these algebras.     

Interpretations of intuitionist logic in non-normal modal logics

Historically, it was the interpretations of intuitionist logic in the modal logic S4 that inspired the standard Kripke semantics for intuitionist logic. The inspiration of this paper is the interpretation of intuitionist logic in the non-normal modal logic S3: an S3 model structure can be 'looked at' as an intuitionist model structure and the semantics for S3 can be 'cashed in' to obtain a non-normal semantics for intuitionist propositional logic. This non-normal semantics is then extended to intuitionist quantificational logic.