ON FLATTENING ELIMINATION RULES

DOI10.1017/S1755020313000385zbMath1329.03087MaRDI QIDQ2940866

Grigory K. Olkhovikov, Peter Schroeder-Heister

Publication date: 21 January 2015

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

zbMATH Keywords

intuitionistic logicintroduction rulesflat elimination rulessecond-order propositional logic

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

SEMANTIC POLLUTION AND SYNTACTIC PURITY ⋮ Proof-theoretic harmony: towards an intensional account ⋮ General-elimination stability ⋮ Harmony in multiple-conclusion natural-deduction ⋮ The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony ⋮ Harmony in Proof-Theoretic Semantics: A Reductive Analysis ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus ⋮ A Poly-Connexive Logic ⋮ The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on harmony
• General-elimination harmony and the meaning of the logical constants
• Natural deduction with general elimination rules
• A natural extension of natural deduction
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• Die Vollständigkeit des Operatorensystems {¬, ∨, ⊃} für die Intuitionistische Aussagenlogik im Rahmen der Gentzensematik