The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
From MaRDI portal
Publication:2118979
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
propositional quantificationsecond-order logicpredicativityidentity of proofsfinite polynomial functorpermutative conversionsRussell-Prawitz translation
Related Items
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?
