The Basic Constructive Logic for a Weak Sense of Consistency defined with a Propositional Falsity Constant

The logic B_Kc1 is the basic constructive logic in the ternaryrelational semantics (without a set of designated points) adequateto consistency understood as the absence of the negation ofany theorem. Negation is introduced in B_Kc1 with a negationconnective. The aim of this paper is to define the logic B_Kc1F.In this logic negation is introduced via a propositional falsityconstant. We prove that B_Kc1 and B_Kc1F are definitionally equivalent.     

A general tableau method for propositional interval temporal logics: Theory and implementation

In this paper, we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's CDT logic interpreted over partial orders (BCDT⁺ for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented.     

A Loop-Free Decision Procedure for Modal Propositional Logics K4, S4 and S5

The aim of this paper is to present a loop-free decision procedure for modal propositional logics K4, S4 and S5. We prove that the procedure terminates and that it is sound and complete. The procedure is based on the method of Socratic proofs for modal logics, which is grounded in the logic of questions IEL.     

Proof-Theoretic Functional Completeness for the Hybrid Logics of Everywhere and Elsewhere

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding so-called satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results.     

Completeness of S4 for the Lebesgue Measure Algebra

We prove completeness of the propositional modal logic S4 for the measure algebra based on the Lebesgue-measurable subsets of the unit interval, [0, 1]. In recent talks, Dana Scott introduced a new measure-based semantics for the standard propositional modal language with Boolean connectives and necessity and possibility operators, ^[¯]\Box and \Diamond\Diamond. Propositional modal formulae are assigned to Lebesgue-measurable subsets of the real interval [0, 1], modulo sets of measure zero. Equivalence classes of Lebesgue-measurable subsets form a measure algebra, M\mathcal M, and we add to this a non-trivial interior operator constructed from the frame of ‘open’ elements—elements in M\mathcal M with an open representative. We prove completeness of the modal logic S4 for the algebra M\mathcal M. A corollary to the main result is that non-theorems of S4 can be falsified at each point in a subset of the real interval [0, 1] of measure arbitrarily close to 1. A second corollary is that Intuitionistic propositional logic (IPC) is complete for the frame of open elements in M\mathcal M.     

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.     

Cut-free sequent and tableau systems for propositional Diodorean modal logics

We present sound, (weakly) complete and cut-free tableau systems for the propositional normal modal logicsS4.3, S4.3.1 andS4.14. When the modality is given a temporal interpretation, these logics respectively model time as a linear dense sequence of points; as a linear discrete sequence of points; and as a branching tree where each branch is a linear discrete sequence of points.Although cut-free, the last two systems do not possess the subformula property. But for any given finite set of formulaeX the superformulae involved are always bounded by a finite set of formulaeX* _L depending only onX and the logicL. Thus each system gives a nondeterministic decision procedure for the logic in question. The completeness proofs yield deterministic decision procedures for each logic because each proof is constructive.Each tableau system has a cut-free sequent analogue proving that Gentzen's cut-elimination theorem holds for these latter systems. The techniques are due to Hintikka and Rautenberg.Presented byDov M. Gabbay     

An analytic tableau calculus for a temporalised belief logic

A tableau is a refutation-based decision procedure for a related logic, and is among the most popular proof procedures for modal logics. In this paper, we present a labelled tableau calculus for a temporalised belief logic called TML⁺, which is obtained by adding a linear-time temporal logic onto a belief logic by the temporalisation method of Finger and Gabbay. We first establish the soundness and the completeness of the labelled tableau calculus based on the soundness and completeness results of its constituent logics. We then sketch a resolution-type proof procedure that complements the tableau calculus and also propose a model checking algorithm for TML⁺ based on the recent results for model checking procedures for temporalised logics. TML⁺ is suitable for formalising trust and agent beliefs and reasoning about their evolution for agent-based systems. Based on the logic TML⁺, the proposed labelled tableau calculus could be used for analysis, design and verification of agent-based systems operating in dynamic environments.     

The Method of Socratic Proofs for Modal Propositional Logics: K5, S4.2, S4.3, S4F,S4R,S4M and G

The aim of this paper is to present the method of Socratic proofs for seven modal propositional logics: K5, S4.2, S4.3, S4M, S4F, S4R and G. This work is an extension of [10] where the method was presented for the most common modal propositional logics: K, D, T, KB, K4, S4 and S5. Presented by Jacek Malinowski     

Expressivity of Second Order Propositional Modal Logic

We consider second-order propositional modal logic (SOPML), an extension of the basic modal language with propositional quantifiers introduced by Kit Fine in 1970. We determine the precise expressive power of SOPML by giving analogues of the Van Benthem–Rosen theorem and the Goldblatt Thomason theorem. Furthermore, we show that the basic modal language is the bisimulation invariant fragment of SOPML, and we characterize the bounded fragment of first-order logic as being the intersection of first-order logic and SOPML.     

Identical Twins,Deduction Theorems,and Pattern Functions: Exploring the Implicative BCSK Fragment of S5

