Hypersequent Calculi for Intermediate Predicate Logics

TL;DR

This paper discusses the development of hypersequent calculi tailored for intermediate predicate logics, focusing on axioms like LIN and CD, aiming for well-behaved proof systems.

Contribution

It introduces new hypersequent calculi specifically designed for intermediate predicate logics with particular axioms, advancing proof-theoretic methods.

Findings

Development of hypersequent calculi for LIN and CD axioms

Establishment of well-behaved proof systems for these logics

Progress towards complete proof systems 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}\colon\left(\varphi\to\psi\right)\lor\left(\psi\to\varphi\right)$ and the constant domain axiom $\mathbf{CD}\colon\forall x\left(\varphi\lor\psi\left(x\right)\right)\to\varphi\lor\forall x\psi\left(x\right)$.