Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

Maffezioli, Paolo; Orlandelli, Eugenio

doi:10.18778/0138-0680.48.2.04

Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

Maffezioli, Paolo
Orlandelli, Eugenio

Aldizkaria:

Bulletin of the Section of Logic

ISSN: 2449-836X, 0138-0680

Argitalpen urtea: 2019

Alea: 48

Zenbakia: 2

Orrialdeak: 137-158

Mota: Artikulua

DOI: 10.18778/0138-0680.48.2.04 GOOGLE SCHOLAR Sarbide irekia editor

Beste argitalpen batzuk: Bulletin of the Section of Logic

Laburpena

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.