Labelled Natural Deduction Systems for Quantified Modal Logics

Abstract

In the previous chapters we have given a framework based on labelled deduction that provides a systematic solution to the problem of finding uniform and modular presentations of propositional non-classical logics. Here we consider quantified modal logics [89, 104, 141] as a significant case study of the additional complexity introduced by quantifiers with respect to the range of possible logics and semantics for them. (Other quantified non-classical logics, e.g. quantified relevance logics, can be presented similarly.) In this case we must choose not only properties of the accessibility relation in the Kripke frame, as in the propositional case, but also how the domains of individuals change between worlds; for example, do the domains vary arbitrarily (varying domains), or do the same objects exist in every world (constant domains), or are objects possibly created (increasing domains) or destroyed (decreasing domains) when moving to accessible worlds?