Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

Jurnal Perspektif Pembiayaan dan Pembangunan Daerah

View Publication Info
Field Value
Title Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate
Creator Maffezioli, Paolo
Orlandelli, Eugenio
Description 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.
Publisher Wydawnictwo Uniwersytetu Łódzkiego
Date 2019-06-30
Type info:eu-repo/semantics/article
Format application/pdf
Identifier https://czasopisma.uni.lodz.pl/bulletin/article/view/5441
Source Bulletin of the Section of Logic; Vol 48 No 2 (2019); 137-158
Bulletin of the Section of Logic; Tom 48 Nr 2 (2019); 137-158
Language eng
Relation https://czasopisma.uni.lodz.pl/bulletin/article/view/5441/5382
Rights http://creativecommons.org/licenses/by-nc-nd/4.0

Contact Us

The PKP Index is an initiative of the Public Knowledge Project.

For PKP Publishing Services please use the PKP|PS contact form.

For support with PKP software we encourage users to consult our wiki for documentation and search our support forums.

For any other correspondence feel free to contact us using the PKP contact form.

Find Us


Copyright © 2015-2018 Simon Fraser University Library