| Full text | |
| Author(s): |
Total Authors: 3
|
| Affiliation: | [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
Total Affiliations: 3
|
| Document type: | Journal article |
| Source: | STUDIA LOGICA; OCT 2021. |
| Web of Science Citations: | 0 |
| Abstract | |
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) | |
| FAPESP's process: | 16/25891-3 - Arbitrariness and genericity: or on how to speak of the unspeakable |
| Grantee: | Giorgio Venturi |
| Support Opportunities: | Research Grants - Young Investigators Grants |