Hypersequent Calculi for Intermediate Predicate Logics

Abstract

We report on the current status of our on-going project to develop well-behaved hypersequent calculi for intermediate predicate logics, such as the linearity axiom $\mathbf{LIN}:\left(\phi \to \psi \right)\vee \left(\psi \to \phi \right)$ and the constant domain axiom $\mathbf{CD}:\forall x\left(\phi \vee \psi \left(x\right)\right)\to \phi \vee \forall x\psi \left(x\right)$.