A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism

Studia Logica:1-31 (forthcoming)

Abstract
We study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity. As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic content is made explicit, both for the alternative and the original embeddings. The investigation of preservation of proof-reduction steps by the alternative embedding enables the analysis of generation of “administrative” redexes. These are the key, on the one hand, to understand the difference between the two embeddings; on the other hand, to understand whether the final word on the embedding of IPC into atomic system F has been said.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s11225-019-09858-1
Options
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: 44,340
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

Natural Deduction: A Proof-Theoretical Study.Dag Prawitz - 1965 - Journal of Symbolic Logic 32 (2):255-256.
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.
Rasiowa–Harrop Disjunction Property.Gilda Ferreira - 2017 - Studia Logica 105 (3):649-664.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
Atomic Polymorphism and the Existence Property.Gilda Ferreira - 2018 - Annals of Pure and Applied Logic 169 (12):1303-1316.
On an Intuitionistic Logic for Pragmatics.Gianluigi Bellin, Massimiliano Carrara & Daniele Chiffi - 2018 - Journal of Logic and Computation 50 (28):935–966..
Implicit Versus Explicit Knowledge in Dialogical Logic.Manuel Rebuschi - 2009 - In Ondrej Majer, Ahti-Veikko Pietarinen & Tero Tulenheimo (eds.), Games: Unifying Logic, Language, and Philosophy. Springer Verlag. pp. 229--246.
Towards Intuitionistic Dynamic Logic.J. W. Degen & J. M. Werner - 2006 - Logic and Logical Philosophy 15 (4):305-324.
Η- Conversions of IPC Implemented in Atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.
Intuitionistic Completeness for First Order Classical Logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.
Bi-Simulating in Bi-Intuitionistic Logic.Guillermo Badia - 2016 - Studia Logica 104 (5):1037-1050.
Intuitionistic Completeness for First Order Classical Logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.

Analytics

Added to PP index
2019-03-27

Total views
6 ( #956,727 of 2,271,536 )

Recent downloads (6 months)
1 ( #826,846 of 2,271,536 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature