Workshop on Correspondence and Canonicity in Non-Classical Logic
Title: One-step algebras and frames for intermediate logics (joint work with N. Bezhanishvili and S. Ghilardi)


Building on work by N. Bezhanishvili and S. Ghilardi we introduce one-step Heyting algebras and their dual one-step frames. We show how these can be used to characterize a certain weak analytic subformula property (the bounded proof property) of hypersequent calculi for intermediate logics. For concrete application we develop a basic ALBA-style calculus enabling us to compute first-order correspondents of hypersequent rules on one-step frames. Finally, we illustrate this semantic method by giving examples of hypersequent calculi for well-known intermediate logics with and without the bounded proof property.