The naturality of natural deduction

DOI10.1007/s11225-017-9772-6OpenAlexW2510649957MaRDI QIDQ2631649

Paolo Pistone, Mattia Petrolo, Luca Tranchini

Publication date: 15 May 2019

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1607.06603

zbMATH Keywords

second order logicidentity of proofpermutative conversionsRussell-Prawitz translation$\eta $-conversiondinaturality conditionfunctorial interpretation

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Related Items (7)

General proof theory: introduction ⋮ Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics ⋮ Proof Nets, Coends and the Yoneda Isomorphism ⋮ Proof-theoretic harmony: towards an intensional account ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ Unnamed Item ⋮ The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

Cites Work

• Functorial polymorphism
• Commuting conversions vs. the standard conversions of the ``good connectives
• The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony
• Proof-theoretic harmony: towards an intensional account
• The Russell–Prawitz modality
• Extensional Rewriting with Sums
• A natural extension of natural deduction
• Atomic polymorphism
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The naturality of natural deduction