Graded modalities,II (canonical models)

This work intends to be a generalization and a simplification of the techniques employed in [2], by the proposal of a general strategy to prove satisfiability theorems for NLGM-s (= normal logics with graded modalities), analogously to the well known technique of the canonical models by Lemmon and Scott for classical modal logics.     

Computing with Cylindric Modal Logics and Arrow Logics,Lower Bounds

The complexity of the satisfiability problems of various arrow logics and cylindric modal logics is determined. As is well known, relativising these logics makes them decidable. There are several parameters that can be set in such a relativisation. We focus on the following three: the number of variables involved, the similarity type and the kind of relativised models considered. The complexity analysis shows the importance and relevance of these parameters.     

The Undecidability of Quantified Announcements

This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents (this group may be a proper subset of the set of all agents) all of which are simultaneously (and publicly) making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that group may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics.     

The complexity of satisfiability for fragments of hybrid logic—Part I

The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments.In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments including negation. For the monotone fragments, we are able to distinguish the easy from the hard cases, depending on the allowed set of operators.     

Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)

We present a coinductive definition of models for modal logics and show that it provides a homogeneous framework in which it is possible to include different modal languages ranging from classical modalities to operators from hybrid and memory logics. Moreover, results that had to be proved separately for each different language—but whose proofs were known to be mere routine—now can be proved in a general way. We show, for example, that we can have a unique definition of bisimulation for all these languages, and prove a single invariance-under-bisimulation theorem.We then use the new framework to investigate normal forms for modal logics. The normal form we introduce may have a smaller modal depth than the original formula, and it is inspired by global modalities like the universal modality and the satisfiability operator from hybrid logics. These modalities can be extracted from under the scope of other operators. We provide a general definition of extractable modalities and show how to compute extracted normal forms. As it is the case with other classical normal forms—e.g., the conjunctive normal form of propositional logic—the extracted normal form of a formula can be exponentially bigger than the original formula, if we require the two formulas to be equivalent. If we only require equi-satisfiability, then every modal formula has an extracted normal form which is only polynomially bigger than the original formula, and it can be computed in polynomial time.     

Substructural logics,pluralism and collapse

When discussing Logical Pluralism several critics argue that such an open-minded position is untenable. The key to this conclusion is that, given a number of widely accepted assumptions, the pluralist view collapses into Logical Monism. In this paper we show that the arguments usually employed to arrive at this conclusion do not work. The main reason for this is the existence of certain substructural logics which have the same set of valid inferences as Classical Logic—although they are, in a clear sense, non-identical to it. We argue that this phenomenon can be generalized, given the existence of logics which coincide with Classical Logic regarding a number of metainferential levels—although they are, again, clearly different systems. We claim this highlights the need to arrive at a more refined version of the Collapse Argument, which we discuss at the end of the paper.

     

Selfextensional Logics with a Conjunction

A logic is selfextensional if its interderivability (or mutual consequence) relation is a congruence relation on the algebra of formulas. In the paper we characterize the selfextensional logics with a conjunction as the logics that can be defined using the semilattice order induced by the interpretation of the conjunction in the algebras of their algebraic counterpart. Using the charactrization we provide simpler proofs of several results on selfextensional logics with a conjunction obtained in [13] using Gentzen systems. We also obtain some results on Fregean logics with conjunction.This paper is a version of the invited talk at the conference Trends in Logic III, dedicated to the memory of A. MOSTOWSKI, H. RASIOWA and C. RRAUSZER, and held in Warsaw and Ruciane-Nida from 23rd to 25th September 2005.     

Quantified coalition logic

We add a limited but useful form of quantification to Coalition Logic, a popular formalism for reasoning about cooperation in game-like multi-agent systems. The basic constructs of Quantified Coalition Logic (QCL) allow us to express such properties as “every coalition satisfying property P can achieve φ” and “there exists a coalition C satisfying property P such that C can achieve φ”. We give an axiomatisation of QCL, and show that while it is no more expressive than Coalition Logic, it is nevertheless exponentially more succinct. The complexity of QCL model checking for symbolic and explicit state representations is shown to be no worse than that of Coalition Logic, and satisfiability for QCL is shown to be no worse than satisfiability for Coalition Logic. We illustrate the formalism by showing how to succinctly specify such social choice mechanisms as majority voting, which in Coalition Logic require specifications that are exponentially long in the number of agents.     

Intuitionistic Conditional Logics

Journal of Philosophical Logic - Building on recent work by Yale Weiss, we study conditional logics in the intuitionistic setting. We consider a number of semantic conditions which give rise, among...     

The Decision Problem of Modal Product Logics with a Diagonal,and Faulty Counter Machines

