Switch to: Citations

References in:

Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate

Paolo Maffezioli & Eugenio Orlandelli

Bulletin of the Section of Logic 48 (2):137-158 (2019)

Add references

You must login to add references.

Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.details A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems. Download Export citation Bookmark 104 citations
Contraction-free sequent calculi for geometric theories with an application to Barr's theorem.Sara Negri - 2003 - Archive for Mathematical Logic 42 (4):389-401.details Geometric theories are presented as contraction- and cut-free systems of sequent calculi with mathematical rules following a prescribed rule-scheme that extends the scheme given in Negri and von Plato. Examples include cut-free calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable. Download Export citation Bookmark 37 citations
Gentzen Calculi for the Existence Predicate.Matthias Baaz & Rosalie Iemhoff - 2006 - Studia Logica 82 (1):7-23.details We introduce Gentzen calculi for intuitionistic logic extended with an existence predicate. Such a logic was first introduced by Dana Scott, who provided a proof system for it in Hilbert style. We prove that the Gentzen calculus has cut elimination in so far that all cuts can be restricted to very simple ones. Applications of this logic to Skolemization, truth value logics and linear frames are also discussed. Download Export citation Bookmark 7 citations

1