Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere (Q817688)

A hybrid logic is an extension of modal logic obtained by adding both a sort of propositional symbols, called ``nominals'', and by adding so-called ``satisfaction operators''. A nominal is assumed to be true at exactly one world in a model, so that it is a name of that world. Whereas in a propositional logic a nominal is a propositional symbol, in first-order logic it is an argument of a predicate. An expression of the form \(a:\Phi\) means that the formula \(\Phi\) is true at the world named by the nominal \(a\) (where \(a:\) is a satisfaction operator). In this paper, hybridized versions of propositional modal logics are considered, concretely, S5 and the modal logic of inequality. In the former case we have a modal operator, \(\square\), interpreted as ``everywhere''; and in the latter case we have a modal operator, \(\overline{D}\), interpreted as ``elsewhere''. The author develops natural deduction systems for these logics and he proves their functional completeness. The natural deduction systems are sound and complete in the usual model-theoretic sense.