Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

Paolo Maffezioli; Eugenio Orlandelli

Bulletin of the Section of Logic (2019)

  • Volume: 48, Issue: 2, page 137-158
  • ISSN: 0138-0680

Abstract

top
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.

How to cite

top

Paolo Maffezioli, and Eugenio Orlandelli. "Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate." Bulletin of the Section of Logic 48.2 (2019): 137-158. <http://eudml.org/doc/295600>.

@article{PaoloMaffezioli2019,
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.},
author = {Paolo Maffezioli, Eugenio Orlandelli},
journal = {Bulletin of the Section of Logic},
keywords = {intuitionistic logic; existence predicate; sequent calculi; cut elimination; interpolation; Maehara's lemma},
language = {eng},
number = {2},
pages = {137-158},
title = {Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate},
url = {http://eudml.org/doc/295600},
volume = {48},
year = {2019},
}

TY - JOUR
AU - Paolo Maffezioli
AU - Eugenio Orlandelli
TI - Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
JO - Bulletin of the Section of Logic
PY - 2019
VL - 48
IS - 2
SP - 137
EP - 158
AB - 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.
LA - eng
KW - intuitionistic logic; existence predicate; sequent calculi; cut elimination; interpolation; Maehara's lemma
UR - http://eudml.org/doc/295600
ER -

References

top
  1. [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  
  2. [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  
  3. [3] M. Beeson, Foundations of Constructive Mathematics. Springer, 1985. https://doi.org/10.1007/978-3-642-68952-9  
  4. [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  
  5. [5] S. Maehara, On the interpolation theorem of Craig. Suugaku, vol. 12 (1960), pp. 235–237. (in Japanese). 
  6. [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  
  7. [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  
  8. [8] S. Negri and J. von Plato, Structural Proof Theory. Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511527340  
  9. [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  
  10. [10] A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory. Cambridge University Press, 2nd edition, 2000. https://doi.org/10.1017/CBO9781139168717  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.