Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

Paolo Maffezioli; Eugenio Orlandelli

doi:10.18778/0138-0680.48.2.04

Authors

Paolo Maffezioli Departamet de Filosofia, Universitat de Barcelona, Barcelona, Spain
Eugenio Orlandelli Dipartimento di Filosofia e Comunicazione, Universitá di Bologna, Bologna, Italy

DOI:

https://doi.org/10.18778/0138-0680.48.2.04

Keywords:

intuitionistic logic, existence predicate, sequent calculi, cut elimination, interpolation, Maehara's lemma

Abstract

In previous work by Baaz and Iemhoff, a Gentzen calculus for intuitionistic logic with existence predicate is presented that satisfies partial cut elimination and Craig's interpolation property; it is also conjectured that interpolation fails for the implication-free fragment. In this paper an equivalent calculus is introduced that satisfies full cut elimination and allows a direct proof of interpolation via Maehara's lemma. In this way, it is possible to obtain much simpler interpolants and to better understand and (partly) overcome the failure of interpolation for the implication-free fragment.

References

[1] M. Baaz and R. Iemhoff. On interpolation in existence logics, Logic for Programming, Articial Intelligence, and Reasoning ed. by G. Sutcliffe and A. Voronkov, vol. 3835 of Lecture Notes in Computer Science. Springer, 2005, pp. 697–711. https://doi.org/10.1007/11591191_48

Google Scholar

[2] M. Baaz and R. Iemhoff, Gentzen calculi for the existence predicate, Studia Logica, vol. 82, no. 1 (2006), pp. 7–23. https://doi.org/10.1007/s11225-006-6603-6

Google Scholar

[3] M. Beeson, Foundations of Constructive Mathematics. Springer, 1985. https://doi.org/10.1007/978-3-642-68952-9

Google Scholar

[4] G. Gherardi, P. Maffezioli, and E. Orlandelli, Interpolation in extensions of first-order logic, Studia Logica (2019), pp. 1–30. (published online). https://doi.org/10.1007/s11225-019-09867-0

Google Scholar

[5] S. Maehara, On the interpolation theorem of Craig. Suugaku, vol. 12 (1960), pp. 235–237. (in Japanese).

Google Scholar

[6] S. Negri, Contraction-free sequent calculi for geometric theories with an application to Barr's theorem, Archive for Mathematical Logic, vol. 42, no. 4 (2003), pp. 389–401. https://doi.org/10.1007/s001530100124

Google Scholar

[7] S. Negri, Proof analysis in modal logic, Journal of Philosophical Logic, vol. 34, no. (5-6) (2005), pp. 507–544. https://doi.org/10.1007/s10992-005-2267-3

Google Scholar

[8] S. Negri and J. von Plato, Structural Proof Theory. Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511527340

Google Scholar

[9] D. Scott, Identity and existence in intuitionistic logic. In M. Fourman, C. Mulvey, and D. Scott, editors, Application of Shaves. Springer, 1979, pp. 660–696. https://doi.org/10.1007/BFb0061839

Google Scholar

[10] A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory. Cambridge University Press, 2nd edition, 2000. https://doi.org/10.1017/CBO9781139168717

Google Scholar