Algebraic Kripke Sheaf Semantics for Non-Classical Predicate Logics

In so-called Kripke-type models, each sentence is assigned either to true or to false at each possible world. In this setting, every possible world has the two-valued Boolean algebra as the set of truth values. Instead, we take a collection of algebras each of which is attached to a world as the set of truth values at the world, and obtain an extended semantics based on the traditional Kripke-type semantics, which we call here the algebraic Kripke semantics. We introduce algebraic Kripke sheaf semantics for super-intuitionistic and modal predicate logics, and discuss some basic properties. We can state the Gödel-McKinsey-Tarski translation theorem within this semantics. Further, we show new results on super-intuitionistic predicate logics. We prove that there exists a continuum of super-intuitionistic predicate logics each of which has both of the disjunction and existence properties and moreover the same propositional fragment as the intuitionistic logic.     

Predicate Logical Extensions of some Subintuitionistic Logics

The paper presents predicate logical extensions of some subintuitionistic logics. Subintuitionistic logics result if conditions of the accessibility relation in Kripke models for intuitionistic logic are dropped. The accessibility relation which interprets implication in models for the propositional base subintuitionistic logic considered here is neither persistent on atoms, nor reflexive, nor transitive. Strongly complete predicate logical extensions are modeled with a second accessibility relation, which is a partial order, for the interpretation of the universal quantifier. Presented by Melvin Fitting     

Relational semantics for full linear logic

Relational semantics, given by Kripke frames, play an essential role in the study of modal and intuitionistic logic. In [4] it is shown that the theory of relational semantics is also available in the more general setting of substructural logic, at least in an algebraic guise. Building on these ideas, in [5] a type of frames is described which generalise Kripke frames and provide semantics for substructural logics in a purely relational form.In this paper we study full linear logic from an algebraic point of view. The main additional hurdle is the exponential. We analyse this operation algebraically and use canonical extensions to obtain relational semantics. Thus, we extend the work in [4], [5] and use their approach to obtain relational semantics for full linear logic. Hereby we illustrate the strength of using canonical extension to retrieve relational semantics: it allows a modular and uniform treatment of additional operations and axioms.Traditionally, so-called phase semantics are used as models for (provability in) linear logic [8]. These have the drawback that, contrary to our approach, they do not allow a modular treatment of additional axioms. However, the two approaches are related, as we will explain.     

All Finitely Axiomatizable Tense Logics of Linear Time Flows Are CoNP-complete

We prove that all finitely axiomatizable tense logics with temporal operators for ‘always in the future’ and ‘always in the past’ and determined by linear fows time are coNP-complete. It follows, for example, that all tense logics containing a density axiom of the form ■ⁿ⁺¹_F p → ⁿ_F p, for some n ≥ 0, are coNP-complete. Additionally, we prove coNP-completeness of all ∩-irreducible tense logics. As these classes of tense logics contain many Kripke incomplete bimodal logics, we obtain many natural examples of Kripke incomplete normal bimodal logics which are nevertheless coNP-complete.     

On the Predicate Logic of Linear Kripke Frames and some of its Extensions

We propose a new, rather simple and short proof of Kripke-completeness for the predicate variant of Dummett's logic. Also a family of Kripke-incomplete extensions of this logic that are complete w.r.t. Kripke frames with equality (or equivalently, w.r.t. Kripke sheaves [8]), is described.     

Standard Gödel Modal Logics

We prove strong completeness of the □-version and the ?-version of a Gödel modal logic based on Kripke models where propositions at each world and the accessibility relation are both infinitely valued in the standard Gödel algebra [0,1]. Some asymmetries are revealed: validity in the first logic is reducible to the class of frames having two-valued accessibility relation and this logic does not enjoy the finite model property, while validity in the second logic requires truly fuzzy accessibility relations and this logic has the finite model property. Analogues of the classical modal systems D, T, S4 and S5 are considered also, and the completeness results are extended to languages enriched with a discrete well ordered set of truth constants.     

The Power of a Propositional Constant

Monomodal logic has exactly two maximally normal logics, which are also the only quasi-normal logics that are Post complete, and they are complete for validity in Kripke frames. Here we show that addition of a propositional constant to monomodal logic allows the construction of continuum many maximally normal logics that are not valid in any Kripke frame, or even in any complete modal algebra. We also construct continuum many quasi-normal Post complete logics that are not normal. The set of extensions of S4.3 is radically altered by the addition of a constant: we use it to construct continuum many such normal extensions of S4.3, and continuum many non-normal ones, none of which have the finite model property. But for logics with weakly transitive frames there are only eight maximally normal ones, of which five extend K4 and three extend S4.     

Normal Modal Substructural Logics with Strong Negation

We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.     

Logics of public communications

Multi-modal versions of propositional logics S5 or S4—commonly accepted as logics of knowledge—are capable of describing static states of knowledge but they do not reflect how the knowledge changes after communications among agents. In the present paper (part of broader research on logics of knowledge and communications) we define extensions of the logic S5 which can deal with public communications. The logics have natural semantics. We prove some completeness, decidability and interpretability results and formulate a general method that solves certain kind of problems involving public communications—among them well known puzzles of Muddy Children and Mr. Sum & Mr. Product. As the paper gives a formal logical treatment of the operation of restriction of the universe of a Kripke model, it contributes also to investigations of semantics for modal logics. This paper was originally published as Plaza, J. A. (1989). Logics of public communications. In M. L. Emrich, M. S. Pfeifer, M. Hadzikadic, & Z.W. Ras (Eds.), Proceedings of the fourth international symposium on methodologies for intelligent systems: Poster session program (pp. 201–216). Publisher: Oak Ridge National Laboratory, ORNL/DSRD-24. Research partly supported by NSF Grant CCR-8702307 and PSC-CUNY Grant 668283.     

