دورية أكاديمية

FULL CUT ELIMINATION AND INTERPOLATION FOR INTUITIONISTIC LOGIC WITH EXISTENCE PREDICATE.

التفاصيل البيبلوغرافية
العنوان: FULL CUT ELIMINATION AND INTERPOLATION FOR INTUITIONISTIC LOGIC WITH EXISTENCE PREDICATE.
المؤلفون: Maffezioli, Paolo, Orlandelli, Eugenio
المصدر: Bulletin of the Section of Logic; 2019, Vol. 48 Issue 2, p137-158, 22p
مصطلحات موضوعية: INTUITIONISTIC mathematics, INTERPOLATION, PREDICATE (Logic), SEQUENT calculus, DIRECT proof (Mathematics), IMPLICATION (Logic)
مستخلص: 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. [ABSTRACT FROM AUTHOR]
Copyright of Bulletin of the Section of Logic is the property of Bulletin of the Section of Logic and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
قاعدة البيانات: Complementary Index
الوصف
تدمد:01380680
DOI:10.18778/0138-0680.48.2.04