The Faithfulness of Fat: A Proof-Theoretic Proof

Studia Logica 103 (6):1303-1311 (2015)

It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system F at, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the intuitionistic propositional logic in which commuting conversions are not needed
Keywords Predicative polymorphism  Faithfulness  Natural deduction  Strong normalization  Intuitionistic propositional calculus  Disjunction property
Categories (categorize this paper)
DOI 10.1007/s11225-015-9620-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 45,727
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

Comments on Predicative Logic.Fernando Ferreira - 2006 - Journal of Philosophical Logic 35 (1):1-8.
Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.

Add more references

Citations of this work BETA

Η- Conversions of IPC Implemented in Atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.

Add more citations

Similar books and articles

Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
A Proof-Theoretic Investigation of a Logic of Positions.Stefano Baratella & Andrea Masini - 2003 - Annals of Pure and Applied Logic 123 (1-3):135-162.
Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.
A New Solution to a Problem of Hosoi and Ono.Michael Zakharyaschev - 1994 - Notre Dame Journal of Formal Logic 35 (3):450-457.
Linearizing Intuitionistic Implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
An Approach to Infinitary Temporal Proof Theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.


Added to PP index

Total views
14 ( #614,971 of 2,281,035 )

Recent downloads (6 months)
3 ( #421,058 of 2,281,035 )

How can I increase my downloads?


My notes

Sign in to use this feature