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
info:eu-repo/semantics/publishedVersion
 
Format application/pdf
 
Identifier https://czasopisma.uni.lodz.pl/bulletin/article/view/5441
10.18778/0138-0680.48.2.04
 
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
2449-836X
0138-0680
 
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

Twitter

Copyright © 2015-2018 Simon Fraser University Library