Results for 'Sequents'

81 found
Order:
  1. Stoic Sequent Logic and Proof Theory.Susanne Bobzien - 2019 - History and Philosophy of Logic 40 (3):234-265.
    This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzen-inspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich contemporary discussion. Much of Stoic (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  2. Nested Sequents for Intuitionistic Modal Logics via Structural Refinement.Tim Lyon - 2021 - In Anupam Das & Sara Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021. pp. 409-427.
    We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  3. A Cut-Free Sequent Calculus for Defeasible Erotetic Inferences.Jared Millson - 2019 - Studia Logica (6):1-34.
    In recent years, the e ffort to formalize erotetic inferences (i.e., inferences to and from questions) has become a central concern for those working in erotetic logic. However, few have sought to formulate a proof theory for these inferences. To fill this lacuna, we construct a calculus for (classes of) sequents that are sound and complete for two species of erotetic inferences studied by Inferential Erotetic Logic (IEL): erotetic evocation and regular erotetic implication. While an attempt has been made (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  4. A Nonmonotonic Sequent Calculus for Inferentialist Expressivists.Ulf Hlobil - 2016 - In Pavel Arazim & Michal Dancak (eds.), The Logica Yearbook 2015. College Publications. pp. 87-105.
    I am presenting a sequent calculus that extends a nonmonotonic consequence relation over an atomic language to a logically complex language. The system is in line with two guiding philosophical ideas: (i) logical inferentialism and (ii) logical expressivism. The extension defined by the sequent rules is conservative. The conditional tracks the consequence relation and negation tracks incoherence. Besides the ordinary propositional connectives, the sequent calculus introduces a new kind of modal operator that marks implications that hold monotonically. Transitivity fails, but (...)
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  5. A cut-free sequent calculus for the bi-intuitionistic logic 2Int.Sara Ayhan - manuscript
    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, which Wansing presents in [2016a]. There he also gives a natural deduction system for this logic, N2Int, to which SC2Int is equivalent in terms of what is derivable. What is important is that these calculi represent a kind of bilateralist reasoning, since they (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  6. Dual Systems of Sequents and Tableaux for Many-Valued Logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - Bulletin of the EATCS 51:192-197.
    The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value and (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  7. Uniform and Modular Sequent Systems for Description Logics.Tim Lyon & Jonas Karge - 2022 - In Ofer Arieli, Martin Homola, Jean Christoph Jung & Marie-Laure Mugnier (eds.), Proceedings of the 35th International Workshop on Description Logics (DL 2022).
    We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common description logics, but also allows for sequent systems to be obtained for extensions of description logics with special formulae that we call "role relational axioms." All sequent systems are sound, complete, and possess favorable properties such as height-preserving admissibility of common structural rules and height-preserving invertibility of rules.
    Download  
     
    Export citation  
     
    Bookmark  
  8. A perspective on modal sequent logic.Stephen Blamey & Lloyd Humberstone - 1991 - Publications of the Research Institute for Mathematical Sciences 27 (5):763-782.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  9. Proofnets for S5: sequents and circuits for modal logic.Greg Restall - 2007 - In C. Dimitracopoulos, L. Newelski & D. Normann (eds.), Logic Colloquium 2005: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Held in Athens, Greece, July 28-August 3, 2005. Cambridge: Cambridge University Press. pp. 151-172.
    In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). -/- The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is directly motivated (...)
    Download  
     
    Export citation  
     
    Bookmark   18 citations  
  10. A Simple Logical Matrix and Sequent Calculus for Parry’s Logic of Analytic Implication.Damian E. Szmuc - 2021 - Studia Logica 109 (4):791-828.
    We provide a logical matrix semantics and a Gentzen-style sequent calculus for the first-degree entailments valid in W. T. Parry’s logic of Analytic Implication. We achieve the former by introducing a logical matrix closely related to that inducing paracomplete weak Kleene logic, and the latter by presenting a calculus where the initial sequents and the left and right rules for negation are subject to linguistic constraints.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  11. Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents.Tim Lyon, Alwen Tiu, Rajeev Gore & Ranald Clouston - 2020 - In Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). pp. 1-16.
    We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  12. A multi-succedent sequent calculus for logical expressivists.Daniel Kaplan - 2018 - In Pavel Arazim & Tomas Lavicka (eds.), The Logica Yearbook 2017. College Publications. pp. 139-153.
    Expressivism in logic is the view that logical vocabulary plays a primarily expressive role: that is, that logical vocabulary makes perspicuous in the object language structural features of inference and incompatibility (Brandom, 1994, 2008). I present a precise, technical criterion of expressivity for a logic (§2). I next present a logic that meets that criterion (§3). I further explore some interesting features of that logic: first, a representation theorem for capturing other logics (§3.1), and next some novel logical vocabulary for (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  13. Translating Metainferences Into Formulae: Satisfaction Operators and Sequent Calculi.Ariel Jonathan Roffé & Federico Pailos - 2021 - Australasian Journal of Logic 3.
    In this paper, we present a way to translate the metainferences of a mixed metainferential system into formulae of an extended-language system, called its associated σ-system. To do this, the σ-system will contain new operators (one for each standard), called the σ operators, which represent the notions of "belonging to a (given) standard". We first prove, in a model-theoretic way, that these translations preserve (in)validity. That is, that a metainference is valid in the base system if and only if its (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  14. Automating Reasoning with Standpoint Logic via Nested Sequents.Tim Lyon & Lucía Gómez Álvarez - 2018 - In Michael Thielscher, Francesca Toni & Frank Wolter (eds.), Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR2018). pp. 257-266.
    Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics---proof systems that manipulate trees whose nodes are multisets of formulae---and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique in the context (...)
    Download  
     
    Export citation  
     
    Bookmark  
  15. Cut elimination for systems of transparent truth with restricted initial sequents.Carlo Nicolai - manuscript
    The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, (...)
    Download  
     
    Export citation  
     
    Bookmark  
  16. Elimination of Cuts in First-order Finite-valued Logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - Journal of Information Processing and Cybernetics EIK 29 (6):333-355.
    A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.
    Download  
     
    Export citation  
     
    Bookmark   18 citations  
  17. Cut-free Calculi and Relational Semantics for Temporal STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In Francesco Calimeri, Nicola Leone & Marco Manna (eds.), Logics in Artificial Intelligence. Springer. pp. 803 - 819.
    We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for Ldm , Tstit and Xstit. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3Ldm and G3Tstit are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also Xstit can be characterized through relational frames, omitting the use of BT+AC frames.
    Download  
     
    Export citation  
     
    Bookmark  
  18. Proof Theory and Semantics for a Theory of Definite Descriptions.Nils Kürbis - 2021 - In Anupam Das & Sara Negri (eds.), TABLEAUX 2021, LNAI 12842.
    This paper presents a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier I. I forms a formula from two formulas. Ix[F, G] means ‘The F is G’. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with I and it is shown to be (...)
    Download  
     
    Export citation  
     
    Bookmark  
  19. Refutation systems in modal logic.Valentin Goranko - 1994 - Studia Logica 53 (2):299 - 324.
    Complete deductive systems are constructed for the non-valid (refutable) formulae and sequents of some propositional modal logics. Thus, complete syntactic characterizations in the sense of Lukasiewicz are established for these logics and, in particular, purely syntactic decision procedures for them are obtained. The paper also contains some historical remarks and a general discussion on refutation systems.
    Download  
     
    Export citation  
     
    Bookmark   28 citations  
  20. A General Schema for Bilateral Proof Rules.Ryan Simonelli - 2024 - Journal of Philosophical Logic (3):1-34.
    Bilateral proof systems, which provide rules for both affirming and denying sentences, have been prominent in the development of proof-theoretic semantics for classical logic in recent years. However, such systems provide a substantial amount of freedom in the formulation of the rules, and, as a result, a number of different sets of rules have been put forward as definitive of the meanings of the classical connectives. In this paper, I argue that a single general schema for bilateral proof rules has (...)
    Download  
     
    Export citation  
     
    Bookmark  
  21. Fusion, fission, and Ackermann’s truth constant in relevant logics: A proof-theoretic investigation.Fabio De Martin Polo - forthcoming - In Andrew Tedder, Shawn Standefer & Igor Sedlar (eds.), New Directions in Relevant Logic. Springer.
    The aim of this paper is to provide a proof-theoretic characterization of relevant logics including fusion and fission connectives, as well as Ackermann’s truth constant. We achieve this by employing the well-established methodology of labelled sequent calculi. After having introduced several systems, we will conduct a detailed proof-theoretic analysis, show a cut-admissibility theorem, and establish soundness and completeness. The paper ends with a discussion that contextualizes our current work within the broader landscape of the proof theory of relevant logics.
    Download  
     
    Export citation  
     
    Bookmark  
  22. LP, K3, and FDE as Substructural Logics.Lionel Shapiro - 2017 - In Arazim Pavel & Lávička Tomáš (eds.), The Logica Yearbook 2016. College Publications.
    Building on recent work, I present sequent systems for the non-classical logics LP, K3, and FDE with two main virtues. First, derivations closely resemble those in standard Gentzen-style systems. Second, the systems can be obtained by reformulating a classical system using nonstandard sequent structure and simply removing certain structural rules (relatives of exchange and contraction). I clarify two senses in which these logics count as “substructural.”.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  23. Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems. Springer. pp. 202-218.
    This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  24. Proof Theory of Finite-valued Logics.Richard Zach - 1993 - Dissertation, Technische Universität Wien
    The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order (...)
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  25. A Binary Quantifier for Definite Descriptions for Cut Free Free Logics.Nils Kürbis - 2021 - Studia Logica 110 (1):219-239.
    This paper presents rules in sequent calculus for a binary quantifier I to formalise definite descriptions: Ix[F, G] means ‘The F is G’. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of I. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions with a (...)
    Download  
     
    Export citation  
     
    Bookmark  
  26. Expanding the universe of universal logic.James Trafford - 2014 - Theoria: Revista de Teoría, Historia y Fundamentos de la Ciencia 29 (3):325-343.
    In [5], Béziau provides a means by which Gentzen’s sequent calculus can be combined with the general semantic theory of bivaluations. In doing so, according to Béziau, it is possible to construe the abstract “core” of logics in general, where logical syntax and semantics are “two sides of the same coin”. The central suggestion there is that, by way of a modification of the notion of maximal consistency, it is possible to prove the soundness and completeness for any normal logic. (...)
    Download  
     
    Export citation  
     
    Bookmark  
  27. Theories of truth based on four-valued infectious logics.Damian Szmuc, Bruno Da Re & Federico Pailos - 2020 - Logic Journal of the IGPL 28 (5):712-746.
    Infectious logics are systems that have a truth-value that is assigned to a compound formula whenever it is assigned to one of its components. This paper studies four-valued infectious logics as the basis of transparent theories of truth. This take is motivated as a way to treat different pathological sentences differently, namely, by allowing some of them to be truth-value gluts and some others to be truth-value gaps and as a way to treat the semantic pathology suffered by at least (...)
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  28. Logic for Exact Entailment.Kit Fine & Mark Jago - 2019 - Review of Symbolic Logic 12 (3):536-556.
    An exact truthmaker for A is a state which, as well as guaranteeing A’s truth, is wholly relevant to it. States with parts irrelevant to whether A is true do not count as exact truthmakers for A. Giving semantics in this way produces a very unusual consequence relation, on which conjunctions do not entail their conjuncts. This feature makes the resulting logic highly unusual. In this paper, we set out formal semantics for exact truthmaking and characterise the resulting notion of (...)
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  29. An Epistemic Interpretation of Paraconsistent Weak Kleene Logic.Damian E. Szmuc - forthcoming - Logic and Logical Philosophy:1.
    This paper extends Fitting's epistemic interpretation of some Kleene logics, to also account for Paraconsistent Weak Kleene logic. To achieve this goal, a dualization of Fitting's "cut-down" operator is discussed, rendering a "track-down" operator later used to represent the idea that no consistent opinion can arise from a set including an inconsistent opinion. It is shown that, if some reasonable assumptions are made, the truth-functions of Paraconsistent Weak Kleene coincide with certain operations defined in this track-down fashion. Finally, further reflections (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  30. What is a Paraconsistent Logic?Damian Szmuc, Federico Pailos & Eduardo Barrio - 2018 - In Walter Carnielli & Jacek Malinowski (eds.), Contradictions, from Consistency to Inconsistency. Cham, Switzerland: Springer.
    Paraconsistent logics are logical systems that reject the classical principle, usually dubbed Explosion, that a contradiction implies everything. However, the received view about paraconsistency focuses only the inferential version of Explosion, which is concerned with formulae, thereby overlooking other possible accounts. In this paper, we propose to focus, additionally, on a meta-inferential version of Explosion, i.e. which is concerned with inferences or sequents. In doing so, we will offer a new characterization of paraconsistency by means of which a logic (...)
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
  31. Relevant Logics Obeying Component Homogeneity.Roberto Ciuni, Damian Szmuc & Thomas Macaulay Ferguson - 2018 - Australasian Journal of Logic 15 (2):301-361.
    This paper discusses three relevant logics that obey Component Homogeneity - a principle that Goddard and Routley introduce in their project of a logic of significance. The paper establishes two main results. First, it establishes a general characterization result for two families of logic that obey Component Homogeneity - that is, we provide a set of necessary and sufficient conditions for their consequence relations. From this, we derive characterization results for S*fde, dS*fde, crossS*fde. Second, the paper establishes complete sequent calculi (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  32. Paradoxes and Failures of Cut.David Ripley - 2013 - Australasian Journal of Philosophy 91 (1):139 - 164.
    This paper presents and motivates a new philosophical and logical approach to truth and semantic paradox. It begins from an inferentialist, and particularly bilateralist, theory of meaning---one which takes meaning to be constituted by assertibility and deniability conditions---and shows how the usual multiple-conclusion sequent calculus for classical logic can be given an inferentialist motivation, leaving classical model theory as of only derivative importance. The paper then uses this theory of meaning to present and motivate a logical system---ST---that conservatively extends classical (...)
    Download  
     
    Export citation  
     
    Bookmark   160 citations  
  33. Metainferences from a Proof-Theoretic Perspective, and a Hierarchy of Validity Predicates.Rea Golan - 2022 - Journal of Philosophical Logic 51 (6):1295–1325.
    I explore, from a proof-theoretic perspective, the hierarchy of classical and paraconsistent logics introduced by Barrio, Pailos and Szmuc in (Journal o f Philosophical Logic,49, 93-120, 2021). First, I provide sequent rules and axioms for all the logics in the hierarchy, for all inferential levels, and establish soundness and completeness results. Second, I show how to extend those systems with a corresponding hierarchy of validity predicates, each one of which is meant to capture “validity” at a different inferential level. Then, (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  34. Logics Based on Linear Orders of Contaminating Values.Roberto Ciuni, Thomas Macaulay Ferguson & Damian Szmuc - 2019 - Journal of Logic and Computation 29 (5):631–663.
    A wide family of many-valued logics—for instance, those based on the weak Kleene algebra—includes a non-classical truth-value that is ‘contaminating’ in the sense that whenever the value is assigned to a formula φ⁠, any complex formula in which φ appears is assigned that value as well. In such systems, the contaminating value enjoys a wide range of interpretations, suggesting scenarios in which more than one of these interpretations are called for. This calls for an evaluation of systems with multiple contaminating (...)
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  35. Systematic construction of natural deduction systems for many-valued logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - In Unknown (ed.), Proceedings of The Twenty-Third International Symposium on Multiple-Valued Logic, 1993. IEEE Press. pp. 208-213.
    A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  36. A paraconsistent route to semantic closure.Eduardo Alejandro Barrio, Federico Matias Pailos & Damian Enrique Szmuc - 2017 - Logic Journal of the IGPL 25 (4):387-407.
    In this paper, we present a non-trivial and expressively complete paraconsistent naïve theory of truth, as a step in the route towards semantic closure. We achieve this goal by expressing self-reference with a weak procedure, that uses equivalences between expressions of the language, as opposed to a strong procedure, that uses identities. Finally, we make some remarks regarding the sense in which the theory of truth discussed has a property closely related to functional completeness, and we present a sound and (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  37. Proof Systems for Super- Strict Implication.Guido Gherardi, Eugenio Orlandelli & Eric Raidl - 2023 - Studia Logica 112 (1):249-294.
    This paper studies proof systems for the logics of super-strict implication ST2–ST5, which correspond to C.I. Lewis’ systems S2–S5 freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating STn in Sn and backsimulating Sn in STn, respectively(for n=2,...,5). Next, G3-style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive of G3-style calculi, that they are sound and complete, and (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  38. Display to Labeled Proofs and Back Again for Tense Logics.Agata Ciabattoni, Tim Lyon, Revantha Ramanayake & Alwen Tiu - 2021 - ACM Transactions on Computational Logic 22 (3):1-31.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  39. Uniqueness of Logical Connectives in a Bilateralist Setting.Sara Ayhan - 2021 - In Martin Blicha & Igor Sedlár (eds.), The Logica Yearbook 2020. College Publications. pp. 1-16.
    In this paper I will show the problems that are encountered when dealing with uniqueness of connectives in a bilateralist setting within the larger framework of proof-theoretic semantics and suggest a solution. Therefore, the logic 2Int is suitable, for which I introduce a sequent calculus system, displaying - just like the corresponding natural deduction system - a consequence relation for provability as well as one dual to provability. I will propose a modified characterization of uniqueness incorporating such a duality of (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  40. Characterizing generics are material inference tickets: a proof-theoretic analysis.Preston Stovall - 2019 - Inquiry: An Interdisciplinary Journal of Philosophy (5):668-704.
    An adequate semantics for generic sentences must stake out positions across a range of contested territory in philosophy and linguistics. For this reason the study of generic sentences is a venue for investigating different frameworks for understanding human rationality as manifested in linguistic phenomena such as quantification, classification of individuals under kinds, defeasible reasoning, and intensionality. Despite the wide variety of semantic theories developed for generic sentences, to date these theories have been almost universally model-theoretic and representational. This essay outlines (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  41. The (Greatest) Fragment of Classical Logic that Respects the Variable-Sharing Principle (in the FMLA-FMLA Framework).Damian E. Szmuc - 2021 - Bulletin of the Section of Logic 50 (4):421-453.
    We examine the set of formula-to-formula valid inferences of Classical Logic, where the premise and the conclusion share at least a propositional variable in common. We review the fact, already proved in the literature, that such a system is identical to the first-degree entailment fragment of R. Epstein's Relatedness Logic, and that it is a non-transitive logic of the sort investigated by S. Frankowski and others. Furthermore, we provide a semantics and a calculus for this logic. The semantics is defined (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  42. Modeling the interaction of computer errors by four-valued contaminating logics.Roberto Ciuni, Thomas Macaulay Ferguson & Damian Szmuc - 2019 - In Rosalie Iemhoff, Michael Moortgat & Ruy de Queiroz (eds.), Logic, Language, Information, and Computation. Folli Publications on Logic, Language and Information. pp. 119-139.
    Logics based on weak Kleene algebra (WKA) and related structures have been recently proposed as a tool for reasoning about flaws in computer programs. The key element of this proposal is the presence, in WKA and related structures, of a non-classical truth-value that is “contaminating” in the sense that whenever the value is assigned to a formula ϕ, any complex formula in which ϕ appears is assigned that value as well. Under such interpretations, the contaminating states represent occurrences of a (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  43. Aristotle on the Individuation of Syllogisms.Phil Corkum - forthcoming - Ancient Philosophy.
    Discussion of the Aristotelian syllogistic over the last sixty years has arguably centered on the question whether syllogisms are inferences or implications. But the significance of this debate at times has been taken to concern whether the syllogistic is a logic or a theory, and how it ought to be represented by modern systems. Largely missing from this discussion has been a study of the few passages in the Prior Analytics where Aristotle provides explicit guidance on how to individuate syllogisms. (...)
    Download  
     
    Export citation  
     
    Bookmark  
  44. Non-reflexive Nonsense: Proof-Theory for Paracomplete Weak Kleene Logic.Bruno Da Ré, Damian Szmuc & María Inés Corbalán - forthcoming - Studia Logica:1-17.
    Our aim is to provide a sequent calculus whose external consequence relation coincides with the three-valued paracomplete logic `of nonsense' introduced by Dmitry Bochvar and, independently, presented as the weak Kleene logic K3W by Stephen C. Kleene. The main features of this calculus are (i) that it is non-reflexive, i.e., Identity is not included as an explicit rule (although a restricted form of it with premises is derivable); (ii) that it includes rules where no variable-inclusion conditions are attached; and (iii) (...)
    Download  
     
    Export citation  
     
    Bookmark  
  45. Refining Labelled Systems for Modal and Constructive Logics with Applications.Tim Lyon - 2021 - Dissertation, Technischen Universität Wien
    This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  46. Natural Deduction for the Sheffer Stroke and Peirce’s Arrow (and any Other Truth-Functional Connective).Richard Zach - 2015 - Journal of Philosophical Logic 45 (2):183-197.
    Methods available for the axiomatization of arbitrary finite-valued logics can be applied to obtain sound and complete intelim rules for all truth-functional connectives of classical logic including the Sheffer stroke and Peirce’s arrow. The restriction to a single conclusion in standard systems of natural deduction requires the introduction of additional rules to make the resulting systems complete; these rules are nevertheless still simple and correspond straightforwardly to the classical absurdity rule. Omitting these rules results in systems for intuitionistic versions of (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  47. Intensional models for the theory of types.Reinhard Muskens - 2007 - Journal of Symbolic Logic 72 (1):98-118.
    In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cut-free sequent calculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to applications. Firstly, it (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  48. The Epsilon Calculus and Herbrand Complexity.Georg Moser & Richard Zach - 2006 - Studia Logica 82 (1):133-155.
    Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator εx. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  49. Degree supervaluational logic.J. Robert G. Williams - 2011 - Review of Symbolic Logic 4 (1):130-149.
    Supervaluationism is often described as the most popular semantic treatment of indeterminacy. There’s little consensus, however, about how to fill out the bare-bones idea to include a characterization of logical consequence. The paper explores one methodology for choosing between the logics: pick a logic thatnorms beliefas classical consequence is standardly thought to do. The main focus of the paper considers a variant of standard supervaluational, on which we can characterizedegrees of determinacy. It applies the methodology above to focus ondegree logic. (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  50. Labeled calculi and finite-valued logics.Matthias Baaz, Christian G. Fermüller, Gernot Salzer & Richard Zach - 1998 - Studia Logica 61 (1):7-33.
    A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite -valued logic if the labels are interpreted as sets of truth values. Furthermore, it is shown that any finite -valued logic can be given an axiomatization by such a labeled calculus using arbitrary "systems of signs," i.e., of sets of truth values, as labels. The number of labels needed is logarithmic in the (...)
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
1 — 50 / 81