Geodesic
Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
Bulletin of the Section of Logic, Tome 48 (2019) no. 2, pp. 137-158.

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: intuitionistic logic, existence predicate, sequent calculi, cut elimination, interpolation, Maehara's lemma 
@article{BSL_2019_48_2_a2,
     author = {Maffezioli, Paolo and Orlandelli, Eugenio},
     title = {Full {Cut} {Elimination} and {Interpolation} for {Intuitionistic} {Logic} with {Existence} {Predicate}},
     journal = {Bulletin of the Section of Logic},
     pages = {137--158},
     publisher = {mathdoc},
     volume = {48},
     number = {2},
     year = {2019},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2019_48_2_a2/}
}
TY  - JOUR
AU  - Maffezioli, Paolo
AU  - Orlandelli, Eugenio
TI  - Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
JO  - Bulletin of the Section of Logic
PY  - 2019
SP  - 137
EP  - 158
VL  - 48
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2019_48_2_a2/
LA  - en
ID  - BSL_2019_48_2_a2
ER  - 
%0 Journal Article
%A Maffezioli, Paolo
%A Orlandelli, Eugenio
%T Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
%J Bulletin of the Section of Logic
%D 2019
%P 137-158
%V 48
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2019_48_2_a2/
%G en
%F BSL_2019_48_2_a2
Maffezioli, Paolo; Orlandelli, Eugenio. Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate. Bulletin of the Section of Logic, Tome 48 (2019) no. 2, pp. 137-158. http://geodesic.mathdoc.fr/item/BSL_2019_48_2_a2/