A decidable multi-modal logic of context

We give a logic for formulas φ−ψ, with the informal reading “ψ is true in the context described by φ”. These are interpreted as binary modalities, by quantification over an enumerable set of unary modalities c−ψ, meaning “ψ is true in context c”. The logic allows arbitrary nesting of contexts.A corresponding axiomatic presentation is given, and proven to be decidable, sound, and complete.Previously, quantificational logic of context restricted the nesting of contexts, and was only known to be decidable in very special cases.