Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
Discussiones Mathematicae Graph Theory, Tome 48 (2019) no. 2.

Voir la notice de l'article dans 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.
Mots-clés : intuitionistic logic, existence predicate, sequent calculi, cut elimination, interpolation, Maehara's lemma 
@article{DMGT_2019_48_2_a2,
     author = {Maffezioli, Paolo and Orlandelli, Eugenio},
     title = {Full {Cut} {Elimination} and {Interpolation} for {Intuitionistic} {Logic} with {Existence} {Predicate}},
     journal = {Discussiones Mathematicae Graph Theory},
     publisher = {mathdoc},
     volume = {48},
     number = {2},
     year = {2019},
     language = {en},
     url = {https://geodesic-test.mathdoc.fr/item/DMGT_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  - Discussiones Mathematicae Graph Theory
PY  - 2019
VL  - 48
IS  - 2
PB  - mathdoc
UR  - https://geodesic-test.mathdoc.fr/item/DMGT_2019_48_2_a2/
LA  - en
ID  - DMGT_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 Discussiones Mathematicae Graph Theory
%D 2019
%V 48
%N 2
%I mathdoc
%U https://geodesic-test.mathdoc.fr/item/DMGT_2019_48_2_a2/
%G en
%F DMGT_2019_48_2_a2
Maffezioli, Paolo; Orlandelli, Eugenio. Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate. Discussiones Mathematicae Graph Theory, Tome 48 (2019) no. 2. https://geodesic-test.mathdoc.fr/item/DMGT_2019_48_2_a2/