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

DOI10.1007/S11225-021-09964-ZMaRDI QIDQ2118979zbMATH OpenOpenAlexFDO

Authors Paolo Pistone, Luca Tranchini, Mattia Petrolo

Publication date 23 March 2022

Published in Studia Logica (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

predicativitysecond-order logicpropositional quantificationidentity of proofsfinite polynomial functorpermutative conversionsRussell-Prawitz translation

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Recommendations

• The naturality of natural deduction
• Atomic polymorphism
• The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof
• Atomic polymorphism and the existence property
• A refined interpretation of intuitionistic logic by means of atomic polymorphism

Cites work

• scientific article; zbMATH DE number 3683840 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 65746 (Why is no real title available?)
• scientific article; zbMATH DE number 3630747 (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 3358455 (Why is no real title available?)
• A natural extension of natural deduction
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• Atomic polymorphism
• Comments on predicative logic
• Commuting conversions vs. the standard conversions of the ``good connectives
• Deciding equivalence with sums and the empty type
• Domain-free pure type systems
• Extensional Rewriting with Sums
• Finitely stratified polymorphism
• Functorial polymorphism
• Identity of Proofs Based on Normalization and Generality
• Instantiation overflow
• On flattening elimination rules
• Polynomial functors and polynomial monads
• Proof-theoretic harmony: towards an intensional account
• Semantical investigations in Heyting's intuitionistic logic
• Stabilizing quantum disjunction
• The Russell-Prawitz embedding and the atomization of universal instantiation
• The intuitionistic propositional calculus with quantifiers
• The naturality of natural deduction
• What’s Decidable About (Atomic) Polymorphism?
• \(\eta\)-conversions of IPC implemented in atomic F

Cited in

(3)

• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• On the Structure of Natural Deduction Derivations for “Generally”
• scientific article; zbMATH DE number 7577586 (Why is no real title available?)

This page was built for publication: The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

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