Uniform interpolation and the existence of sequent calculi |
| |
Authors: | Rosalie Iemhoff |
| |
Institution: | Utrecht University, Janskerkhof 13, 3512 BL, the Netherlands |
| |
Abstract: | This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of and (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus. |
| |
Keywords: | 03B45 03B55 03B62 03F03 03F07 Uniform interpolation Sequent calculus Intermediate logic Intuitionistic modal logic Propositional quantifiers |
本文献已被 ScienceDirect 等数据库收录! |
|