Logic Games are Complete for Game Logics

Game logics describe general games through powers of players for forcing outcomes. In particular, they encode an algebra of sequential game operations such as choice, dual and composition. Logic games are special games for specific purposes such as proof or semantical evaluation for first-order or modal languages. We show that the general algebra of game operations coincides with that over just logical evaluation games, whence the latter are quite general after all. The main tool in proving this is a representation of arbitrary games as modal or first-order evaluation games. We probe how far our analysis extends to product operations on games. We also discuss some more general consequences of this new perspective for standard logic.     

Game Logic - An Overview

Game Logic is a modal logic which extends Propositional Dynamic Logic by generalising its semantics and adding a new operator to the language. The logic can be used to reason about determined 2-player games. We present an overview of meta-theoretic results regarding this logic, also covering the algebraic version of the logic known as Game Algebra.     

On Fork Arrow Logic and its Expressive Power

We compare fork arrow logic, an extension of arrow logic, and its natural first-order counterpart (the correspondence language) and show that both have the same expressive power. Arrow logic is a modal logic for reasoning about arrow structures, its expressive power is limited to a bounded fragment of first-order logic. Fork arrow logic is obtained by adding to arrow logic the fork modality (related to parallelism and synchronization). As a result, fork arrow logic attains the expressive power of its first-order correspondence language, so both can express the same input–output behavior of processes.     

An n-Player Semantic Game for an n + 1-Valued Logic

First we show that the classical two-player semantic game actually corresponds to a three-valued logic. Then we generalize this result and give an n-player semantic game for an n + 1-valued logic with n binary connectives, each associated with a player. We prove that player i has a winning strategy in game if and only if the truth value of is t _i in the model M, for 1 ≤ i ≤ n; and none of the players has a winning strategy in if and only if the truth value of is t ₀ in M.     

