The Naturality of Natural Deduction (II): On Atomic Polymorphism and Generalized Propositional Connectives

Autor(es)

Pistone, Paolo ^[1] ; Tranchini, Luca ^[2] ; Petrolo, Mattia ^[3]

Afiliação do(s) autor(es)

^[1] Univ Bologna, Dipartimento Informat Sci & Ingn, Bologna - Italy

^[2] Univ Tubingen, Wilhelm Schickard Inst, Tubingen - Germany

^[3] Univ Fed ABC, Ctr Ciencias Nat & Humanas, Sao Bernardo Do Campo - Brazil

• Tipo de documento: Artigo Científico
• Fonte: STUDIA LOGICA; OCT 2021.
• Citações Web of Science: 0

Resumo

In a previous paper (of which this is a prosecution) 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 predicative fragment of System F, called atomic System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification in terms of parametricity. (AU)

• Processo FAPESP: 16/25891-3 - Arbitrariedade e genericidade: ou sobre como falar do indizível
• Beneficiário: Giorgio Venturi
• Modalidade de apoio: Auxílio à Pesquisa - Jovens Pesquisadores