Inversion principles and introduction rules

DOI10.1007/978-3-319-11041-7_8zbMATH Open1429.03202OpenAlexW2117477628MaRDI QIDQ5213611FDOQ5213611

Authors Peter Milne

Publication date 4 February 2020

Published in Dag Prawitz on Proofs and Meaning (Search for Journal in Brave)

Full work available at URL http://www.springer.com/us/book/9783319110400

zbMATH Keywords

sequent calculuselimination rulesintroduction rulesinversion principlegeneral elimination rules

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07)

Recommendations

• On Inversion Principles
• Generalized definitional reflection and the inversion principle
• INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES
• Intelim rules for classical connectives
• Inferring, splicing, and the Stoic analysis of argument

Cites work

• scientific article; zbMATH DE number 3125691 (Why is no real title available?)
• scientific article; zbMATH DE number 3758289 (Why is no real title available?)
• scientific article; zbMATH DE number 43055 (Why is no real title available?)
• scientific article; zbMATH DE number 3630747 (Why is no real title available?)
• scientific article; zbMATH DE number 1478228 (Why is no real title available?)
• scientific article; zbMATH DE number 3895056 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• A natural extension of natural deduction
• A note on existential instantiation
• A note on harmony
• Connectives stranger than tonk
• Die Vollständigkeit des Operatorensystems {¬, ∨, ⊃} für die Intuitionistische Aussagenlogik im Rahmen der Gentzensematik
• General-elimination harmony and the meaning of the logical constants
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus
• Gentzen's Proof of Normalization for Natural Deduction
• Harmony and autonomy in classical logic
• Identity and harmony
• Inferring, splicing, and the Stoic analysis of argument
• Is Even Minimal Negation Constructive?
• Meaning approached via proofs
• Natural deduction with general elimination rules
• On Inversion Principles
• On reduction rules, meaning-as-use, and proof-theoretic semantics
• Structural proof theory. With an appendix by Aarne Ranta
• Subformula and separation properties in natural deduction via small Kripke models
• THE SUBFORMULA PROPERTY IN CLASSICAL NATURAL DEDUCTION ESTABLISHED CONSTRUCTIVELY
• The consistency of arithmetics
• Varieties of linear calculi

Cited in

(13)

• Bilateral inversion principles
• Normalisation and subformula property for a system of classical logic with Tarski's rule
• Inverse rules of ECA with rule number 150
• Bilateral Rules as Complex Rules
• Single-assumption systems in proof-theoretic semantics
• INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES
• On Inversion Principles
• Deriving natural deduction rules from truth tables
• Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules
• Intelim rules for classical connectives
• General-elimination stability
• Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi
• Proof Terms for Generalized Natural Deduction

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Inversion principles and introduction rules

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