Sahlqvist Correspondence

A syntactic method in modal logic identifying a wide class of modal formulas (Sahlqvist formulas) that enjoy guaranteed first-order frame correspondents and canonical completeness: each Sahlqvist formula corresponds effectively to a first-order condition on frames and generates a canonical axiom whose addition yields completeness for the corresponding frame class.