The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

DOI10.1007/s11225-021-09964-zOpenAlexW3208162158MaRDI QIDQ2118979

Paolo Pistone, Mattia Petrolo, Luca Tranchini

Publication date: 23 March 2022

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

Full work available at URL: https://doi.org/10.1007/s11225-021-09964-z

zbMATH Keywords

propositional quantificationsecond-order logicpredicativityidentity of proofsfinite polynomial functorpermutative conversionsRussell-Prawitz translation

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Related Items

Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Functorial polymorphism
• Commuting conversions vs. the standard conversions of the ``good connectives
• The intuitionistic propositional calculus with quantifiers
• Semantical investigations in Heyting's intuitionistic logic
• Finitely stratified polymorphism
• Stabilizing quantum disjunction
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• Comments on predicative logic
• The naturality of natural deduction
• Proof-theoretic harmony: towards an intensional account
• ON FLATTENING ELIMINATION RULES
• Extensional Rewriting with Sums
• A natural extension of natural deduction
• η-conversions of IPC implemented in atomic F
• Identity of Proofs Based on Normalization and Generality
• Domain-free pure type systems
• Polynomial functors and polynomial monads
• Atomic polymorphism
• The Russell-Prawitz embedding and the atomization of universal instantiation
• Deciding equivalence with sums and the empty type
• What’s Decidable About (Atomic) Polymorphism?