General-elimination harmony and higher-level rules

DOI10.1007/978-3-319-11041-7_13zbMATH Open1429.03203OpenAlexW71761585MaRDI QIDQ5213616FDOQ5213616

Authors 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

harmonyDummettintuitionistic logicnegationreductionflatteningclassical logicPrawitzGentzenlocal completenesshigher-level rules`tonk'generalized-elimination rules

Mathematics Subject Classification ID

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

Recommendations

• General-elimination stability
• General-elimination harmony and the meaning of the logical constants
• A note on harmony
• HARMONISING HARMONY
• Classical harmony: Rules of inference and the meaning of the logical constants

Cites work

• scientific article; zbMATH DE number 5902347 (Why is no real title available?)
• scientific article; zbMATH DE number 3115105 (Why is no real title available?)
• scientific article; zbMATH DE number 3140506 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3062910 (Why is no real title available?)
• scientific article; zbMATH DE number 3076631 (Why is no real title available?)
• A modal analysis of staged computation
• A natural extension of natural deduction
• A note on harmony
• 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
• Generalized definitional reflection and the inversion principle
• Harmony and autonomy in classical logic
• Inferentialism and the categoricity problem: reply to Raatikainen
• Inferentialism, Logicism, Harmony, and a Counterpoint
• Meaning approached via proofs
• On the idea of a general proof theory
• Structural proof theory. With an appendix by Aarne Ranta
• Validity concepts in proof-theoretic semantics

Cited in

(16)

• TRANSLATIONS BETWEEN LINEAR AND TREE NATURAL DEDUCTION SYSTEMS FOR RELEVANT LOGICS
• Peano's Counterexample to Harmony
• Not so stable
• Classical harmony: Rules of inference and the meaning of the logical constants
• On flattening elimination rules
• A note on harmony
• General-elimination harmony and the meaning of the logical constants
• Some Remarks on Proof-Theoretic Semantics
• Prawitz, Proofs, and Meaning
• Proof-theoretic harmony: towards an intensional account
• On harmony and permuting conversions
• The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony
• Harmony in Proof-Theoretic Semantics: A Reductive Analysis
• General-elimination stability
• Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus

Describes a project that uses

Uses Software

• Pesca
• MiniML

This page was built for publication: General-elimination harmony and higher-level rules

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