Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

DOI10.18778/0138-0680.48.2.04zbMath1477.03242OpenAlexW2974740209MaRDI QIDQ5241408

Eugenio Orlandelli, Paolo Maffezioli

Publication date: 31 October 2019

Published in: Bulletin of the Section of Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.18778/0138-0680.48.2.04

zbMATH Keywords

interpolationcut eliminationintuitionistic logicsequent calculiexistence predicateMaehara's lemma

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (6)

A more unified approach to free logics ⋮ Tableaux for free logics with descriptions ⋮ ABSTRACT FORMS OF QUANTIFICATION IN THE QUANTIFIED ARGUMENT CALCULUS ⋮ Neutral free logic: motivation, proof theory and models ⋮ Free logics are cut-free ⋮ Free Definite Description Theory – Sequent Calculi and Cut Elimination

Uses Software

• Pesca

Cites Work

• Proof analysis in modal logic
• Gentzen calculi for the existence predicate
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• Interpolation in extensions of first-order logic
• On Interpolation in Existence Logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate