General-Elimination Harmony and Higher-Level Rules

DOI10.1007/978-3-319-11041-7_13zbMath1429.03203OpenAlexW71761585MaRDI QIDQ5213616

Stephen Read

Publication date: 4 February 2020

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

Full work available at URL: https://doi.org/10.1007/978-3-319-11041-7_13

zbMATH Keywords

harmonyreductionflatteningintuitionistic logicnegationDummettclassical logicPrawitzGentzenlocal completenesshigher-level rules`tonk'generalized-elimination rules

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

TRANSLATIONS BETWEEN LINEAR AND TREE NATURAL DEDUCTION SYSTEMS FOR RELEVANT LOGICS ⋮ Proof-theoretic harmony: towards an intensional account ⋮ On harmony and permuting conversions ⋮ General-elimination stability ⋮ The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony ⋮ Subatomic natural deduction for a naturalistic first-order language with non-primitive identity ⋮ Prawitz, Proofs, and Meaning ⋮ Harmony in Proof-Theoretic Semantics: A Reductive Analysis ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus

Uses Software

• Pesca
• MiniML

Cites Work

• 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
• On the idea of a general proof theory
• Harmony and autonomy in classical logic
• Generalized definitional reflection and the inversion principle
• Meaning approached via proofs
• Validity concepts in proof-theoretic semantics
• A modal analysis of staged computation
• A natural extension of natural deduction
• Inferentialism and the categoricity problem: reply to Raatikainen
• Inferentialism, Logicism, Harmony, and a Counterpoint
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus

This page was built for publication: General-Elimination Harmony and Higher-Level Rules