We recapitulate (Section 1) some basic details of the system of implicative BCSK logic, which has two primitive binary implicational connectives, and which can be viewed as a certain fragment of the modal logic S5. From this modal perspective we review (Section 2) some results according to which the pure sublogic in either of these connectives (i.e., each considered without the other) is an exact replica of the material implication fragment of classical propositional logic. In Sections 3 and 5 we show that for the pure logic of one of these implicational connectives two – in general distinct – consequence relations (global and local) definable in the Kripke semantics for modal logic turn out to coincide, though this is not so for the pure logic of the other connective, and that there is an intimate relation between formulas constructed by means of the former connective and the local consequence relation. (Corollary 5.8. This, as we show in an Appendix, is connected to the fact that the ‘propositional operations’ associated with both of our implicational connectives are close to being what R. Quackenbush has called pattern functions.) Between these discussions Section 4 examines some of the replacement-of-equivalents properties of the two connectives, relative to these consequence relations, and Section 6 closes with some observations about the metaphor of identical twins as applied to such pairs of connectives.     

SUPERVALUATION FIXED-POINT LOGICS OF TRUTH

Michael Kremer defines fixed-point logics of truth based on Saul Kripke’s fixed point semantics for languages expressing their own truth concepts. Kremer axiomatizes the strong Kleene fixed-point logic of truth and the weak Kleene fixed-point logic of truth, but leaves the axiomatizability question open for the supervaluation fixed-point logic of truth and its variants. We show that the principal supervaluation fixed point logic of truth, when thought of as consequence relation, is highly complex: it is not even analytic. We also consider variants, engendered by a stronger notion of ‘fixed point’, and by variant supervaluation schemes. A ‘logic’ is often thought of, not as a consequence relation, but as a set of sentences – the sentences true on each interpretation. We axiomatize the supervaluation fixed-point logics so conceived.     

Generic generalized Rosser fixed points

To the standard propositional modal system of provability logic constants are added to account for the arithmetical fixed points introduced by Bernardi-Montagna in [5]. With that interpretation in mind, a system LR of modal propositional logic is axiomatized, a modal completeness theorem is established for LR and, after that, a uniform arithmetical (Solovay-type) completeness theorem with respect to PA is obtained for LR. This paper supersedes: Franco Montagna, Extremely undecidable sentences and generic generalized Rosser's fixed points, Rapporto Matematico, No. 95, Siena, 1983.     

Complexity Results for Modal Dependence Logic

Modal dependence logic was introduced recently by Väänänen. It enhances the basic modal language by an operator = (). For propositional variables p ₁, . . . , p _n , = (p ₁, . . . , p _n-1, p _n ) intuitively states that the value of p _n is determined by those of p ₁, . . . , p _n-1. Sevenster (J. Logic and Computation, 2009) showed that satisfiability for modal dependence logic is complete for nondeterministic exponential time. In this paper we consider fragments of modal dependence logic obtained by restricting the set of allowed propositional connectives. We show that satisfiability for poor man’s dependence logic, the language consisting of formulas built from literals and dependence atoms using ${\wedge, \square, \lozenge}$ (i. e., disallowing disjunction), remains NEXPTIME-complete. If we only allow monotone formulas (without negation, but with disjunction), the complexity drops to PSPACE-completeness. We also extend Väänänen’s language by allowing classical disjunction besides dependence disjunction and show that the satisfiability problem remains NEXPTIME-complete. If we then disallow both negation and dependence disjunction, satisfiability is complete for the second level of the polynomial hierarchy. Additionally we consider the restriction of modal dependence logic where the length of each single dependence atom is bounded by a number that is fixed for the whole logic. We show that the satisfiability problem for this bounded arity dependence logic is PSPACE-complete and that the complexity drops to the third level of the polynomial hierarchy if we then disallow disjunction. In this way we completely classify the computational complexity of the satisfiability problem for all restrictions of propositional and dependence operators considered by Väänänen and Sevenster.     

Uniform Interpolation and Propositional Quantifiers in Modal Logics

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible. We shall present such a proof of the uniform interpolation theorem for normal modal logics K and T. It provides an explicit algorithm constructing the interpolants. Presented by Heinrich Wansing     

An O(n log n)-Space Decision Procedure for the Relevance Logic B+

In previous work we gave a new proof-theoretical method for establishing upper-bounds on the space complexity of the provability problem of modal and other propositional non-classical logics. Here we extend and refine these results to give an O(n log n)-space decision procedure for the basic positive relevance logic B⁺. We compute this upper-bound by first giving a sound and complete, cut-free, labelled sequent system for B⁺, and then establishing bounds on the application of the rules of this system.     

Three-valued Logics in Modal Logic

Every truth-functional three-valued propositional logic can be conservatively translated into the modal logic S5. We prove this claim constructively in two steps. First, we define a Translation Manual that converts any propositional formula of any three-valued logic into a modal formula. Second, we show that for every S5-model there is an equivalent three-valued valuation and vice versa. In general, our Translation Manual gives rise to translations that are exponentially longer than their originals. This fact raises the question whether there are three-valued logics for which there is a shorter translation into S5. The answer is affirmative: we present an elegant linear translation of the Logic of Paradox and of Strong Three-valued Logic into S5.