So-called dyadic deontic logic (DDL for short) of the Hansson-Lewis family is one of the most agreed-upon systems of deontic logic. A locus classicus is the book by L. Åqvist [Introduction to deontic logic and the theory of normative systems. Indices. Monographs in Philosophical Logic and Formal Linguistics, IV. Napoli: Bibliopolis (1987; Zbl 0645.03001)]. The language has two dyadic operators: “it ought to be that …given that …” and “it is permitted that …given that …”. These modalities are interpreted using a comparative goodness relation ranking possible worlds in terms of betterness. The usual presentations of DDL are either axiomatic or semantic. Against this background the paper develops the beginnings of a tableau system methodology for this class of logics. The relationship with systems proposed by Åqvist is discussed.
Over the past few years, similar work has been done in the related areas of conditional logic and nonmonotonic reasoning. As far as I know, the paper under review is the first to focus on DDL specifically. In this respect, it can be viewed as an interesting attempt to fill in a gap in the deontic logic literature. The existence of a tableau method for a framework is a first step towards automated theorem proving.
Two quick points.
First, the paper simplifies somewhat the original framework. DDL is re-cast within the framework of multi-modal logic. The conditional obligation operator is treated as a propositionally indexed modality. Correlatively, its evaluation rule is as in a usual modal logic except for the fact that the accessibility relation (in the RHS) has the antecedent of the conditional (appearing in the LHS) as subscript. The tableau rules described in Section 4 are for such a framework. This undoubtedly facilitates the transfer of methods from one area to the other. Still, this leaves unanswered the question of what a tableau construction would be like in the original set-up, where the comparative goodness or betterness relation has first-class citizenship. Results are available in the related area of preference-based conditional logic (see e.g. [L. Giordano, V. Gliozzi, N. Olivetti and C. Schwind, “Tableau calculus for preference-based conditional logics: PCL and its extensions”, ACM Trans. Comput. Log. 10, No. 3, Article No. 21 (2009)]).
Secondly, the paper looks at the relationship between tableaux and models. The main result has the form: any attempt to construct a counterexample to \(A\) using tableaux fails if and only if \(A\) is semantically valid in the class of models considered. The paper does not say much about the relationship between tableaux and proofs in the axiomatic system. In a modal logic setting, the issue is raised in, e.g., Section 4.2 of the paper numbered as [15] in the bibliography. It is the paper by S. A. Kripke [“Semantical analysis of modal logic. I: Normal modal propositional calculi”, Z. Math. Logik Grundlagen Math. 9, 67–96 (1963; Zbl 0118.01305)]. This leaves unanswered the question of whether it can be shown, in a purely syntactical way (without reference to models), that, if \(A\) is a law according to the tableau method, then \(A\) is provable in the corresponding axiomatic system. Kripke’s own answer is based on the notion of characteristic formula of a tableau. It remains to be seen what its counterpart would be within a tableau-based method where the betterness relation has first-class citizenship.