Natural deduction with general elimination rules

DOI10.1007/S001530100091zbMATH Open1021.03050OpenAlexW2060230835MaRDI QIDQ1407508FDOQ1407508

Authors: Jan von Plato 

Publication date: 16 September 2003

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001530100091

Recommendations

• Sequent calculus in natural deduction style
• scientific article; zbMATH DE number 1406467
• On structural inference rules for Gentzen-style natural deduction. I
• Translations from natural deduction to sequent calculus
• scientific article; zbMATH DE number 1302506

zbMATH Keywords

normalizationsequent calculusconjunction eliminationcut-free derivationderivations with cutsimplication eliminationstructure of derivations in natural deduction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Cited In (60)

• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• Which `intensional paradoxes' are paradoxes?
• Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules
• A faithful and quantitative notion of distant reduction for generalized applications
• Eight rules for implication elimination
• Bilateral inversion principles
• Proof Terms for Generalized Natural Deduction
• A framework for proof systems
• Strong normalization of classical natural deduction with disjunctions
• A note on harmony
• Does the implication elimination rule need a minor premise?
• General-elimination harmony and the meaning of the logical constants
• Normalisation and subformula property for a system of classical logic with Tarski's rule
• On the notion of canonical derivations from open assumptions and its role in proof-theoretic semantics
• A Sequent Systems without Improper Derivations
• Prawitz, Proofs, and Meaning
• The polarized \(\lambda\)-calculus
• Natural deduction bottom up
• Normal derivability in classical natural deduction
• Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications
• Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective)
• On flattening elimination rules
• Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization
• Inversion principles and introduction rules
• Meaning in use
• On structural inference rules for Gentzen-style natural deduction. I
• Translations from natural deduction to sequent calculus
• Semantic values for natural deduction derivations
• The \(\lambda \)-calculus and the unity of structural proof theory
• AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
• The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony
• Harmony in multiple-conclusion natural-deduction
• Sequent calculus in natural deduction style
• INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES
• Deriving natural deduction rules from truth tables
• The normalization theorem for extended natural deduction
• From Gentzen to Jaśkowski and back: algorithmic translation of derivations between the two main systems of natural deduction
• Normal derivations and sequent derivations
• Emptiness and discharge in sequent calculus and natural deduction
• Title not available (Why is that?)
• A new connective in natural deduction, and its application to quantum computing
• In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs
• Bilateralism in proof-theoretic semantics
• A logic inspired by natural language: quantifiers as subnectors
• Varieties of linear calculi
• Existential instantiation and normalization in sequent natural deduction
• Focusing in Linear Meta-logic
• Type checking and typability in domain-free lambda calculi
• On sequence-conclusion natural deduction systems
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus
• Cut elimination, substitution and normalisation
• An alternative natural deduction for the intuitionistic propositional logic
• A survey of nonstandard sequent calculi
• On the unity of duality
• Gentzen's proof systems: byproducts in a work of genius
• A cut-like inference in a framework of explicit composition for various calculi of natural deduction
• On harmony and permuting conversions
• Bilateral relevant logic
• Normal proofs, cut free derivations and structural rules
• A sequent calculus isomorphic to Gentzen's natural deduction

This page was built for publication: Natural deduction with general elimination rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1407508)