R. Kuznets, B. Lellmann:

"Translating Quantitative Semantic Bounds into Nested Sequents";

Talk: Fifth TICAMORE MEETING, Wien (invited); 2019-11-11 - 2019-11-13.

As follows from their name, tree-hypersequents (also known as nested sequents) were created to represent the tree structure of underlying Kripke models. While this approach works well on modal and intermediate logics complete w.r.t. many types of tree-like frames, it is not directly suited to encode quantitative restrictions on these frames, e.g., bounded depth and/or bounded number of children per node. In order to capture these restrictions, we add the injectivity condition to nested sequents requiring different sequent nodes to correspond to distinct worlds in the underlying Kripke model. The downside is the loss of the formula interpretation. On the plus side, we show how the injective nested sequents can be used to constructively prove the Craig interpolation property for all interpolable intermediate logics strictly between the intuitionistic and classical propositional logics that are complete with respect to tree-like models, i.e., Smetanich logic (also known as the logic of here and there), the greatest semiconstructive logic, logic BD_2 of bounded depth 2, and Gödel logic. For the last one, we obtain a stronger form of interpolation called Lyndon interpolation.

Created from the Publication Database of the Vienna University of Technology.