4 found
Order:
  1.  34
    The Naturality of Natural Deduction.Luca Tranchini, Paolo Pistone & Mattia Petrolo - 2019 - Studia Logica 107 (1):195-231.
    Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of NI\ is assumed to consist only of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  2.  40
    On Paradoxes in Normal Form.Mattia Petrolo & Paolo Pistone - 2019 - Topoi 38 (3):605-617.
    A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational interpretation of proofs and from the viewpoint of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  11
    Polymorphism and the Obstinate Circularity of Second Order Logic: A Victims’ Tale.Paolo Pistone - 2018 - Bulletin of Symbolic Logic 24 (1):1-52.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  4.  8
    The Naturality of Natural Deduction (II): On Atomic Polymorphism and Generalized Propositional Connectives.Paolo Pistone, Luca Tranchini & Mattia Petrolo - 2022 - Studia Logica 110 (2):545-592.
    In a previous paper we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models of polymorphic type theory. A different approach to extract proof-theoretic properties of natural deduction derivations was proposed in a recent series of papers on the basis of an embedding of intuitionistic propositional logic into a (...)
    Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark