Labelled sequent calculi are provided for a wide class of normal modal systems using truth values as labels. The rules for formula constructors are common to all modal systems. For each modal system, specific rules for truth values are provided that reflect the envisaged properties of the accessibility relation. Both local and global reasoning are supported. Strong completeness is proved for a natural two-sorted algebraic semantics. As a corollary, strong completeness is also obtained over general Kripke semantics. A duality result (...) is established between the category of sober algebras and the category of general Kripke structures. A simple enrichment of the proposed sequent calculi is proved to be complete over standard Kripke structures. The calculi are shown to be analytic in a useful sense. (shrink)

We start with Fodor's critique of cognitive science in "The mind doesn't work that way: The scope and limits of computational psychology": he argues that much mental activity cannot be handled by the current methods of cognitive science because it is nonmonotonic and, therefore, is global in nature, is not context-free, and is thus not capable of being formalized by a Turing-like mental architecture. We look at the use of nonmonotonic logic in the artificial intelligence community, particularly with the discussion (...) of the so-called frame problem. The mainstream approach to the frame problem is, we argue, probably susceptible to Fodor's critique; however, there is an alternative approach, due to McCain and Turner, which is, when suitably reformulated, not susceptible. In the course of our argument, we give a proof theory for the McCain-Turner system and show that it satisfies cut elimination. We have two substantive conclusions: first, that Fodor's argument depends on assumptions about logical form which not all nonmonotonic theories satisfy and, second, that metatheory plays an important role in the context of evolutionary accounts of rationality. (shrink)

We present some proof-theoretic results for the normal modal logic whose characteristic axiom is \. We present a sequent system for this logic and a hypersequent system for its first-order form and show that these are equivalent to Hilbert-style axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and first-order logical truth, respectively. We close by proving equivalences with a Fitch-style proof system for revision theory.

In the last decade the concept of context has been extensivelyexploited in many research areas, e.g., distributed artificialintelligence, multi agent systems, distributed databases, informationintegration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion ofcontext have been proposed: Giunchiglia and Serafini's Multi LanguageSystems (ML systems), McCarthy's modal logics of contexts, andGabbay's Labelled Deductive Systems.Previous papers have argued in favor of ML systems with respect to theother approaches. Our aim in this paper is to support these arguments froma (...) theoretical perspective. We provide a very general definition of ML systems, which covers allthe ML systems used in the literature, and we develop a proof theoryfor an important subclass of them: the MR systems. We prove variousimportant results; among other things, we prove a normal form theorem,the sub-formula property, and the decidability of an importantinstance of the class of the MR systems. The paper concludes with a detailed comparison among the alternativeapproaches. (shrink)

We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination theorem isproved (...) in a syntactic way by modifying Gentzen's method. Thisdual-context style system exemplifies the effectiveness of dual-contextformulation in formalizing various non-classical logics. (shrink)

A theorem for embedding a first-order linear- time temporal logic LTL into its intuitionistic counterpart ILTL is proved using Baratella-Masini's temporal extension of the Gödel-Gentzen negative translation of classical logic into intuitionistic logic. A substructural counterpart LLTL of ILTL is introduced, and a theorem for embedding ILTL into LLTL is proved using a temporal extension of the Girard translation of intuitionistic logic into intuitionistic linear logic. These embedding theorems are proved syntactically based on Gentzen-type sequent calculi.

The purpose of this paper is to generalize Kripke semantics for propositional modal logic by geometrizing it, that is, by considering the space underlying the collection of all possible worlds as an important semantic feature in its own right, so as to take the idea of accessibility seriously. The resulting new modal semantics is worked out in a setting coming from Riemannian geometry, where Kripke semantics is shown to correspond to a particular case, namely, the discrete one. Several correspondence results, (...) established between variants of well-known modal systems and corresponding geometric properties, illustrate the import of this new framework. (shrink)

1. It is a fact that developing a good proof theory for modal logics is a difficult task. The problem is not in having deductive systems. In fact, all the main modal logics enjoy an axiomatic prese...

We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Došen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. (...) With the exception of S5, the systems are modular in the sense that different structural rules capture different properties of the accessibility relation. We provide the first direct semantical cut-free completeness proofs for K, T, and D, and show how this method fails in the case of B and S4. (shrink)

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and (...) proof normalization. We have implemented our work in the Isabelle Logical Framework. (shrink)

We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.

Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an ω–type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set of (...) extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness. (shrink)