Universal Proof Theory: Semi-analytic Rules and Craig Interpolation

In [6], Iemhoff introduced the notion of a focused axiom and a focused rule as the building blocks for a certain form of sequent calculus which she calls a focused proof system. She then showed how the existence of a terminating focused system implies the uniform interpolation property for the logic that the calculus captures. In this paper we first generalize her focused rules to semi-analytic rules, a dramatically powerful generalization, and then we will show how the semi-analytic calculi consisting of these rules together with our generalization of her focused axioms, lead to the feasible Craig interpolation property. Using this relationship, we first present a uniform method to prove interpolation for different logics from sub-structural logics $\mathbf{FL_e}$, $\mathbf{FL_{ec}}$, $\mathbf{FL_{ew}}$ and $\mathbf{IPC}$ to their appropriate classical and modal extensions, including the intuitionistic and classical linear logics. Then we will use our theorem negatively, first to show that so many sub-structural logics including $\L_n$, $G_n$, $BL$, $R$ and $RM^e$ and almost all super-intutionistic logics (except at most seven of them) do not have a semi-analytic calculus. To investigate the case that the logic actually has the Craig interpolation property, we will first define a certain specific type of semi-analytic calculus which we call PPF systems and we will then present a sound and complete PPF calculus for classical logic. However, we will show that all such PPF calculi are exponentially slower than the classical Hilbert-style proof system (or equivalently $\mathbf{LK+Cut}$). We will then present a similar exponential lower bound for a certain form of complete PPF calculi, this time for any super-intuitionistic logic.Comment: 45 page