Kripke‐style semantics for many‐valued logics

This paper deals with Kripke‐style semantics for many‐valued logics. We introduce various types of Kripke semantics, and we connect them with algebraic semantics. As for modal logics, we relate the axioms of logics extending MTL to properties of the Kripke frames in which they are valid. We show that in the propositional case most logics are complete but not strongly complete with respect to the corresponding class of complete Kripke frames, whereas in the predicate case there are important many‐valued logics like BL, ? and Π, which are not even complete with respect to the class of all predicate Kripke frames in which they are valid. Thus although very natural, Kripke semantics seems to be slightly less powerful than algebraic semantics. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

All finitely axiomatizable subframe logics containing the provability logic CSM_{0} are decidable

In this paper we investigate those extensions of the bimodal provability logic (alias or which are subframe logics, i.e. whose general frames are closed under a certain type of substructures. Most bimodal provability logics are in this class. The main result states that all finitely axiomatizable subframe logics containing are decidable. We note that, as a rule, interesting systems in this class do not have the finite model property and are not even complete with respect to Kripke semantics. Received July 15, 1997     

Polymodal Lattices and Polymodal Logic

A polymodal lattice is a distributive lattice carrying an n-place operator preserving top elements and certain finite meets. After exploring some of the basic properties of such structures, we investigate their freely generated instances and apply the results to the corresponding logical systems — polymodal logics — which constitute natural generalizations of the usual systems of modal logic familiar from the literature. We conclude by formulating an extension of Kripke semantics to classical polymodal logic and proving soundness and completeness theorems. Mathematics Subject Classification: 03G10, 06D99, 03B45.     

On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics.     

CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT

The aim of this paper is to extend the semantic analysis of tense logic in Rescher/Urquhart [3] to propositional dynamic logic without*. For this we develop a nested sequential calculus whose axioms and rules directly reflect the steps in the semantic analysis. It is shown that this calculus, with the cut rule omitted, is complete with respect to the standard semantics. It follows that cut elimination does hold for this nested sequential calculus. MSC: 03B45.     

La connaissance commune en logique modale

The problem of Common Knowledge will be considered in two classes of models: a class K.* of Kripke models and a class S of Scott models. Two modal logic systems will be defined. Those systems, KC and MC, include an axiomatisation of Common Knowledge. We prove determination of each system by the corresponding class of models. MSC: 03B45, 68T25.     

Über Deformationen von analytischen Abbildungskeimen

The notion of deformations of germs of k-analytic mappings generalizes the one of deformations of germs of k-analytic spaces. Using algebraic terms, we prove:

1. The morphism f: A→B of analytic algebras is rigid, iff it is infinitesimally rigid. Moreover, this is equivalent to Ex_A (B,B)=0. This theorem generalizes a result of SCHUSTER [11].
2. Let A be a regular analytic algebra. Then f is rigid iff there exists a rigid analytic algebra B_o such that f is equivalent to the canonic injection A→A?B_o.
3. If f is “almost everywhere” rigid or smooth, then the injection Ext _B ^l (Ω_B|A, Bⁿ)→Ex_A(B, Bⁿ) is an isomorphism.

     

Modal Multilattice Logic

A modal extension of multilattice logic, called modal multilattice logic, is introduced as a Gentzen-type sequent calculus \(\hbox {MML}_n\). Theorems for embedding \(\hbox {MML}_n\) into a Gentzen-type sequent calculus S4C (an extended S4-modal logic) and vice versa are proved. The cut-elimination theorem for \(\hbox {MML}_n\) is shown. A Kripke semantics for \(\hbox {MML}_n\) is introduced, and the completeness theorem with respect to this semantics is proved. Moreover, the duality principle is proved as a characteristic property of \(\hbox {MML}_n\).     

Topological completeness of the provability logic GLP

Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of GLP. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.     

A secondary semantics for Second Order Intuitionistic Propositional Logic

In this paper we propose a Kripke‐style semantics for second order intuitionistic propositional logic and we provide a semantical proof of the disjunction and the explicit definability property. Moreover, we provide a tableau calculus which is sound and complete with respect to such a semantics. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Modal Extensions of Sub-classical Logics for Recovering Classical Logic

In this paper we introduce non-normal modal extensions of the sub-classical logics CLoN, CluN and CLaN, in the same way that S0.5 ⁰ extends classical logic. The first modal system is both paraconsistent and paracomplete, while the second one is paraconsistent and the third is paracomplete. Despite being non-normal, these systems are sound and complete for a suitable Kripke semantics. We also show that these systems are appropriate for interpreting □ as “is provable in classical logic”. This allows us to recover the theorems of propositional classical logic within three sub-classical modal systems.     

Incompleteness Results in Kripke Bundle Semantics

Kripke bundle and C-set semantics are known as semantics which generalize standard Kripke semantics. In [4] and in [1, 2] it is shown that Kripke bundle and C-set semantics are stronger than standard Kripke semantics. Also it is true that C-set semantics for superintuitionistic logics is stronger than Kripke bundle semantics ([6]). Modal predicate logic Q-S4.1 is not Kripke bundle complete ([3] - it is also yielded as a corollary to Theorem 6.1(a) of the present paper). This is shown by using difference of Kripke bundle semantics and C-set semantics. In this paper, by using the same idea we show that incompleteness results in Kripke bundle semantics which are extended versions of [2].     

ŁΠ logic with fixed points

We study a system, μ?Π, obtained by an expansion of ?Π logic with fixed points connectives. The first main result of the paper is that μ?Π is standard complete, i.e., complete with regard to the unit interval of real numbers endowed with a suitable structure. We also prove that the class of algebras which forms algebraic semantics for this logic is generated, as a variety, by its linearly ordered members and that they are precisely the interval algebras of real closed fields. This correspondence is extended to a categorical equivalence between the whole category of those algebras and another category naturally arising from real closed fields. Finally, we show that this logic enjoys implicative interpolation.     

Decidability results in non-classical logic. III

A Kripke type semantics is given to a large class of tense logics with statability operators (including PriorsQK _t) in such a manner as to obtain their decidability using Rabin’s theorem. Dedicated to the Memory of A. N. Prior     

A spatial modal logic with a location interpretation

A spatial modal logic (SML) is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space (or location) interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut‐elimination theorem for a modified subsystem of SML are also presented. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The logical consequence relation of propositional tense logic

This work concerns the model theory of propositional tense logic with the Kripke relational semantics. It is shown (i) that there is a formula y whose logical consequences form a complete II set, and (ii) that for 0 ≦ m < ω+ ω there are formulas γ_m such that all models of γ_m are isomorphic and have cardinality x_m, where x₀ = χ₀, x_m+1 = 2^xm, and x_ω = lim{x_m < | m ω}. Familiarity with the relational semantics for modal and tense logic ([1] or [3], for example) will be presumed. A knowledge of recursion theory would be helpful, although some background material will be provided.     

Exhibiting Wide Families of Maximal Intermediate Propositional Logics with the Disjunction Property

We provide results allowing to state, by the simple inspection of suitable classes of posets (propositional Kripke frames), that the corresponding intermediate propositional logics are maximal among the ones which satisfy the disjunction property. Starting from these results, we directly exhibit, without using the axiom of choice, the Kripke frames semantics of 2^No maximal intermediate propositional logics with the disjunction property. This improves previous evaluations, giving rise to the same conclusion but made with an essential use of the axiom of choice, of the cardinality of the set of the maximal intermediate propositional logics with the disjunction property. Mathematics Subject Classification: 03B55, 03C90.     

Forcing operators on MTL‐algebras

We study the forcing operators on MTL‐algebras, an algebraic notion inspired by the Kripke semantics of the monoidal t ‐norm based logic (MTL). At logical level, they provide the notion of the forcing value of an MTL‐formula. We characterize the forcing operators in terms of some MTL‐algebras morphisms. From this result we derive the equality of the forcing value and the truth value of an MTL‐formula (© 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

L-algebras and three main non-classical logics

The semantics of three main branches of non-classical logic, intuitionistic, many-valued, and quantum logic, is unified by the concept of L-algebra. The corresponding three classes of algebras (Heyting algebras, MV-algebras, and orthomodular lattices) are associated to specializations of a bounded L-algebra, given by simple equations. Three basic specializations lead to three more classes of algebras, including quantized Heyting algebras which have not been considered before. All these algebras are obtained from a new class of L-algebras which simultaneously satisfy general versions of Glivenko's and Mundici's theorems.