Cooperation,Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as Alternating-time Temporal Logic (ATL). The key insight in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form , where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as group can cooperate to bring about iff it is common knowledge in that . The resulting logic — Alternating-time Temporal Epistemic Logic (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems.     

An Impossibility Theorem on Beliefs in Games

A paradox of self-reference in beliefs in games is identified, which yields a game-theoretic impossibility theorem akin to Russell’s Paradox. An informal version of the paradox is that the following configuration of beliefs is impossible:Ann believes that Bob assumes thatAnn believes that Bob’s assumption is wrongThis is formalized to show that any belief model of a certain kind must have a ‘hole.’ An interpretation of the result is that if the analyst’s tools are available to the players in a game, then there are statements that the players can think about but cannot assume. Connections are made to some questions in the foundations of game theory.Special Issue Ways of Worlds II. On Possible Worlds and Related Notions Edited by Vincent F. Hendricks and Stig Andur Pedersen     

The Basic Algebra of Game Equivalences

We give a complete axiomatization of the identities of the basic game algebra valid with respect to the abstract game board semantics. We also show that the additional conditions of termination and determinacy of game boards do not introduce new valid identities.En route we introduce a simple translation of game terms into plain modal logic and thus translate, while preserving validity both ways, game identities into modal formulae.The completeness proof is based on reduction of game terms to a certain minimal canonical form, by using only the axiomatic identities, and on showing that the equivalence of two minimal canonical terms can be established from these identities.     

Constructing Finite Least Kripke Models for Positive Logic Programs in Serial Regular Grammar Logics

A serial context-free grammar logic is a normal multimodal logicL characterized by the seriality axioms and a set of inclusionaxioms of the form _ts1..._sk. Such an inclusion axiom correspondsto the grammar rule t s₁... s_k. Thus the inclusion axioms ofL capture a context-free grammar . If for every modal index t, the set of words derivable fromt using is a regular language, then L is a serial regular grammar logic. In this paper, we present an algorithm that, given a positivemultimodal logic program P and a set of finite automata specifyinga serial regular grammar logic L, constructs a finite leastL-model of P. (A model M is less than or equal to model M' iffor every positive formula , if M then M' .) A least L-modelM of P has the property that for every positive formula , P iff M . The algorithm runs in exponential time and returnsa model with size 2^O(n³). We give examples of P and L, for bothof the case when L is fixed or P is fixed, such that every finiteleast L-model of P must have size 2⁽ⁿ⁾. We also prove that ifG is a context-free grammar and L is the serial grammar logiccorresponding to G then there exists a finite least L-modelof _s p iff the set of words derivable from s using G is a regularlanguage.     

Elementary Classes in Basic Modal Logic

Dealing with topics of definability, this paper provides some interesting insights into the expressive power of basic modal logic. After some preliminary work it presents an abstract algebraic characterization of the elementary classes of basic modal logic, that is, of the classes of models that are definable by means of (sets of) basic modal formulas. Taking that for a start, the paper further contains characterization results for modal universal classes and modal positive classes.     

Constructive Logic with Strong Negation is a Substructural Logic. I

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL _ew of the substructural logic FL _ew . In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL _ew (namely, a certain variety of FL _ew -algebras) are term equivalent. This answers a longstanding question of Nelson [30]. Extensive use is made of the automated theorem-prover Prover9 in order to establish the result. The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL _ew are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL _ew . Presented by Heinrich Wansing     

Some Embedding Theorems for Conditional Logic

We prove some embedding theorems for classical conditional logic, covering ‘finitely cumulative’ logics, ‘preferential’ logics and what we call ‘semi-monotonic’ logics. Technical tools called ‘partial frames’ and ‘frame morphisms’ in the context of neighborhood semantics are used in the proof.     

The Greatest Extension of S4 into which Intuitionistic Logic is Embeddable

This paper gives a characterization of those quasi-normal extensions of the modal system S4 into which intuitionistic propositional logic Int is embeddable by the Gödel translation. It is shown that, as in the normal case, the set of quasi-normal modal companions of Int contains the greatest logic, M*, for which, however, the analog of the Blok-Esakia theorem does not hold. M* is proved to be decidable and Halldén-complete; it has the disjunction property but does not have the finite model property.     

A Logic for Information Systems

A conception of an information system has been introduced by Pawlak. The study has been continued in works of Pawlak and Orlowska and in works of Vakarelov. They had proposed some basic relations and had constructed a formal system of a modal logic that describes the relations and some of their Boolean combinations. Our work is devoted to a generalization of this approach. A class of relation systems and a complete calculus construction method for these systems are proposed. As a corollary of our main result, our paper contains a solution of a Vakarelov's problem: how to construct a formal system that describes all the Boolean combinations of the basic relations.     

Supererogation in Deontic Logic: Metatheory for DWE and Some Close Neighbours

In "Doing Well Enough: Toward a Logic for Common Sense Morality", Paul McNamara sets out a semantics for a deontic logic which contains the operator It is supererogatory that. As well as having a binary accessibility relation on worlds, that semantics contains a relative ordering relation, . For worlds u, v and w, we say that u w v when v is at least as good as u according to the standards of w. In this paper we axiomatize logics complete over three versions of the semantics. We call the strongest of these logics DWE for Doing Well Enough.     

A Note on the Interpolation Property in Tense Logic

It is proved that all bimodal tense logics which contain the logic of the weak orderings and have unbounded depth do not have the interpolation property.     

Constructive Logic with Strong Negation is a Substructural Logic. II

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL _ew of the substructural logic FL _ew . The main result of Part I of this series [41] shows that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL _ew (namely, a certain variety of FL _ew -algebras) are term equivalent. In this paper, the term equivalence result of Part I [41] is lifted to the setting of deductive systems to establish the definitional equivalence of the logics N and NFL _ew . It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural logic. Presented by Heinrich Wansing     

Model Existence in Non-Compact Modal Logic

Predicate modal logics based on Kwith non-compact extra axioms are discussed and a sufficient condition for the model existence theorem is presented. We deal with various axioms in a general way by an algebraic method, instead of discussing concrete non-compact axioms one by one.     

Squares in Fork Arrow Logic

In this paper we show that the class of fork squares has a complete orthodox axiomatization in fork arrow logic (FAL). This result may be seen as an orthodox counterpart of Venema's non-orthodox axiomatization for the class of squares in arrow logic. FAL is the modal logic of fork algebras (FAs) just as arrow logic is the modal logic of relation algebras (RAs). FAs extend RAs by a binary fork operator and are axiomatized by adding three equations to RAs equational axiomatization. A proper FA is an algebra of relations where the fork is induced by an injective operation coding pair formation. In contrast to RAs, FAs are representable by proper ones and their equational theory has the expressive power of full first-order logic. A square semantics (the set of arrows is U×U for some set U) for arrow logic was defined by Y. Venema. Due to the negative results about the finite axiomatizability of representable RAs, Venema provided a non-orthodox finite axiomatization for arrow logic by adding a new rule governing the applications of a difference operator. We address here the question of extending the type of relational structures to define orthodox axiomatizations for the class of squares. Given the connections between this problem and the finitization problem addressed by I. Németi, we suspect that this cannot be done by using only logical operations. The modal version of the FA equations provides an orthodox axiomatization for FAL which is complete in view of the representability of FAs. Here we review this result and carry it further to prove that this orthodox axiomatization for FAL also axiomatizes the class of fork squares.     

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.