Coherentisation of Accessibility Conditions in Labelled Sequent Calculi

ABSTRACT. One methodology for going beyond1 the expressive power of traditional Gentzen systems for non-classical (e.g. intermediate and modal) logics is (instead of hypersequents or nested sequents) the use of labelled sequent calculi, with rules for analysing implications or modal formulae and a representation of conditions on the accessibility relation(s); this allows a wide range of such logics to be represented. Two ways have been studied of representing the accessibility conditions as inference rules: (1) converts the conditions into CNF, using Skolemisation to reduce quantifier alternation, then generating rules that act on both sides of the sequent (papers by Castellini & Smaill, and by Ciabattoni et al), and (2) is, where the accessibility conditions are coherent (aka geometric) implications, to represent them directly as inference rules (acting only on the antecedent) (as in papers by the authors). These latter rules are natural and transparent, whereas clausification tends to render the conditions rather opaquely.

It has been suggested that the second approach is limited to just those accessibility conditions representable as coherent implications. We show this suggestion to be false, by proving that every first-order theory has a coherent conservative extension, i.e. one in which all the necessary reasoning can be carried out using the (coherent) rule-based approach of the authors. This widens the range of logics that approach (2) can handle to all those based on a first-order Hintikka-Kripke semantics.

Such an extension is easily constructed by adding new predicate symbols (and no Skolemisation). Several approaches can be adopted: we consider them in turn, both from a historical and from a practical perspective.