Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
Paolo Maffezioli, Eugenio Orlandelli (2019)
Bulletin of the Section of Logic
Similarity:
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...