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

DOI10.1007/S11225-021-09964-ZOpenAlexW3208162158MaRDI QIDQ2118979FDOQ2118979

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

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

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Cites Work

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

Cited In (3)

• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• On the Structure of Natural Deduction Derivations for “Generally”
• Title not available (Why is that?)

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)