On Logics with Coimplication

This paper investigates (modal) extensions of Heyting–Brouwer logic, i.e., the logic which results when the dual of implication (alias coimplication) is added to the language of intuitionistic logic. We first develop matrix as well as Kripke style semantics for those logics. Then, by extending the Gödel-embedding of intuitionistic logic into S4 , it is shown that all (modal) extensions of Heyting–Brouwer logic can be embedded into tense logics (with additional modal operators). An extension of the Blok–Esakia-Theorem is proved for this embedding.     

A First Order Nonmonotonic Extension of Constructive Logic

Certain extensions of Nelson's constructive logic N with strong negation have recently become important in arti.cial intelligence and nonmonotonic reasoning, since they yield a logical foundation for answer set programming (ASP). In this paper we look at some extensions of Nelson's .rst-order logic as a basis for de.ning nonmonotonic inference relations that underlie the answer set programming semantics. The extensions we consider are those based on 2-element, here-and-there Kripke frames. In particular, we prove completeness for .rst-order here-and-there logics, and their minimal strong negation extensions, for both constant and varying domains. We choose the constant domain version, which we denote by QN^c₅, as a basis for de.ning a .rst-order nonmonotonic extension called equilibrium logic. We establish several metatheoretic properties of QN^c₅, including Skolem forms and Herbrand theorems and Interpolation, and show that the .rst-oder version of equilibrium logic can be used as a foundation for answer set inference.     

A Map of Common Knowledge Logics

In order to capture the concept of common knowledge, various extensions of multi-modal epistemic logics, such as fixed-point ones and infinitary ones, have been proposed. Although we have now a good list of such proposed extensions, the relationships among them are still unclear. The purpose of this paper is to draw a map showing the relationships among them. In the propositional case, these extensions turn out to be all Kripke complete and can be comparable in a meaningful manner. F. Wolter showed that the predicate extension of the Halpern-Moses fixed-point type common knowledge logic is Kripke incomplete. However, if we go further to an infinitary extension, Kripke completeness would be recovered. Thus there is some gap in the predicate case. In drawing the map, we focus on what is happening around the gap in the predicate case. The map enables us to better understand the common knowledge logics as a whole.     

Making Things Happen

We explore some logics of change, focusing on commands to change the world in such a way that certain elementary propositions become true or false. This investigation starts out from the following two simplifying assumptions: (1) the world is a collection of facts (Wittgenstein), and (2), the world can be changed by changing elementary facts (Marx). These assumptions allow us to study the logic of imperatives in the simplest possible setting.     

Fibred Security Language

We study access control policies based on the says operator by introducing a logical framework called Fibred Security Language (FSL) which is able to deal with features like joint responsibility between sets of principals and to identify them by means of first-order formulas. FSL is based on a multimodal logic methodology. We first discuss the main contributions from the expressiveness point of view, we give semantics for the language both for classical and intuitionistic fragment), we then prove that in order to express well-known properties like ‘speaks-for’ or ‘hand-off’, defined in terms of says, we do not need second-order logic (unlike previous approaches) but a decidable fragment of first-order logic suffices. We propose a model-driven study of the says axiomatization by constraining the Kripke models in order to respect desirable security properties, we study how existing access control logics can be translated into FSL and we give completeness for the logic.     

现代本质主义的逻辑基础与哲学意蕴

<正>现代分析哲学家致力于意义的分析,力图通过对语言的分析使哲学科学化。以罗素和逻辑实证主义为代表的前期分析哲学家拒斥一切形而上学,所有导致本质主义的学说均被他们宣布为虚妄。但到     

Tableaus for many-valued modal logic

We continue a series of papers on a family of many-valued modal logics, a family whose Kripke semantics involves many-valued accessibility relations. Earlier papers in the series presented a motivation in terms of a multiple-expert semantics. They also proved completeness of sequent calculus formulations for the logics, formulations using a cut rule in an essential way. In this paper a novel cut-free tableau formulation is presented, and its completeness is proved.Research partly supported by NSF Grant CCR-9104015.     

Pure Extensions, Proof Rules, and Hybrid Axiomatics

In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity).We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic.A preliminary version of this paper was presented at the fifth conference on Advances in Modal Logic (AiML 2004) in Manchester. We would like to thank Maarten Marx for his comments on an early draft and Agnieszka Kisielewska for help with the proof reading.Special Issue Ways of Worlds II. On Possible Worlds and Related Notions Edited by Vincent F. Hendricks and Stig Andur Pedersen     

Subjective Situations and Logical Omniscience

The beliefs of the agents in a multi-agent system have been formally modelled in the last decades using doxastic logics. The possible worlds model and its associated Kripke semantics provide an intuitive semantics for these logics, but they commit us to model agents that are logically omniscient. We propose a way of avoiding this problem, using a new kind of entities called subjective situations. We define a new doxastic logic based on these entities and we show how the belief operators have some desirable properties, while avoiding logical omniscience. A comparison with two well-known proposals (Levesque's logic of explicit and implicit beliefs and Thijsse's hybrid sieve systems) is also provided.