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 (where these connectives are defined according to the Russell–Prawitz translation). 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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ferreira, F., Comments on predicative logic, Journal of Philosophical Logic 35:1–8, 2006.
Ferreira, F., and G. Ferreira, Commuting conversions vs. the standard conversions of the “good” connectives, Studia Logica 92:63–84, 2009.
Ferreira, F., and G. Ferreira, Atomic polymorphism, The Journal of Symbolic Logic 78(1):260–274, 2013.
Ferreira, G., Eta-conversions of \({\bf IPC}\) implemented in atomic \({\bf F}\), Logic Jnl IGPL 25(2):115–130, 2017.
Ferreira, G., Rasiowa–Harrop disjunction property, Studia Logica 105(3):649–664, 2017.
Ghani, N., \(\beta \eta \)-equality for coproducts, in Second International Conference on Typed Lambda Calculi and Applications, TLCA ’95, Edinburgh, UK, April 10–12, 1995, Proceedings, vol. 902 of Lecture Notes in Computer Science, Springer, 1995, pp. 171–185.
Girard, J-Y., Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, Cambridge, 1989.
Kretz, M., On the treatment of predicative polymorphism in theories of explicit mathematics, Ph.D. thesis, Universitat Bern, 2002.
Leivant, D., A foundational delineation of poly-time, Information and Computation 110(2):391–420, 1994.
Lindley, S., Extensional rewriting with sums, in Proc. of 8th International Conference on Typed Lambda Calculi and Applications, vol. 624 of Lecture Notes in Computer Science, Springer, 2007, pp. 255–271.
Mitchell, J. C., Type systems for programming languages, in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, Elsevier, Amsterdam, 1990, pp. 365–458.
Mitchell, J. C., and R. Harper, The essence of ML, in Proc. of the 15th ACM Symp. on Principles of Programming Languages, ACM, 1988, pp. 28–46.
Plotkin, G., Call-by-name, call-by-value and the \(\lambda \)-calculus, Theoretical Computer Science 1:125–159, 1975.
Prawitz, D., Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm, 1965.
Prawitz, D., Ideas and results in proof theory, in Proc. Second Scandinavian Logic Symposium, vol. 63 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1971, pp. 235–307.
Seely, R. A. G., Weak adjointness in proof theory, in Proc. of the Durham Conference on Applications of Sheaves, vol. 753 of Lecture Notes in Mathematics, Springer, 1979, pp. 697–701.
Acknowledgements
The first author acknowledges support from Fundação para a Ciência e a Tecnologia (FCT) through project UID/MAT/00013/2013. The second author acknowledges support from FCT through projects UID/MAT/04561/2019 and UID/CEC/00408/2019 and she is also grateful to Centro de Matemática, Aplicações Fundamentais e Investigação Operacional and to Large-Scale Informatics Systems Laboratory (Universidade de Lisboa).
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Presented by Heinrich Wansing
Rights and permissions
About this article
Cite this article
Espírito Santo, J., Ferreira, G. A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism. Stud Logica 108, 477–507 (2020). https://doi.org/10.1007/s11225-019-09858-1
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-019-09858-1