Unified Correspondence

The present chapter is aimed at giving a conceptual exposition of the mathematical principles underlying Sahlqvist correspondence theory. These principles are argued to be inherently algebraic and order-theoretic. They translate naturally on relational structures thanks to Stone-type duality theory. The availability of this analysis in the setting of the algebras dual to relational models leads naturally to the definition of an expanded (object) language in which the well-known ‘minimal valuation’ meta-arguments can be encoded, and of a calculus for correspondence of a proof-theoretic style in the expanded language, mechanically computing the first-order correspondent of given propositional formulas. The main advantage brought about by this formal machinery is that correspondence theory can be ported in a uniform way to families of nonclassical logics, ranging from substructural logics to mu-calculi, and also to different semantics for the same logic, paving the way to a uniform correspondence theory.