Studia Logica 110 (2):545-592 (2022)

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 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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s11225-021-09964-z
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Translate to english
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,172
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Proofs and Types.Jean-Yves Girard - 1989 - Cambridge University Press.
A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
Identity of Proofs Based on Normalization and Generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.

View all 13 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Expressive Power and Incompleteness of Propositional Logics.James W. Garson - 2010 - Journal of Philosophical Logic 39 (2):159-171.
Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
Neighbourhood Semantics and Generalized Kripke Models.Bernd Dahn - 1976 - Bulletin of the Section of Logic 5 (1):2-7.
A Binary-Conclusion Natural Deduction System.K. Fujita - 1999 - Logic Journal of the IGPL 7 (4):517-545.
On Quine's Approach to Natural Deduction'.Carlo Cellucci - 1995 - In Paolo Leonardi & Marco Santambrogio (eds.), On Quine: New Essays. Cambridge University Press. pp. 314--335.


Added to PP index

Total views
9 ( #954,194 of 2,517,876 )

Recent downloads (6 months)
1 ( #409,482 of 2,517,876 )

How can I increase my downloads?


My notes