In the propositional modal (and algebraic) treatment of two-variable first-order logic equality is modelled by a ‘diagonal’ constant, interpreted in square products of universal frames as the identity (also known as the ‘diagonal’) relation. Here we study the decision problem of products of two arbitrary modal logics equipped with such a diagonal. As the presence or absence of equality in two-variable first-order logic does not influence the complexity of its satisfiability problem, one might expect that adding a diagonal to product logics in general is similarly harmless. We show that this is far from being the case, and there can be quite a big jump in complexity, even from decidable to the highly undecidable. Our undecidable logics can also be viewed as new fragments of first-order logic where adding equality changes a decidable fragment to undecidable. We prove our results by a novel application of counter machine problems. While our formalism apparently cannot force reliable counter machine computations directly, the presence of a unique diagonal in the models makes it possible to encode both lossy and insertion-error computations, for the same sequence of instructions. We show that, given such a pair of faulty computations, it is then possible to reconstruct a reliable run from them.     

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.     

Two notions of compactness in Gödel logics

Compactness is an important property of classical propositional logic. It can be defined in two equivalent ways. The first one states that simultaneous satisfiability of an infinite set of formulae is equivalent to the satisfiability of all its finite subsets. The second one states that if a set of formulae entails a formula, then there is a finite subset entailing this formula as well.In propositional many-valued logic, we have different degrees of satisfiability and different possible definitions of entailment, hence the questions of compactness is more complex. In this paper we will deal with compactness of Gödel, Gödel_Δ, and Gödel_～ logics.There are several results (all for the countable set of propositional variables) concerning the compactness (based on satisfiability) of these logic by Cintula and Navara, and the question of compactness (based on entailment) for Gödel logic was fully answered by Baaz and Zach (see papers [3] and [2]).In this paper we give a nearly complete answer to the problem of compactness based on both concepts for all three logics and for an arbitrary cardinality of the set of propositional variables. Finally, we show a tight correspondence between these two concepts     

Temporal logics for concurrent recursive programs: Satisfiability and model checking

We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and which, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.     

A logical formalization of the OCC theory of emotions

In this paper, we provide a logical formalization of the emotion triggering process and of its relationship with mental attitudes, as described in Ortony, Clore, and Collins’s theory. We argue that modal logics are particularly adapted to represent agents’ mental attitudes and to reason about them, and use a specific modal logic that we call Logic of Emotions in order to provide logical definitions of all but two of their 22 emotions. While these definitions may be subject to debate, we show that they allow to reason about emotions and to draw interesting conclusions from the theory.     

Two dimensional Standard Deontic Logic [including a detailed analysis of the 1985 Jones–P?rn deontic logic system]

This paper offers a two dimensional variation of Standard Deontic Logic SDL, which we call 2SDL. Using 2SDL we can show that we can overcome many of the difficulties that SDL has in representing linguistic sets of Contrary-to-Duties (known as paradoxes) including the Chisholm, Ross, Good Samaritan and Forrester paradoxes. We note that many dimensional logics have been around since 1947, and so 2SDL could have been presented already in the 1970s. Better late than never! As a detailed case study illustrating the power of 2SDL, we examine the system DL of Deontic Logic of Andrew Jones and Ingmar P?rn offered in 1985 to solve the Chisholm paradox of Contrary to Duties. The critical examination is done using logics and methods available in 1985 and solutions are proposed using what was available in 1985.     

Complexity Results of STIT Fragments

We provide a Kripke semantics for a STIT logic with the ??next?? operator. As the atemporal group STIT is undecidable and unaxiomatizable, we are interested in strict fragments of atemporal group STIT. First we prove that the satisfiability problem of a formula of the fragment made up of individual coalitions plus the grand coalition is also NEXPTIME-complete. We then generalize this result to a fragment where coalitions are in a given lattice. We also prove that if we restrict the language to nested coalitions the satisfiability problem is NP-complete if the number of agents is fixed and PSPACEcomplete if the number of agents is variable. Finally we embed individual STIT with the ??next?? operator into a fragment of atemporal group STIT.     

《逻辑学研究》征稿启事

《逻辑学研究》是中山大学和中国逻辑学会主办,由教育部高等院校人文社会科学重点研究基地中山大学逻辑与认知研究所承办的学术刊物,旨在积极推动我国逻辑学及相关学科的学术研究水平,增进海内外逻辑学及相关领域学术同行的交流。《逻辑学研究》是当前我国在逻辑学领域内唯一正式出版的专业刊物,采用中英双语发表论文。《逻辑学研究》目前为季刊,逢每季度第三个月的18日出版。自2011年起,中英文分开隔期出版《逻辑学研究》征稿的内容将主要包括下述方向:符号逻辑、非形式逻辑、逻辑与哲学、