Switch to: References

Add citations

You must login to add citations.
  1. Nested sequents for intermediate logics: the case of Gödel-Dummett logics.Tim S. Lyon - 2023 - Journal of Applied Non-Classical Logics 33 (2):121-164.
    We present nested sequent systems for propositional Gödel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these Gödel-Dummett logics, we introduce a new structural rule, called the linearity rule, which (bottom-up) operates by linearising branching structure in a given nested sequent. In addition, an interesting feature of our calculi is the inclusion of reachability rules, which are special logical rules that operate by propagating data and/or checking (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics.Tim Lyon - 2021 - Journal of Logic and Computation 31 (1):213-265.
    This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems.Tim Lyon - 2013 - In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734). Springer. pp. 177-194.
    This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Transgressions Are Equal, and Right Actions Are Equal: some Philosophical Reflections on Paradox III in Cicero’s Paradoxa Stoicorum.Daniel Rönnedal - 2017 - Philosophia 45 (1):317-334.
    In Paradoxa Stoicorum, the Roman philosopher Cicero defends six important Stoic theses. Since these theses seem counterintuitive, and it is not likely that the average person would agree with them, they were generally called "paradoxes". According to the third paradox, (P3), (all) transgressions (wrong actions) are equal and (all) right actions are equal. According to one interpretation of this principle, which I will call (P3′), it means that if it is forbidden that A and it is forbidden that B, then (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Counterfactuals and semantic tableaux.Daniel Rönnedal - 2009 - Logic and Logical Philosophy 18 (1):71-91.
    The purpose of this paper is to develop a class of semantic tableau systems for some counterfactual logics. All in all I will discuss 1024 systems. Possible world semantics is used to interpret our formal languages. Soundness results are obtained for every tableau system and completeness results for a large subclass of these.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Dyadic deontic logic and semantic tableaux.Daniel Rönnedal - 2009 - Logic and Logical Philosophy 18 (3-4):221-252.
    The purpose of this paper is to develop a class of semantic tableau systems for some dyadic deontic logics. We will consider 16 different pure dyadic deontic tableau systems and 32 different alethic dyadic deontic tableau systems. Possible world semantics is used to interpret our formal languages. Some relationships between our systems and well known dyadic deontic logics in the literature are pointed out and soundness results are obtained for every tableau system. Completeness results are obtained for all 16 pure (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Prefixed tableaus and nested sequents.Melvin Fitting - 2012 - Annals of Pure and Applied Logic 163 (3):291 - 313.
    Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants (...)
    Download  
     
    Export citation  
     
    Bookmark   20 citations  
  • First-Order Modal Logic.Melvin Fitting & Richard L. Mendelsohn - 1998 - Dordrecht, Netherland: Kluwer Academic Publishers.
    This is a thorough treatment of first-order modal logic. The book covers such issues as quantification, equality (including a treatment of Frege's morning star/evening star puzzle), the notion of existence, non-rigid constants and function symbols, predicate abstraction, the distinction between nonexistence and nondesignation, and definite descriptions, borrowing from both Fregean and Russellian paradigms.
    Download  
     
    Export citation  
     
    Bookmark   83 citations  
  • Relevant analytic tableaux.Michael A. McRobbie & Nuel D. Belnap - 1979 - Studia Logica 38 (2):187 - 200.
    Tableau formulations are given for the relevance logics E (Entailment), R (Relevant implication) and RM (Mingle). Proofs of equivalence to modus-ponens-based formulations are vialeft-handed Gentzen sequenzen-kalküle. The tableau formulations depend on a detailed analysis of the structure of tableau rules, leading to certain global requirements. Relevance is caught by the requirement that each node must be used; modality is caught by the requirement that only certain rules can cross a barrier. Open problems are discussed.
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • A Natural Deduction Calculus for S4.2.Simone Martini, Andrea Masini & Margherita Zorzi - 2024 - Notre Dame Journal of Formal Logic 65 (2):127-150.
    We propose a natural deduction calculus for the modal logic S4.2. The system is designed to match as much as possible the structure and the properties of the standard system of natural deduction for first-order classical logic, exploiting the formal analogy between modalities and quantifiers. The system is proved sound and complete with respect to (w.r.t.) the standard Hilbert-style formulation of S4.2. Normalization and its consequences are obtained in a natural way, with proofs that closely follow the analogous ones for (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Axiomatic and Tableau-Based Reasoning for Kt.Renate A. Schmidt, John G. Stell & David Rydeheard - 2014 - In Rajeev Goré, Barteld Kooi & Agi Kurucz (eds.), Advances in Modal Logic, Volume 10: Papers From the Tenth Aiml Conference, Held in Groningen, the Netherlands, August 2014. London, England: CSLI Publications. pp. 478-497.
    Download  
     
    Export citation  
     
    Bookmark  
  • Interpolation for first order S5.Melvin Fitting - 2002 - Journal of Symbolic Logic 67 (2):621-634.
    An interpolation theorem holds for many standard modal logics, but first order $S5$ is a prominent example of a logic for which it fails. In this paper it is shown that a first order $S5$ interpolation theorem can be proved provided the logic is extended to contain propositional quantifiers. A proper statement of the result involves some subtleties, but this is the essence of it.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Grafting hypersequents onto nested sequents.Roman Kuznets & Björn Lellmann - 2016 - Logic Journal of the IGPL 24 (3):375-423.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Synthetic completeness proofs for Seligman-style tableau systems.Klaus Frovin Jørgensen, Patrick Blackburn, Thomas Bolander & Torben Braüner - 2016 - In Lev Beklemishev, Stéphane Demri & András Máté (eds.), Advances in Modal Logic, Volume 11. CSLI Publications. pp. 302-321.
    Download  
     
    Export citation  
     
    Bookmark  
  • Barcan Both Ways.Melvin Fitting - 1999 - Journal of Applied Non-Classical Logics 9 (2):329-344.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Natural Deduction, Hybrid Systems and Modal Logics.Andrzej Indrzejczak - 2010 - Dordrecht, Netherland: Springer.
    This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • Model existence theorems for modal and intuitionistic logics.Melvin Fitting - 1973 - Journal of Symbolic Logic 38 (4):613-627.
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Cut Elimination for Extended Sequent Calculi.Simone Martini, Andrea Masini & Margherita Zorzi - 2023 - Bulletin of the Section of Logic 52 (4):459-495.
    We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Two-Dimensional Tableaux.David Gilbert - 2016 - Australasian Journal of Logic 13 (7).
    We present two-dimensional tableau systems for the actuality, fixedly, and up-arrow operators. All systems are proved sound and complete with respect to a two-dimensional semantics. In addition, a decision procedure for the actuality logics is discussed.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • First-order intensional logic.Melvin Fitting - 2004 - Annals of Pure and Applied Logic 127 (1-3):171-193.
    First - order modal logic is very much under current development, with many different semantics proposed. The use of rigid objects goes back to Saul Kripke. More recently, several semantics based on counterparts have been examined, in a development that goes back to David Lewis. There is yet another line of research, using intensional objects, that traces back to Richard Montague. I have been involved with this line of development for some time. In the present paper, I briefly sketch several (...)
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Nested Sequents for Intuitionistic Logics.Melvin Fitting - 2014 - Notre Dame Journal of Formal Logic 55 (1):41-61.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Destructive Modal Resolution ∗.Melvin Fitting - unknown
    We present non-clausal resolution systems for propositional modal logics whose Kripke models do not involve symmetry, and for first order versions whose Kripke models do not involve constant domains. We give systems for K, T , K4 and S4; other logics are also possible. Our systems do not require preliminary reduction to a normal form and, in the first order case, intermingle resolution steps with Skolemization steps.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Theory matrices (for modal logics) using alphabetical monotonicity.Ian P. Gent - 1993 - Studia Logica 52 (2):233 - 257.
    In this paper I give conditions under which a matrix characterisation of validity is correct for first order logics where quantifications are restricted by statements from a theory. Unfortunately the usual definition of path closure in a matrix is unsuitable and a less pleasant definition must be used. I derive the matrix theorem from syntactic analysis of a suitable tableau system, but by choosing a tableau system for restricted quantification I generalise Wallen's earlier work on modal logics. The tableau system (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Investigations into quantified modal logic.Zane Parks - 1976 - Studia Logica 35:109.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Modal Hybrid Logic.Andrzej Indrzejczak - 2007 - Logic and Logical Philosophy 16 (2-3):147-257.
    This is an extended version of the lectures given during the 12-thConference on Applications of Logic in Philosophy and in the Foundationsof Mathematics in Szklarska Poręba. It contains a surveyof modal hybrid logic, one of the branches of contemporary modal logic. Inthe first part a variety of hybrid languages and logics is presented with adiscussion of expressivity matters. The second part is devoted to thoroughexposition of proof methods for hybrid logics. The main point is to showthat application of hybrid logics (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Labeled sequent calculi for modal logics and implicit contractions.Pierluigi Minari - 2013 - Archive for Mathematical Logic 52 (7-8):881-907.
    The paper settles an open question concerning Negri-style labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s tree-hypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain complete w.r.t. valid sequents whose relational (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Modal logic should say more than it does.Melvin Fitting - unknown
    First-order modal logics, as traditionally formulated, are not expressive enough. It is this that is behind the difficulties in formulating a good analog of Herbrand’s Theorem, as well as the well-known problems with equality, non-rigid designators, definite descriptions, and nondesignating terms. We show how all these problems disappear when modal language is made more expressive in a simple, natural way. We present a semantic tableaux system for the enhanced logic, and (very) briefly discuss implementation issues.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Modal interpolation via nested sequents.Melvin Fitting & Roman Kuznets - 2015 - Annals of Pure and Applied Logic 166 (3):274-305.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Noncumulative dialectical models and formal dialectics.Erik C. W. Krabbe - 1985 - Journal of Philosophical Logic 14 (2):129 - 168.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • A Bi-Modal Characterization of Epistemic Logic.Arata Ishimoto - 1978 - Annals of the Japan Association for Philosophy of Science 5 (3):135-155.
    Download  
     
    Export citation  
     
    Bookmark