On semantically labelled syntax trees and the non-existence of certain Sahlqvist formulae

We elaborate on semantically labelled syntax trees that provide a method of proving the non-existence of modal formulae satisfying certain syntactic properties and defining a given class of frames and use them to show that there are classes of Kripke frames that are definable by both non-Sahlqvist and Sahlqvist formulae, but the latter requires more propositional variables.

Automated summary

We discuss semantically labelled syntax trees as a means of proving the absence of modal formulas that satisfy specific syntactic properties and define a given class of frames. Using these trees, we demonstrate the existence of classes of Kripke frames that can be defined by both non-Sahlqvist and Sahlqvist formulas, with the latter requiring more propositional variables.