A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism

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.

This is a preview of subscription content, log in to check access.

References

  1. 1.

    Ferreira, F., Comments on predicative logic, Journal of Philosophical Logic 35:1–8, 2006.

    Article  Google Scholar 

  2. 2.

    Ferreira, F., and G. Ferreira, Commuting conversions vs. the standard conversions of the “good” connectives, Studia Logica 92:63–84, 2009.

    Article  Google Scholar 

  3. 3.

    Ferreira, F., and G. Ferreira, Atomic polymorphism, The Journal of Symbolic Logic 78(1):260–274, 2013.

    Article  Google Scholar 

  4. 4.

    Ferreira, G., Eta-conversions of \({\bf IPC}\) implemented in atomic \({\bf F}\), Logic Jnl IGPL 25(2):115–130, 2017.

    Google Scholar 

  5. 5.

    Ferreira, G., Rasiowa–Harrop disjunction property, Studia Logica 105(3):649–664, 2017.

    Article  Google Scholar 

  6. 6.

    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.

  7. 7.

    Girard, J-Y., Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, Cambridge, 1989.

    Google Scholar 

  8. 8.

    Kretz, M., On the treatment of predicative polymorphism in theories of explicit mathematics, Ph.D. thesis, Universitat Bern, 2002.

  9. 9.

    Leivant, D., A foundational delineation of poly-time, Information and Computation 110(2):391–420, 1994.

    Article  Google Scholar 

  10. 10.

    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.

  11. 11.

    Mitchell, J. C., Type systems for programming languages, in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, Elsevier, Amsterdam, 1990, pp. 365–458.

    Google Scholar 

  12. 12.

    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.

  13. 13.

    Plotkin, G., Call-by-name, call-by-value and the \(\lambda \)-calculus, Theoretical Computer Science 1:125–159, 1975.

    Article  Google Scholar 

  14. 14.

    Prawitz, D., Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm, 1965.

    Google Scholar 

  15. 15.

    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.

  16. 16.

    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.

Download references

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

Affiliations

Authors

Corresponding author

Correspondence to José Espírito Santo.

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

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation

Keywords

  • Atomic system F
  • Permutative conversion
  • Instantiation overflow