This paper investigates first-order game logic and first-order modal mu-calculus, which extend their propositional modal logic counterparts with first-order modalities of interpreted effects such as variable assignments. Unlike in the propositional case, both logics are shown to have the same expressive power and their proof calculi to have the same deductive power. Both calculi are also mutually relatively complete.
In the presence of differential equations, corollaries obtain usable and complete translations between differential game logic, a logic for the deductive verification of hybrid games, and the differential mu-calculus, the modal mu-calculus for hybrid systems. The differential mu-calculus is complete with respect to first-order fixpoint logic and differential game logic is complete with respect to its ODE-free fragment.
This paper proposes first-order modal $ξ$-calculus as well as genealogical Kripke models. Inspired by modal $μ$-calculus, first-order modal $ξ$-calculus takes a quite similar form and extends its inductive expressivity onto a different dimension. We elaborate on several vivid examples that demonstrate this logic's profound utility, especially for depicting genealogy of concurrent computer processes. Bisimulation notion for the logic has also been thoroughly examined.
This paper positively solves an open problem if it is possible to provide a Hilbert system to Epistemic Logic of Friendship (EFL) by Seligman, Girard and Liu. To find a Hilbert system, we first introduce a sound, complete and cut-free tree (or nested) sequent calculus for EFL, which is an integrated combination of Seligman's sequent calculus for basic hybrid logic and a tree sequent calculus for modal logic. Then we translate a tree sequent into an ordinary formula to specify a Hilbert system of EFL and finally show that our Hilbert system is sound and complete for the intended two-dimensional…
The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int. Calculi for this logic represent a kind of bilateralist reasoning, since they do not only internalize processes of verification or provability but also the dual processes in terms of falsification or what is called dual provability. A normal form theorem for a natural deduction calculus of 2Int has already been stated, in this paper I want to prove a cu…
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, branching recurrence, and branching corecurrence. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html). The logical vocabulary of the system consists of negation, parallel conjunction, parallel disjunction, branching recurrence, and branching corecurrence. The article is published in two parts, with (the previous) Part I containing preliminaries and a soundness proof, and (the present) Part II containing a completeness proof.
We introduce a sequent calculus for the temporal-over-topological fragment $\textbf{DTL}_{0}^{\circ * \slash \Box}$ of dynamic topological logic $\textbf{DTL}$, prove soundness semantically, and prove completeness syntactically using the axiomatization of $\textbf{DTL}_{0}^{\circ * \slash \Box}$ given in \cite{paper3}. A cut-free sequent calculus for $\textbf{DTL}_{0}^{\circ * \slash \Box}$ is obtained as the union of the propositional fragment of Gentzen's classical sequent calculus, two $\Box$ structural rules for the modal extension, and nine $\circ$ (next) and $*$ (henceforth) structural r…
Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；School of Computer Science, University of Birmingham（伯明翰大学计算机学院）
We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this con…
We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent. Using our translations, we also transfer the structural operations of composition and quotient from disjunctive modal transition systems to the modal nu-calculus. This shows that the modal nu-calculus supports composition and decomposition of specifications.
Computability logic is a formal theory of computability. The earlier article "Introduction to cirquent calculus and abstract resource semantics" by Japaridze proved soundness and completeness for the basic fragment CL5 of computability logic. The present article extends that result to the more expressive cirquent calculus system CL6, which is a conservative extension of both CL5 and classical propositional logic.
Public announcement logic(PAL) is an extension of epistemic logic (EL) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for PAL, which is an extension of that for EL with sequent rules adapted from the reduction axioms. This calculus admits cut and allows terminating proof search.
In this paper, we consider the polymodal version of Lambek calculus with subexponential modalities initially introduced by Kanovich, Kuznetsov, Nigam, and Scedrov and its quantale semantics. In our approach, subexponential modalities have an interpretation in terms of quantic conuclei. We show that this extension of Lambek calculus is complete w.r.t quantales with quantic conuclei. Also, we prove a representation theorem for quantales with quantic conuclei and show that Lambek calculus with subexponentials is relationally complete. Finally, we extend this representation theorem to the category…
We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show this calculus to be sound and complete for the above-mentioned semantics.
Cirquent calculus is a proof system manipulating circuit-style constructs rather than formulas. Using it, this article constructs a sound and complete axiomatization CL16 of the propositional fragment of computability logic (the game-semantically conceived logic of computational problems - see http://www.csc.villanova.edu/~japaridz/CL/ ) whose logical vocabulary consists of negation and parallel and choice connectives, and whose atoms represent elementary, i.e. moveless, games.
We present an extension of an algorithm for computing directly the denotation of a mu-calculus formula X over the configuration graph of a pushdown system to allow backwards modalities. Our method gives the first extension of the saturation technique to the full mu-calculus with backwards modalities.
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability for guarded formulas. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn eq…
We characterize the expressive power of the modal mu-calculus on monotone neighborhood structures, in the style of the Janin-Walukiewicz theorem for the standard modal mu-calculus. For this purpose we consider a monadic second-order logic for monotone neighborhood structures. Our main result shows that the monotone modal mu-calculus corresponds exactly to the fragment of this second-order language that is invariant for neighborhood bisimulations.
Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ``cut-free'' sequent calculus for BiInt has recently been shown by Uustalu to fail cut-elimination. We present a new cut-free sequent calculus for BiInt, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between implication and its dual, similarly to future and past modalities in tense logic…
This paper introduces a refinement of the sequent calculus approach called cirquent calculus. While in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint sequences of formulas, in cirquent calculus they are permitted to share elements. Explicitly allowing or disallowing shared resources and thus taking to a more subtle level the resource-awareness intuitions underlying substructural logics, cirquent calculus offers much greater flexibility and power than sequent calculus does. A need for substantially new deductive tools came with the birth of computability logic (see ht…
The so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we show that shifting from usual call-by-name to call-by-value lambda calculus allows regaining strong connections with the underlying logic. This will be done in the context of Elementary Affine Logic (EAL), designing a type system in natural deduction style assigning EAL formulae to lambda terms.
In this note we discuss a variant of linear logic with idempotent exponential modalities. We propose a sequent calculus system and discuss its semantics. We also give a concrete relational model for this calculus.
The paper introduces a knowledge representation language that combines the event calculus with description logic in a logic programming framework. The purpose is to provide the user with an expressive language for modelling and analysing systems that evolve over time. The approach is exemplified with the logic programming language as implemented in the Fusemate system. The paper extends Fusemate's rule language with a weakly DL-safe interface to the description logic $\cal ALCIF$ and adapts the event calculus to this extended language. This way, time-stamped ABoxes can be manipulated as fluent…
We investigate quantitative extensions of modal logic and the modal mu-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative mu-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particula…
This paper introduces a new proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of nontrivial schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms. The static semantics of differential dynamic logic is captured ex…
In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics, namely CK, CK+ID, CK+MP and CK+MP+ID. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also present CondLean, a theorem prover for these logics implementing SeqS calculi written in SICStus Prolog.
Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with aconjunctive and alternation-free fixpoint operators as well as the universal modality; the resulting logic -- the aconjunctive alternation-free monotone $μ$-calculus with the universal modality -- contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes.
We introduce a refutation graph calculus for classical first-order predicate logic, which is an extension of previous ones for binary relations. One reduces logical consequence to establishing that a constructed graph has empty extension, i. e. it represents bottom. Our calculus establishes that a graph has empty extension by converting it to a normal form, which is expanded to other graphs until we can recognize conflicting situations (equivalent to a formula and its negation).
We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some application…
We present a hypersequent calculus $\text{G}^3\textŁ\forall$ for first-order infinite-valued Łukasiewicz logic and for an extension of it, first-order rational Pavelka logic; the calculus is intended for bottom-up proof search. In $\text{G}^3\textŁ\forall$, there are no structural rules, all the rules are invertible, and designations of multisets of formulas are not repeated in any premise of the rules. The calculus $\text{G}^3\textŁ\forall$ proves any sentence that is provable in at least one of the previously known hypersequent calculi for the given logics. We study proof-theoretic propertie…
A genoid is a category of two objects such that one is the product of itself with the other. A genoid may be viewed as an abstract substitution algebra. It is a remarkable fact that such a simple concept can be applied to present a unified algebraic approach to lambda calculus and first order logic.
The formal system of intuitionistic epistemic logic IEL was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer-Hayting-Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. So, we prove that IEL is PSPACE-complete.
The modal logic S4 can be used via a Curry-Howard style correspondence to obtain a lambda-calculus. Modal (boxed) types are intuitively interpreted as `closed syntax of the calculus'. This lambda-calculus is called modal type theory --- this is the basic case of a more general contextual modal type theory, or CMTT. CMTT has never been given a denotational semantics in which modal types are given denotation as closed syntax. We show how this can indeed be done, with a twist. We also use the denotation to prove some properties of the system.
Thirty years ago, I introduced a non-commutative variant of classical linear logic, called "pomset logic", issued from a particular categorical interpretation of linear logic known as coherence spaces. In addition to the usual commutative multiplicative connectives of linear logic, pomset logic includes a non-commutative connective, "$\triangleleft$" called "before", associative and self-dual: $(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$. The conclusion of a pomset logic proof is a Partially Ordered MultiSET of formulas. Pomset logic enjoys a proof net calculus with cut-elimination…
Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any values considered so far). Previous attempts have been made to develop convenient rules for reasoning with the new-quantifier, but we argue that none of these attempts is completely satisfactory. In this article we develop a new sequent calculus for nominal logic in which the rules for the new- quantifier are much simpler than in previous attempts. We also pro…
Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuits, as opposed to the more traditional approaches that deal with tree-like objects such as formulas or sequents. Among its advantages are greater efficiency, flexibility and expressiveness. This paper presents a detailed elaboration of a deep-inference cirquent logic, which is naturally and inherently resource conscious. It shows that classical logic, both syntactically and semantically, is just a special, conservative fragment of this more general and, in a sense, more …
The primary goal of this paper is to present a unified way to transform the syntax of a logic system into certain initial algebraic structure so that it can be studied algebraically. The algebraic structures which one may choose for this purpose are various clones over a full subcategory of a category. We show that the syntax of equational logic, lambda calculus and first order logic can be represented as clones or right algebras of clones over the set of positive integers. The semantics is then represented by structures derived from left algebras of these clones.
The purpose of this paper is to give an easy to understand with step-by-step explanation to allow interested people to fully appreciate the power of natural deduction for first-order logic. Natural deduction as a proof system can be used to prove various statements in propositional logic, but we will see its extension to cover quantifiers which gives it more power over propositional logic in solving more complex, real-world problems. We started by going over logical connectives and quantifiers to agree on the symbols that will be used throughout the paper, as some authors use different symbols…
Nakano's "later" modality, inspired by Gödel-Löb provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a marriage of the intuitionistic modal logic KM and the intermediate logic LC. We therefore call this logic $\mathrm{KM}_{\mathrm{lin}}$. We give a sound and cut-free complete sequent calculus for $\math…
In this paper hypergraph Lambek calculus ($\mathrm{HL}$) is presented. This formalism aims to generalize the Lambek calculus ($\mathrm{L}$) to hypergraphs as hyperedge replacement grammars extend context-free grammars. In contrast to the Lambek calculus, $\mathrm{HL}$ deals with hypergraph types and sequents; its axioms and rules naturally generalize those of $\mathrm{L}$. Consequently, certain properties (e.g. the cut elimination) can be lifted from $\mathrm{L}$ to $\mathrm{HL}$. It is shown that $\mathrm{L}$ can be naturally embedded in $\mathrm{HL}$; moreover, a number of its variants ($\ma…
The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, a…
Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex annotations to guarantee soundness and cut-elimination. We give a simple and annotation-free display calculus for FILL which satisfies Belnap's generic cut-elimination theorem. To do so, our display calculus actually handles an extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with an `exclusion' connective defined via an adjunction with par. We…
