Results for 'introduction and elimination rules'

933 found
Order:
  1. A Categorical Approach To Higher-level Introduction And Elimination Rules.Haydee Poubel & Luiz Pereira - 1994 - Reports on Mathematical Logic:3-19.
    A natural extension of Natural Deduction was defined by Schroder-Heister where not only formulas but also rules could be used as hypotheses and hence discharged. It was shown that this extension allows the definition of higher-level introduction and elimination schemes and that the set $\{ \vee, \wedge, \rightarrow, \bot \}$ of intuitionist sentential operators forms a {\it complete} set of operators modulo the higher level introduction and elimination schemes, i.e., that any operator whose introduction (...)
     
    Export citation  
     
    Bookmark  
  2.  89
    Introduction and Elimination Rules vs. Equivalence Rules in Systems of Formal Logic.Deborah C. Smith - 2001 - Teaching Philosophy 24 (4):379-390.
    This paper argues that Lemmon-style proof systems (those that consist of only introduction and elimination inference rules) have several pedagogical benefits over Copi-style systems (those that make use of inference rules and equivalence rules). It is argued that Lemmon-style systems are easier to learn as they do not require memorizing as many rules, they do not require learning the subtle distinction between a rule of inference and a rule of replacement, and deriving material conditionals (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  3. Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules.Nils Kürbis - 2021 - Synthese 199 (5-6):14223-14248.
    This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  37
    Logical Revisionism: Logical Rules vs. Structural Rules.Fabrice Pataut - unknown
    As far as logic is concerned, the conclusion of Michael Dummett's manifestability argument is that intuitionistic logic, as first developed by Heyting, satisfies the semantic requirements of antirealism. The argument may be roughly sketched as follows: since we cannot manifest a grasp of possibly justification-transcendent truth conditions, we must countenance conditions which are such that, at least in principle and by the very nature of the case, we are able to recognize that they are satisfied whenever they are. Intuitionistic logic (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  5.  61
    Rules for subatomic derivation.Bartosz Więckowski - 2011 - Review of Symbolic Logic 4 (2):219-236.
    In proof-theoretic semantics the meaning of an atomic sentence is usually determined by a set of derivations in an atomic system which contain that sentence as a conclusion (see, in particular, Prawitz, 1971, 1973). The paper critically discusses this standard approach and suggests an alternative account which proceeds in terms of subatomic introduction and elimination rules for atomic sentences. A simple subatomic normal form theorem by which this account of the semantics of atomic sentences and the terms (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   22 citations  
  6.  43
    Structural Rules in Natural Deduction with Alternatives.Greg Restall - 2023 - Bulletin of the Section of Logic 52 (2):109-143.
    Natural deduction with alternatives extends Gentzen–Prawitz-style natural deduction with a single structural addition: negatively signed assumptions, called alternatives. It is a mildly bilateralist, single-conclusion natural deduction proof system in which the connective rules are unmodi_ed from the usual Prawitz introduction and elimination rules — the extension is purely structural. This framework is general: it can be used for (1) classical logic, (2) relevant logic without distribution, (3) affine logic, and (4) linear logic, keeping the connective (...) fixed, and varying purely structural rules. The key result of this paper is that the two principles that introduce kinds of irrelevance to natural deduction proofs: (a) the rule of explosion (from a contradiction, anything follows); and (b) the structural rule of vacuous discharge; are shown to be two sides of a single coin, in the same way that they correspond to the structural rule of weakening in the sequent calculus. The paper also includes a discussion of assumption classes, and how they can play a role in treating additive connectives in substructural natural deduction. (shrink)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  32
    (1 other version)Intelim rules for classical connectives.David C. Makinson - 2013 - In Sven Ove Hansson, David Makinson on Classical Methods for Non-Classical Problems. Dordrecht, Netherland: Springer. pp. 359-382.
    We investigate introduction and elimination rules for truth-functional connectives, focusing on the general questions of the existence, for a given connective, of at least one such rule that it satisfies, and the uniqueness of a connective with respect to the set of all of them. The answers are straightforward in the context of rules using general set/set sequents of formulae, but rather complex and asymmetric in the restricted (but more often used) context of set/formula sequents, as (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8. Intelim rules for classical connectives.Sven Ove Hansson - 2013 - In David Makinson on Classical Methods for Non-Classical Problems. Dordrecht, Netherland: Springer. pp. 359-382.
    We investigate introduction and elimination rules for truth-functional connectives, focusing on the general questions of the existence, for a given connective, of at least one such rule that it satisfies, and the uniqueness of a connective with respect to the set of all of them. The answers are straightforward in the context of rules using general set/set sequents of formulae, but rather complex and asymmetric in the restricted (but more often used) context of set/formula sequents, as (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  9. General-Elimination Stability.Bruno Jacinto & Stephen 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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  10.  90
    Natural deduction rules for English.Frederic B. Fitch - 1973 - Philosophical Studies 24 (2):89 - 104.
    A system of natural deduction rules is proposed for an idealized form of English. The rules presuppose a sharp distinction between proper names and such expressions as the c, a (an) c, some c, any c, and every c, where c represents a common noun. These latter expressions are called quantifiers, and other expressions of the form that c or that c itself, are called quantified terms. Introduction and elimination rules are presented for any, every, (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  11. A fundamental non-classical logic.Wesley Holliday - 2023 - Logics 1 (1):36-79.
    We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deduction system for the logic that contains only the introduction and elimination rules for the logical constants. From this starting point, if one adds the rule that Fitch called Reiteration, one obtains a proof system for intuitionistic logic in (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  12. A Note on Harmony.Nissim Francez & Roy Dyckhoff - 2012 - Journal of Philosophical Logic 41 (3):613-628.
    In the proof-theoretic semantics approach to meaning, harmony , requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature: 1. GE-harmony , requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony : imposes the existence of certain transformations of derivations, (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   36 citations  
  13.  11
    Introduction: Antipolitics or Antinomianism?Jeffrey M. Perl - 2023 - Common Knowledge 29 (3):317-323.
    In this introduction to part 3 of the Common Knowledge symposium “Antipolitics,” the journal's editor argues that, apart from sortition, the best guarantees of safety in a democracy are, first, to augment judicial oversight of all political processes and, second, to exclude politicians from the process of selecting judges. “There can never be too much judicial interference,” he writes, “in what politicians regard as their domain.” The author reached this conclusion during attempts by the newly elected Israeli government, in (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  14.  90
    Natural deduction with general elimination rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
    The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   58 citations  
  15. Decidability in Proof-Theoretic Validity.Will Stafford - 2022 - In Igor Sedlár, The Logica Yearbook 2021. College Publications. pp. 153-166.
    Proof-theoretic validity has proven a useful tool for proof-theoretic semantics, because it explains the harmony found in the introduction and elimination rules for the intuitionistic calculus. However, the demonstration that a rule of proof is proof-theoretically valid requires checking an infinite number of cases, which raises the question of whether proof-theoretic validity is decidable. It is proven here that it is for the most prominent formulations in the literature for propositional logic.
     
    Export citation  
     
    Bookmark  
  16.  41
    A classification of intersection type systems.M. W. Bunder - 2002 - Journal of Symbolic Logic 67 (1):353-368.
    The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in [6] that for both these (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  17. Does the Implication Elimination Rule Need a Minor Premise?Nissim Francez - 2018 - Logic and Logical Philosophy 27 (3):351-373.
    The paper introduces NJ g, a variant of Gentzen’s NJ natural deduction system, in which the implication elimination rule has no minor premise. The NJ g -systems extends traditional ND-system with a new kind of action in derivations, assumption incorporation, a kind of dual to the assumption discharge action. As a result, the implication (I/E)-rules are invertible and, almost by definition, harmonious and stable, a major condition imposed by proof-theoretic semantics on ND-systems to qualify as meaning-conferring. There is (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18.  76
    Implications-as-Rules vs. Implications-as-Links: An Alternative Implication-Left Schema for the Sequent Calculus. [REVIEW]Peter Schroeder-Heister - 2011 - Journal of Philosophical Logic 40 (1):95 - 101.
    The interpretation of implications as rules motivates a different left-introduction schema for implication in the sequent calculus, which is conceptually more basic than the implication-left schema proposed by Gentzen. Corresponding to results obtained for systems with higher-level rules, it enjoys the subformula property and cut elimination in a weak form.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  19.  49
    Common knowledge: finite calculus with syntactic cut-elimination procedure.Francesca Poggiolesi & Brian Hill - 2015 - Logique Et Analyse 58 (230):279-306.
    In this paper we present a finitary sequent calculus for the S5 multi-modal system with common knowledge. The sequent calculus is based on indexed hypersequents which are standard hypersequents refined with indices that serve to show the multi-agent feature of the system S5. The calculus has a non-analytic right introduction rule. We prove that the calculus is contraction- and weakening-free, that (almost all) its logical rules are invertible, and finally that it enjoys a syntactic cut-elimination procedure. Moreover, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  20.  36
    Elements of Combinatory Logic. [REVIEW]F. K. C. - 1975 - Review of Metaphysics 28 (3):552-553.
    Professor Fitch carefully guides the reader through the first and second chapters demonstrating how theorems of a sentential logic are truths about so-called Q-functions. These Q-functions are given by presenting symbols for twelve basic functions, specifying that finite combinations of these basic symbols give Q-functions, and by giving rules for the introduction of basic symbols into, and the elimination of basic symbols from, combinations of these symbols. The combinators are the basic symbols which are not symbols for (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  21. Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
    A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their single-succedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and sequent (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  22. The enduring scandal of deduction: is propositional logic really uninformative?Marcello D'Agostino & Luciano Floridi - 2009 - Synthese 167 (2):271-315.
    Deductive inference is usually regarded as being “tautological” or “analytical”: the information conveyed by the conclusion is contained in the information conveyed by the premises. This idea, however, clashes with the undecidability of first-order logic and with the (likely) intractability of Boolean logic. In this article, we address the problem both from the semantic and the proof-theoretical point of view. We propose a hierarchy of propositional logics that are all tractable (i.e. decidable in polynomial time), although by means of growing (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   60 citations  
  23. Grounding Grounding.Jon Erling Litland - 2017 - Oxford Studies in Metaphysics 10.
    The Problem of Iterated Ground is to explain what grounds truths about ground: if Γ grounds φ, what grounds that Γ grounds φ? This paper develops a novel solution to this problem. The basic idea is to connect ground to explanatory arguments. By developing a rigorous account of explanatory arguments we can equip operators for factive and non-factive ground with natural introduction and elimination rules. A satisfactory account of iterated ground falls directly out of the resulting logic: (...)
    Direct download  
     
    Export citation  
     
    Bookmark   63 citations  
  24.  48
    A Note on the v-Elimination Rule.Karl Pfeifer - 1990 - Cogito 4 (1):69-70.
    The paper reports that the explanations of the v-elimination rule in three commonly used introductory logic textbooks are misleading to students and can result in invalid inferences.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  25.  76
    ‘Conspiracy Theory’ as a Tonkish Term: Some Runabout Inference-Tickets from Truth to Falsehood.Charles Pigden - 2023 - Social Epistemology 37 (4):423-437.
    I argue that ‘conspiracy theory’ and ‘conspiracy theorist’ as commonly employed are ‘tonkish’ terms (as defined by Arthur Prior and Michael Dummett), licensing inferences from truths to falsehoods; indeed, that they are mega-tonkish terms, since their use is governed by different and competing sets of introduction and elimination rules, delivering different and inconsistent results. Thus ‘conspiracy theory’ and ‘conspiracy theorist’ do not have determinate extensions, which means that generalizations about conspiracy theories or conspiracy theorists do not have (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  26.  52
    Advances in Proof-Theoretic Semantics.Peter Schroeder-Heister & Thomas Piecha (eds.) - 2015 - Cham, Switzerland: Springer Verlag.
    This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed for almost 50 years, (...)
  27.  66
    A New Normalization Strategy for the Implicational Fragment of Classical Propositional Logic.Luiz C. Pereira, Edward H. Haeusler, Vaston G. Costa & Wagner Sanz - 2010 - Studia Logica 96 (1):95-108.
    The introduction and elimination rules for material implication in natural deduction are not complete with respect to the implicational fragment of classical logic. A natural way to complete the system is through the addition of a new natural deduction rule corresponding to Peirce's formula → A) → A). E. Zimmermann [6] has shown how to extend Prawitz' normalization strategy to Peirce's rule: applications of Peirce's rule can be restricted to atomic conclusions. The aim of the present paper (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  28.  74
    A Hypersequent Solution to the Inferentialist Problem of Modality.Andrew Parisi - 2022 - Erkenntnis 87 (4):1605-1633.
    The standard inferentialist approaches to modal logic tend to suffer from not being able to uniquely characterize the modal operators, require that introduction and elimination rules be interdefined, or rely on the introduction of possible-world like indexes into the object language itself. In this paper I introduce a hypersequent calculus that is flexible enough to capture many of the standard modal logics and does not suffer from the above problems. It is therefore an ideal candidate to (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  29. (1 other version)Bilateralism in Proof-Theoretic Semantics.Nissim Francez - 2013 - Journal of Philosophical Logic (2-3):1-21.
    The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between (positive) introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  30. A modal type theory for formalizing trusted communications.Giuseppe Primiero & Mariarosaria Taddeo - 2012 - Journal of Applied Logic 10 (1):92-114.
    This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  31. Inferentialist-Expressivism for Explanatory Vocabulary.Jared A. Millson, Kareem Khalifa & Mark Risjord - 2018 - In Ondřej Beran, Vojtěch Kolman & ‎Ladislav Koreň, From rules to meanings. New essays on inferentialism. New York, NY, USA: Routledge.
    In this essay, we extend earlier inferentialist-expressivist treatments of traditional logical, semantic, modal, and representational vocabulary (Brandom 1994, 2008, 2015; Peregrin 2014) to explanatory vocabulary. From this perspective, Inference to the Best Explanation (IBE) appears to be an obvious starting point. In its simplest formulation, IBE has the form: A best explains why B, B; so A. It thereby captures one of the central inferential features of explanation. An inferentialist-expressivist treatment of “best explains” would treat it as a logical operator. (...)
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  32.  51
    Models & Proofs: LFIs Without a Canonical Interpretations.Eduardo Alejandro Barrio - 2018 - Principia: An International Journal of Epistemology 22 (1):87-112.
    In different papers, Carnielli, W. & Rodrigues, A., Carnielli, W. Coniglio, M. & Rodrigues, A. and Rodrigues & Carnielli, present two logics motivated by the idea of capturing contradictions as conflicting evidence. The first logic is called BLE and the second—that is a conservative extension of BLE—is named LETJ. Roughly, BLE and LETJ are two non-classical logics in which the Laws of Explosion and Excluded Middle are not admissible. LETJ is built on top of BLE. Moreover, LETJ is a Logic (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  33. A natural extension of natural deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
    The framework of natural deduction is extended by permitting rules as assumptions which may be discharged in the course of a derivation. this leads to the concept of rules of higher levels and to a general schema for introduction and elimination rules for arbitrary n-ary sentential operators. with respect to this schema, (functional) completeness "or", "if..then" and absurdity is proved.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   106 citations  
  34.  22
    On an Ecumenical Natural Deduction with Stoup. Part I: The Propositional Case.Luiz Carlos Pereira & Elaine Pimentel - 2024 - In Antonio Piccolomini D'Aragona, Perspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction. Springer Verlag. pp. 139-169.
    In 2015 Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In his ecumenical system, Prawitz recovers the harmony of rules, but the rules for the classical operators do not satisfy separability. In fact, the classical rules are not pure, in the sense that negation is used in the definition of the introduction and elimination rules for the classical operators. In this work we (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  35. How To Precisify Quantifiers.Arvid Båve - 2011 - Journal of Philosophical Logic 40 (1):103-111.
    I here argue that Ted Sider's indeterminacy argument against vagueness in quantifiers fails. Sider claims that vagueness entails precisifications, but holds that precisifications of quantifiers cannot be coherently described: they will either deliver the wrong logical form to quantified sentences, or involve a presupposition that contradicts the claim that the quantifier is vague. Assuming (as does Sider) that the “connectedness” of objects can be precisely defined, I present a counter-example to Sider's contention, consisting of a partial, implicit definition of the (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  36.  45
    On the strength of dependent products in the type theory of Martin-Löf.Richard Garner - 2009 - Annals of Pure and Applied Logic 160 (1):1-12.
    One may formulate the dependent product types of Martin-Löf type theory either in terms of abstraction and application operators like those for the lambda-calculus; or in terms of introduction and elimination rules like those for the other constructors of type theory. It is known that the latter rules are at least as strong as the former: we show that they are in fact strictly stronger. We also show, in the presence of the identity types, that the (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  37. Tonk- A Full Mathematical Solution.Arnon Avron - unknown
    There is a long tradition (See e.g. [9, 10]) starting from [12], according to which the meaning of a connective is determined by the introduction and elimination rules which are associated with it. The supporters of this thesis usually have in mind natural deduction systems of a certain ideal type (explained in Section 3 below). Unfortunately, already the handling of classical negation requires rules which are not of that type. This problem can be solved in the (...)
     
    Export citation  
     
    Bookmark   5 citations  
  38.  82
    New Foundations for a Relational Theory of Theory-revision.Neil Tennant - 2006 - Journal of Philosophical Logic 35 (5):489-528.
    AGM-theory, named after its founders Carlos Alchourrón, Peter Gärdenfors and David Makinson, is the leading contemporary paradigm in the theory of belief-revision. The theory is reformulated here so as to deal with the central relational notions 'J is a contraction of K with respect to A' and 'J is a revision of K with respect to A'. The new theory is based on a principal-case analysis of the domains of definition of the three main kinds of theory-change (expansion, contraction and (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  39. What does '&' mean?Axel Arturo Barceló Aspeitia - 2007 - The Proceedings of the Twenty-First World Congress of Philosophy 5:45-50.
    Using conjunction as an example, I show a technical and philosophical problem when trying to conciliate the currently prevailing views on the meaning of logical connectives: the inferientialist (also called 'syntactic') one based on introduction and elimination rules, and the representationalist (also called 'semantic') one given through truth tables. Mostly I show that the widespread strategy of using the truth theoretical definition of logical consequence to collapse both definitions must be rejected by inferentialists. An important consequence of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  40. Jan Dullaert of Ghent on the Foundations of Propositional Logic.Miroslav Hanke - 2017 - Vivarium 55 (4):273-306.
    _ Source: _Volume 55, Issue 4, pp 273 - 306 Jan Dullaert was a direct student of John Mair and a teacher of Gaspar Lax, Juan de Celaya, and Juan Luis Vives. His commentary on Aristotle’s _Peri Hermeneias_ addresses the foundations of propositional logic, including a detailed analysis of conditionals and the semantics of logical connectives. Dullaert’s propositional logic is limited to the immediate implications of the semantics of these connectives, i.e., their introduction and elimination rules. In (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  41.  82
    Introducing Identity.Owen Griffiths & Arif Ahmed - 2021 - Journal of Philosophical Logic 50 (6):1449-1469.
    The best-known syntactic account of the logical constants is inferentialism. Following Wittgenstein’s thought that meaning is use, inferentialists argue that meanings of expressions are given by introduction and elimination rules. This is especially plausible for the logical constants, where standard presentations divide inference rules in just this way. But not just any rules will do, as we’ve learnt from Prior’s famous example of tonk, and the usual extra constraint is harmony. Where does this leave identity? (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42.  85
    Connectives stranger than tonk.Heinrich Wansing - 2006 - Journal of Philosophical Logic 35 (6):653 - 660.
    Many logical systems are such that the addition of Prior's binary connective tonk to them leads to triviality, see [1, 8]. Since tonk is given by some introduction and elimination rules in natural deduction or sequent rules in Gentzen's sequent calculus, the unwanted effects of adding tonk show that some kind of restriction has to be imposed on the acceptable operational inferences rules, in particular if these rules are regarded as definitions of the operations (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   15 citations  
  43. Peter.milne@stir.ac.Uk.ProfPeter Milne - unknown
    In natural deduction classical logic is commonly formulated by adding a rule such as Double Negation Elimination (DNE) or Classical Reductio ad Absurdum (CRA) to a set of introduction and elimination rules sufficient for intuitionist first-order logic with conjunction, disjunction, implication, negation and the universal and existential quantifiers all taken as primitive. The natural deduction formulation of intuitionist logic, coming from Gentzen, has nice properties:— (i) the separation property: an intuitionistically valid inference is derivable using only (...)
     
    Export citation  
     
    Bookmark  
  44.  17
    Rule-Elimination Theorems.Sayantan Roy - 2024 - Logica Universalis 18 (3):355-393.
    Cut-elimination theorems constitute one of the most important classes of theorems of proof theory. Since Gentzen’s proof of the cut-elimination theorem for the system LK, several other proofs have been proposed. Even though the techniques of these proofs can be modified to sequent systems other than LK\textbf{LK}, they are essentially of a very particular nature; each of them describes an algorithm to transform a given proof to a cut-free proof. However, due to its reliance on heavy syntactic arguments (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  45. (1 other version)Against Harmony.Ian Rumfitt - 1995 - In B. Hale & Crispin Wright, Blackwell Companion to the Philosophy of Language. Blackwell.
    Many prominent writers on the philosophy of logic, including Michael Dummett, Dag Prawitz, Neil Tennant, have held that the introduction and elimination rules of a logical connective must be ‘in harmony ’ if the connective is to possess a sense. This Harmony Thesis has been used to justify the choice of logic: in particular, supposed violations of it by the classical rules for negation have been the basis for arguments for switching from classical to intuitionistic logic. (...)
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  46.  65
    Truth table logic, with a survey of embeddability results.Neil Tennant - 1989 - Notre Dame Journal of Formal Logic 30 (3):459-484.
    Kalrnaric. We set out a system T, consisting of normal proofs constructed by means of elegantly symmetrical introduction and elimination rules. In the system T there are two requirements, called ( ) and ()), on applications of discharge rules. T is sound and complete for Kalmaric arguments. ( ) requires nonvacuous discharge of assumptions; ()) requires that the assumption discharged be the sole one available of highest degree. We then consider a 'Duhemian' extension T*, obtained simply (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  47.  77
    El Significado de la Negación Paraconsistente.Gladys Palau & Cecilia Duran - 2009 - Principia: An International Journal of Epistemology 13 (3):357-370.
    This work agrees and supports the I. Hacking’s thesis regarding the meaningof the logical constants accordingly with Gentzen’s Introduction and Elimination Rules of Sequent Calculus, corresponding with the abstract conception of the notion of logical consequence. We would like to ask for the minimum rules that must satisfy a connective in order to be considered as a genuine negation. Mainly, we will refer to both da Costa’s C-Systems and Priest’s LP system. Finally, we will analyze the (...)
    No categories
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  48.  68
    Cut elimination for a calculus with context-dependent rules.Birgit Elbl - 2001 - Archive for Mathematical Logic 40 (3):167-188.
    Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  49. Introduction: Symposium on Paul Gowder, the rule of law in the real world.Matthew J. Lister - 2018 - St. Louis University Law Journal 62 (2):287-91.
    This is a short introduction to a book symposium on Paul Gowder's recent book, _The Rule of Law in thee Real World_ (Cambridge University Press, 2016). The book symposium will appear in the St. Luis University Law Journal, 62 St. Louis U. L.J., -- (2018), with commentaries on Gowder's book by colleen Murphy, Robin West, Chad Flanders, and Matthew Lister, along with replies by Paul Gowder.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  50. (1 other version)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 to (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
1 — 50 / 933