Nick Bezhanishvili, Silvio Ghilardi, Frederik Möllerström Lauridsen; One-step Heyting Algebras and Hypersequent Calculi with the Bounded Proof Property. J Logic Computation 2016 exw029. doi: 10.1093/logcom/exw029
We investigate proof-theoretic properties of hypersequent calculi for intermediate logics using algebraic methods. More precisely, we consider a new weakly analytic subformula property (the bounded proof property) of such calculi. Despite being strictly weaker than both cut-elimination and the subformula property, this property is sufficient to ensure decidability of finitely axiomatized calculi. We introduce one-step Heyting algebras and establish a semantic criterion characterizing calculi for intermediate logics with the bounded proof property and the finite model property in terms of one-step Heyting algebras. Finally, we show how this semantic criterion can be applied to a number of calculi for well-known intermediate logics such as and .