Switch to: References

Citations of:

Structural Proof Theory

Philosophical Review 115 (2):255-258 (2006)

Add citations

You must login to add citations.
  1. Variations on Intra-Theoretical Logical Pluralism: Internal Versus External Consequence.Bogdan Dicher - 2020 - Philosophical Studies 177 (3):667-686.
    Intra-theoretical logical pluralism is a form of meaning-invariant pluralism about logic, articulated recently by Hjortland :355–373, 2013). This version of pluralism relies on it being possible to define several distinct notions of provability relative to the same logical calculus. The present paper picks up and explores this theme: How can a single logical calculus express several different consequence relations? The main hypothesis articulated here is that the divide between the internal and external consequence relations in Gentzen systems generates a form (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Translations Between Gentzen–Prawitz and Jaśkowski–Fitch Natural Deduction Proofs.Shawn Standefer - 2019 - Studia Logica 107 (6):1103-1134.
    Two common forms of natural deduction proof systems are found in the Gentzen–Prawitz and Jaśkowski–Fitch systems. In this paper, I provide translations between proofs in these systems, pointing out the ways in which the translations highlight the structural rules implicit in the systems. These translations work for classical, intuitionistic, and minimal logic. I then provide translations for classical S4 proofs.
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  • Socratic Trees.Dorota Leszczyńska-Jasion, Mariusz Urbański & Andrzej Wiśniewski - 2013 - Studia Logica 101 (5):959-986.
    The method of Socratic proofs (SP-method) simulates the solving of logical problem by pure questioning. An outcome of an application of the SP-method is a sequence of questions, called a Socratic transformation. Our aim is to give a method of translation of Socratic transformations into trees. We address this issue both conceptually and by providing certain algorithms. We show that the trees which correspond to successful Socratic transformations—that is, to Socratic proofs—may be regarded, after a slight modification, as Gentzen-style proofs. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Dual Erotetic Calculi and the Minimal {Mathsf{LFI}}.Szymon Chlebowski & Dorota Leszczyńska-Jasion - 2015 - Studia Logica 103 (6):1245-1278.
    An erotetic calculus for a given logic constitutes a sequent-style proof-theoretical formalization of the logic grounded in Inferential Erotetic Logic ). In this paper, a new erotetic calculus for Classical Propositional Logic ), dual with respect to the existing ones, is given. We modify the calculus to obtain complete proof systems for the propositional part of paraconsistent logic \ and its extensions \ and \. The method is based on dual resolution. Moreover, the resolution rule is non-clausal. According to the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Dual Erotetic Calculi and the Minimal $${\Mathsf{LFI}}$$ LFI.Dorota Leszczyńska-Jasion & Szymon Chlebowski - 2015 - Studia Logica 103 (6):1245-1278.
    An erotetic calculus for a given logic constitutes a sequent-style proof-theoretical formalization of the logic grounded in Inferential Erotetic Logic. In this paper, a new erotetic calculus for Classical Propositional Logic, dual with respect to the existing ones, is given. We modify the calculus to obtain complete proof systems for the propositional part of paraconsistent logic $${\mathsf{CLuN}}$$ CLuN and its extensions $${\mathsf{CLuNs}}$$ CLuNs and $${\mathsf{mbC}}$$ mbC. The method is based on dual resolution. Moreover, the resolution rule is non-clausal. According to (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Sequent Calculi for $${\Mathsf {SCI}}$$ SCI.Szymon Chlebowski - 2018 - Studia Logica 106 (3):541-563.
    In this paper we are applying certain strategy described by Negri and Von Plato :418–435, 1998), allowing construction of sequent calculi for axiomatic theories, to Suszko’s Sentential calculus with identity. We describe two calculi obtained in this way, prove that the cut rule, as well as the other structural rules, are admissible in one of them, and we also present an example which suggests that the cut rule is not admissible in the other.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Reasoning About Collectively Accepted Group Beliefs.Raul Hakli & Sara Negri - 2011 - Journal of Philosophical Logic 40 (4):531-555.
    A proof-theoretical treatment of collectively accepted group beliefs is presented through a multi-agent sequent system for an axiomatization of the logic of acceptance. The system is based on a labelled sequent calculus for propositional multi-agent epistemic logic with labels that correspond to possible worlds and a notation for internalized accessibility relations between worlds. The system is contraction- and cut-free. Extensions of the basic system are considered, in particular with rules that allow the possibility of operative members or legislators. Completeness with (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Reasoning About Truth in First-Order Logic.Claes Strannegård, Fredrik Engström, Abdul Rahim Nizamani & Lance Rips - 2013 - Journal of Logic, Language and Information 22 (1):115-137.
    First, we describe a psychological experiment in which the participants were asked to determine whether sentences of first-order logic were true or false in finite graphs. Second, we define two proof systems for reasoning about truth and falsity in first-order logic. These proof systems feature explicit models of cognitive resources such as declarative memory, procedural memory, working memory, and sensory memory. Third, we describe a computer program that is used to find the smallest proofs in the aforementioned proof systems when (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  • Argumentation Mining.Raquel Mochales & Marie-Francine Moens - 2011 - Artificial Intelligence and Law 19 (1):1-22.
    Argumentation mining aims to automatically detect, classify and structure argumentation in text. Therefore, argumentation mining is an important part of a complete argumentation analyisis, i.e. understanding the content of serial arguments, their linguistic structure, the relationship between the preceding and following arguments, recognizing the underlying conceptual beliefs, and understanding within the comprehensive coherence of the specific topic. We present different methods to aid argumentation mining, starting with plain argumentation detection and moving forward to a more structural analysis of the detected (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  • Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.
    Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  • A Proof-Search Procedure for Intuitionistic Propositional Logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
    A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • Glivenko Sequent Classes in the Light of Structural Proof Theory.Sara Negri - 2016 - Archive for Mathematical Logic 55 (3-4):461-473.
    In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Cut Elimination for Entailment Relations.Davide Rinaldi & Daniel Wessel - 2019 - Archive for Mathematical Logic 58 (5-6):605-625.
    Entailment relations, introduced by Scott in the early 1970s, provide an abstract generalisation of Gentzen’s multi-conclusion logical inference. Originally applied to the study of multi-valued logics, this notion has then found plenty of applications, ranging from computer science to abstract algebra. In particular, an entailment relation can be regarded as a constructive presentation of a distributive lattice and in this guise it has proven to be a useful tool for the constructive reformulation of several classical theorems in commutative algebra. In (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Conditional Heresies.Fabrizio Cariani & Simon Goldstein - 2018 - Philosophy and Phenomenological Research.
  • Free of Detachment: Logic, Rationality, and Gluts.Jc Beall - 2015 - Noûs 49 (2):410-423.
  • Lp+, K3+, Fde+, and Their 'Classical Collapse'.Jc Beall - 2013 - Review of Symbolic Logic 6 (4):742-754.
    This paper is a sequel to Beall (2011), in which I both give and discuss the philosophical import of a result for the propositional (multiple-conclusion) logic LP+. Feedback on such ideas prompted a spelling out of the first-order case. My aim in this paper is to do just that: namely, explicitly record the first-order result(s), including the collapse results for K3+ and FDE+.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  • Translating a Fragment of Natural Deduction System for Natural Language Into Modern Type Theory.Ivo Pezlar - 2019 - In Rainer Osswald, Christian Retoré & Peter Sutton (eds.), Proceedings of the IWCS 2019 Workshop on Computing Semantics with Types, Frames and Related Structures. Stroudsburg, PA: Association for Computational Linguistics. pp. 10-18.
    In this paper, we investigate the possibility of translating a fragment of natural deduction system (NDS) for natural language semantics into modern type theory (MTT), originally suggested by Luo (2014). Our main goal will be to examine and translate the basic rules of NDS (namely, meta-rules, structural rules, identity rules, noun rules and rules for intersective and subsective adjectives) to MTT. Additionally, we will also consider some of their general features.
    Direct download  
     
    Export citation  
     
    Bookmark  
  • Validity Concepts in Proof-Theoretic Semantics.Peter Schroeder-Heister - 2006 - Synthese 148 (3):525-571.
    The standard approach to what I call “proof-theoretic semantics”, which is mainly due to Dummett and Prawitz, attempts to give a semantics of proofs by defining what counts as a valid proof. After a discussion of the general aims of proof-theoretic semantics, this paper investigates in detail various notions of proof-theoretic validity and offers certain improvements of the definitions given by Prawitz. Particular emphasis is placed on the relationship between semantic validity concepts and validity concepts used in normalization theory. It (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   30 citations  
  • Tableaux and Dual Tableaux: Transformation of Proofs.Joanna Golińska-Pilarek & Ewa Orłowska - 2007 - Studia Logica 85 (3):283-302.
    We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Does the Deduction Theorem Fail for Modal Logic?Raul Hakli & Sara Negri - 2012 - Synthese 187 (3):849-867.
    Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  • Reasoning Processes in Propositional Logic.Claes Strannegård, Simon Ulfsbäcker, David Hedqvist & Tommy Gärling - 2010 - Journal of Logic, Language and Information 19 (3):283-314.
    We conducted a computer-based psychological experiment in which a random mix of 40 tautologies and 40 non-tautologies were presented to the participants, who were asked to determine which ones of the formulas were tautologies. The participants were eight university students in computer science who had received tuition in propositional logic. The formulas appeared one by one, a time-limit of 45 s applied to each formula and no aids were allowed. For each formula we recorded the proportion of the participants who (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Cut-Elimination and Quantification in Canonical Systems.Anna Zamansky & Arnon Avron - 2006 - Studia Logica 82 (1):157-176.
    Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  • Normality, Non-Contamination and Logical Depth in Classical Natural Deduction.Marcello D’Agostino, Dov Gabbay & Sanjay Modgil - forthcoming - Studia Logica.
    In this paper we provide a detailed proof-theoretical analysis of a natural deduction system for classical propositional logic that represents classical proofs in a more natural way than standard Gentzen-style natural deduction, admits of a simple normalization procedure such that normal proofs enjoy the Weak Subformula Property, provides the means to prove a Non-contamination Property of normal proofs that is not satisfied by normal proofs in the Gentzen tradition and is useful for applications, especially in formal argumentation, naturally leads to (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Truth in a Logic of Formal Inconsistency: How Classical Can It Get?Lavinia Picollo - forthcoming - Logic Journal of the IGPL.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Absorbing the Structural Rules in the Sequent Calculus with Additional Atomic Rules.Franco Parlamento & Flavio Previale - forthcoming - Archive for Mathematical Logic:1-20.
    We show that if the structural rules are admissible over a set \ of atomic rules, then they are admissible in the sequent calculus obtained by adding the rules in \ to the multisuccedent minimal and intuitionistic \ calculi as well as to the classical one. Two applications to pure logic and to the sequent calculus with equality are presented.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Reaching Transparent Truth.Pablo Cobreros, Paul Égré, David Ripley & Robert van Rooij - 2013 - Mind 122 (488):841-866.
    This paper presents and defends a way to add a transparent truth predicate to classical logic, such that and A are everywhere intersubstitutable, where all T-biconditionals hold, and where truth can be made compositional. A key feature of our framework, called STTT (for Strict-Tolerant Transparent Truth), is that it supports a non-transitive relation of consequence. At the same time, it can be seen that the only failures of transitivity STTT allows for arise in paradoxical cases.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   40 citations  
  • On Paradoxes in Normal Form.Mattia Petrolo & Paolo Pistone - 2019 - Topoi 38 (3):605-617.
    A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational interpretation of proofs and from the viewpoint of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Proof Theory for Quantified Monotone Modal Logics.Sara Negri & Eugenio Orlandelli - 2019 - Logic Journal of the IGPL 27 (4):478-506.
    This paper provides a proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi introduced (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • Judgement Aggregation in Non-Classical Logics.Daniele Porello - 2017 - Journal of Applied Non-Classical Logics 27 (1-2):106-139.
    This work contributes to the theory of judgement aggregation by discussing a number of significant non-classical logics. After adapting the standard framework of judgement aggregation to cope with non-classical logics, we discuss in particular results for the case of Intuitionistic Logic, the Lambek calculus, Linear Logic and Relevant Logics. The motivation for studying judgement aggregation in non-classical logics is that they offer a number of modelling choices to represent agents’ reasoning in aggregation problems. By studying judgement aggregation in logics that (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  • Kripke Completeness Revisited.Sara Negri - 2009 - In Giuseppe Primiero (ed.), Acts of Knowledge: History, Philosophy and Logic. College Publications. pp. 233--266.
  • Incomplete Symbols — Definite Descriptions Revisited.Norbert Gratzl - 2015 - Journal of Philosophical Logic 44 (5):489-506.
    We investigate incomplete symbols, i.e. definite descriptions with scope-operators. Russell famously introduced definite descriptions by contextual definitions; in this article definite descriptions are introduced by rules in a specific calculus that is very well suited for proof-theoretic investigations. That is to say, the phrase ‘incomplete symbols’ is formally interpreted as to the existence of an elimination procedure. The last section offers semantical tools for interpreting the phrase ‘no meaning in isolation’ in a formal way.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  • The Inexpressibility of Validity.Julien Murzi - 2014 - Analysis 74 (1):65-81.
    Tarski's Undefinability of Truth Theorem comes in two versions: that no consistent theory which interprets Robinson's Arithmetic (Q) can prove all instances of the T-Scheme and hence define truth; and that no such theory, if sound, can even express truth. In this note, I prove corresponding limitative results for validity. While Peano Arithmetic already has the resources to define a predicate expressing logical validity, as Jeff Ketland has recently pointed out (2012, Validity as a primitive. Analysis 72: 421-30), no theory (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Frontiers of Conditional Logic.Yale Weiss - 2019 - Dissertation, The Graduate Center, City University of New York
    Conditional logics were originally developed for the purpose of modeling intuitively correct modes of reasoning involving conditional—especially counterfactual—expressions in natural language. While the debate over the logic of conditionals is as old as propositional logic, it was the development of worlds semantics for modal logic in the past century that catalyzed the rapid maturation of the field. Moreover, like modal logic, conditional logic has subsequently found a wide array of uses, from the traditional (e.g. counterfactuals) to the exotic (e.g. conditional (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  • Double-Line Harmony in a Sequent Setting.Gratzl Norbert & Orlandelli Eugenio - 2017 - In Pavel Arazim & Tomáš Lávička (eds.), The Logica Yearbook 2016.
    This paper concentrates on how to capture harmony in sequent calculi. It starts by considering a proposal made by Tennant and some objections to it which have been presented by Steinberger. Then it proposes a different analysis which makes use of a double-line presentation of sequent calculi in the style of Dosen and it shows that this proposal is able to dismiss disharmonious operators without thereby adopting any global criterion.
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Inferentializing Consequence.Jaroslav Peregrin - unknown
    The proof of correctness and completeness of a logical calculus w.r.t. a given semantics can be read as telling us that the tautologies (or, more gen erally, the relation of consequence) specified in a model theoretic way can be equally well specified in a proof theoretic way, by means of the calculus (as the theorems, resp. the relation of inferability of the calculus). Thus we know that both for the classical propositional calculus and for the clas sical predicate calculus theorems (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  • Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
    The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  • Decision Methods for Linearly Ordered Heyting Algebras.Sara Negri & Roy Dyckhoff - 2005 - Archive for Mathematical Logic 45 (4):411-422.
    The decision problem for positively quantified formulae in the theory of linearly ordered Heyting algebras is known, as a special case of work of Kreisel, to be solvable; a simple solution is here presented, inspired by related ideas in Gödel-Dummett logic.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • An Ecumenical Notion of Entailment.Elaine Pimentel, Luiz Carlos Pereira & Valeria de Paiva - forthcoming - Synthese:1-23.
    Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Proof-Theoretic Pluralism.Filippo Ferrari & Eugenio Orlandelli - forthcoming - Synthese:1-25.
    Starting from a proof-theoretic perspective, where meaning is determined by the inference rules governing logical operators, in this paper we primarily aim at developing a proof-theoretic alternative to the model-theoretic meaning-invariant logical pluralism discussed in Beall and Restall. We will also outline how this framework can be easily extended to include a form of meaning-variant logical pluralism. In this respect, the framework developed in this paper—which we label two-level proof-theoretic pluralism—is much broader in scope than the one discussed in Beall (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Disentangling Structural Connectives or Life Without Display Property.Sergey Drobyshevich - 2019 - Journal of Philosophical Logic 48 (2):279-303.
    The work is concerned with the so called display property of display logic. The motivation behind it is discussed and challenged. It is shown using one display calculus for intuitionistic logic as an example that the display property can be abandoned without losing subformula, cut elimination and completeness properties in such a way that results in additional expressive power of the system. This is done by disentangling structural connectives so that they are no longer context-sensitive. A recipe for characterizing structural (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Are Uniqueness and Deducibility of Identicals the Same?Alberto Naibo & Mattia Petrolo - 2015 - Theoria 81 (2):143-181.
    A comparison is given between two conditions used to define logical constants: Belnap's uniqueness and Hacking's deducibility of identicals. It is shown that, in spite of some surface similarities, there is a deep difference between them. On the one hand, deducibility of identicals turns out to be a weaker and less demanding condition than uniqueness. On the other hand, deducibility of identicals is shown to be more faithful to the inferentialist perspective, permitting definition of genuinely proof-theoretical concepts. This kind of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • Book Reviews. [REVIEW]Roger Antonsen & Andreas Nakkerud - forthcoming - Studia Logica:1-4.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Infinitary Contraction‐Free Revenge.Andreas Fjellstad - 2018 - Thought: A Journal of Philosophy 7 (3):179-189.
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • General-Elimination Stability.Bruno Miguel Jacinto & Stephen Louis Read - 2017 - Studia Logica 105 (2):361-405.
    General-elimination harmony articulates Gentzen’s idea that the elimination-rules are justified if they infer from an assertion no more than can already be inferred from the grounds for making it. Dummett described the rules as not only harmonious but stable if the E-rules allow one to infer no more and no less than the I-rules justify. Pfenning and Davies call the rules locally complete if the E-rules are strong enough to allow one to infer the original judgement. A method is given (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • A Note on Decidability of Variables in Intuitionistic Propositional Logic.Katsumasa Ishii - 2018 - Mathematical Logic Quarterly 64 (3):183-184.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Paradox and Logical Revision. A Short Introduction.Julien Murzi & Massimiliano Carrara - 2015 - Topoi 34 (1):7-14.
    Logical orthodoxy has it that classical first-order logic, or some extension thereof, provides the right extension of the logical consequence relation. However, together with naïve but intuitive principles about semantic notions such as truth, denotation, satisfaction, and possibly validity and other naïve logical properties, classical logic quickly leads to inconsistency, and indeed triviality. At least since the publication of Kripke’s Outline of a theory of truth , an increasingly popular diagnosis has been to restore consistency, or at least non-triviality, by (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Classical Harmony and Separability.Julien Murzi - forthcoming - Erkenntnis:1-25.
    According to logical inferentialists, the meanings of logical expressions are fully determined by the rules for their correct use. Two key proof-theoretic requirements on admissible logical rules, harmony and separability, directly stem from this thesis—requirements, however, that standard single-conclusion and assertion-based formalizations of classical logic provably fail to satisfy :1035–1051, 2011). On the plausible assumption that our logical practice is both single-conclusion and assertion-based, it seemingly follows that classical logic, unlike intuitionistic logic, can’t be accounted for in inferentialist terms. In (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • Proof Theory in Philosophy of Mathematics.Andrew Arana - 2010 - Philosophy Compass 5 (4):336-347.
    A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  • Proof Analysis of Peirce’s Alpha System of Graphs.Minghui Ma & Ahti-Veikko Pietarinen - 2017 - Studia Logica 105 (3):625-647.
    Charles Peirce’s alpha system \ is reformulated into a deep inference system where the rules are given in terms of deep graphical structures and each rule has its symmetrical rule in the system. The proof analysis of \ is given in terms of two embedding theorems: the system \ and Brünnler’s deep inference system for classical propositional logic can be embedded into each other; and the system \ and Gentzen sequent calculus \ can be embedded into each other.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • A Simple Sequent Calculus for Angell’s Logic of Analytic Containment.Rohan French - 2017 - Studia Logica 105 (5):971-994.
    We give a simple sequent calculus presentation of R.B. Angell’s logic of analytic containment, recently championed by Kit Fine as a plausible logic of partial content.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations