Inversion Principles and Introduction Rules

DOI10.1007/978-3-319-11041-7_8zbMath1429.03202OpenAlexW2117477628MaRDI QIDQ5213611

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

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

Related Items

Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules, Bilateral Rules as Complex Rules, Proof Terms for Generalized Natural Deduction, General-elimination stability, Deriving Natural Deduction Rules from Truth Tables, Single-assumption systems in proof-theoretic semantics, CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI, Normalisation and subformula property for a system of classical logic with Tarski's rule

Uses Software

• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on harmony
• General-elimination harmony and the meaning of the logical constants
• Connectives stranger than tonk
• On reduction rules, meaning-as-use, and proof-theoretic semantics
• Natural deduction with general elimination rules
• Harmony and autonomy in classical logic
• Varieties of linear calculi
• Meaning approached via proofs
• Gentzen's Proof of Normalization for Natural Deduction
• On Inversion Principles
• SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS
• A natural extension of natural deduction
• Is Even Minimal Negation Constructive?
• Identity and harmony
• THE SUBFORMULA PROPERTY IN CLASSICAL NATURAL DEDUCTION ESTABLISHED CONSTRUCTIVELY
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus
• A note on existential instantiation
• Die Vollständigkeit des Operatorensystems {¬, ∨, ⊃} für die Intuitionistische Aussagenlogik im Rahmen der Gentzensematik
• The consistency of arithmetics