In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{semi-analytic}. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including $\mathsf{FL_e}$, $\mathsf{FL_{ew}}$, $\mathsf{CFL_e}$, $\mathsf{CFL_{ew}}$, and their $K$, $D$, and $T$-type modal extensions, as well as $\mathsf{CPC}$, $\mathsf{K}$, and $\mathsf{KD}$. However, its more striking consequence lies in the negative direction. It extends the negative results of \cite{Craig} to logics with CIP but without UIP. In particular, it shows that the modal logics $\mathsf{K4}$ and $\mathsf{S4}$ do not have a terminating semi-analytic calculus. \textbf{keywords:} Uniform interpolation, Sequent calculi, Substructural logics, Modal logics, Subexponential modalities

Abstract In this paper, a proof-theoretic method to prove uniform Lyndon interpolation (ULIP) for non-normal modal and conditional logics is introduced and applied to show that the logics, $\textsf{E}$, $\textsf{M}$, $\textsf{EN}$, $\textsf{MN}$, $\textsf{MC}$, $\textsf{K}$, and their conditional versions, $\textsf{CE}$, $\textsf{CM}$, $\textsf{CEN}$, $\textsf{CMN}$, $\textsf{CMC}$, $\textsf{CK}$, in addition to $\textsf{CKID}$ have that property. In particular, it implies that these logics have uniform interpolation (UIP). Although for some of them the latter is known, the fact that they have uniform LIP is new. Also, the proof-theoretic proofs of these facts are new, as well as the constructive way to explicitly compute the interpolants that they provide. On the negative side, it is shown that the logics $\textsf{CKCEM}$ and $\textsf{CKCEMID}$ enjoy UIP but not uniform LIP. Moreover, it is proved that the non-normal modal logics, $\textsf{EC}$ and $\textsf{ECN}$, and their conditional versions, $\textsf{CEC}$ and $\textsf{CECN}$, do not have Craig interpolation, and whence no uniform (Lyndon) interpolation.

Abstract One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in $\textrm{PA}+\bigcup _{\beta \prec \alpha } \textrm{TI}({\prec_{\beta}})$ , the extension of Peano arithmetic by transfinite induction up to the ordinals below $\alpha$ . Roughly speaking, we identify the functions as the ones that are computable by a sequence of $\textrm{PV}$ -provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below $\alpha$ , decreasing by the modifications. In the second part, and choosing $l \leq k$ , we use similar technique to capture the functions with bounded definitions in the theory $T^k_2$ (resp. $S^k_2$ ) as the functions computable by exponentially (resp. polynomially) long sequence of $\textrm{PV}_{k-l +1}$ -provable reductions between $l$ -turn games starting with an explicit $\textrm{PV}_{k-l +1}$ -provable winning strategy for the first game.