Non-iterative Modal Resolution Calculi

Abstract

Non-monotonic modal logics are typically interpreted over neighbourhood frames. For unary operators, this is just a set of worlds, together with an endofunction on predicates (subsets of worlds). It is known that all systems of not necessarily monotonic modal logics that are axiomatised by formulae of modal rank at most one (non-iterative modal logics) are Kripke-complete over neighbourhood semantics. In this paper, we give a uniform construction to obtain complete resolution calculi for all non-iterative logics. We show completeness for generative calculi (where new clauses with new literals are added to the clause set) by means of a canonical model construction. We then define absorptive calculi (where new clauses are generated by generalised resolution rules) and establish completeness by translating between generative and absorptive calculi. Instances of our construction re-prove completeness for already known calculi, but also give rise to a number of previously unknown complete calculi.

1 Introduction

There are two standard ways to define modal logics. The syntactic approach specifies a logic by means of its axioms and proof rules. One way of defining the modal logic $\textsf{K}$ is as the least set of formulae that contains all instances of propositional tautologies and the $\textsf{K}$-axioms, and is closed under modus ponens and necessitation. Alternatively, we can take a semantic approach, and define a logic as the set of formulae that is valid over a given class of frames. For the modal logic $\textsf{K}$, this is typically the class of formulae valid over all Kripke frames, but we can alternatively define $\textsf{K}$ as the class of all formulae that are valid in all neighbourhood frames where neighbourhoods are closed under finite intersections. More often than not, the frame class under consideration is also described using logical formulae as axioms.

No matter whether we take a syntactic or semantic approach, the questions remain the same: can we define a proof calculus that allows us to derive all formulae of the logic? Can we decide whether a formula is in the logic?

In this paper, we answer these questions uniformly for the class of all non-iterative modal logics and resolution calculi. Non-iterative logics are defined (either syntactically or semantically) by axioms without nesting of modal operators. While this excludes e.g. logics with (generalised) transitivity axioms, it still covers a large class of specimens. Examples include various classical modal logics of Chellas [8], all standard conditional logics treated in [19], extensions of the modal logic $\textsf{K}$ with reflexivity, seriality and functionality [6], graded and probabilistic modal logic [13, 14], Pauly’s coalition logic [22], a variety of deontic logics [24] and logics of agency [11]. For all these logics, we construct a complete resolution system that can be turned into a decision procedure. From a syntactic viewpoint, we cannot restrict ourselves to normal modal logics. That is, our basic modal systems will only include modal congruence (from $\phi \leftrightarrow \psi$ infer $\Box \phi \leftrightarrow \Box \psi$, or its multi-argument, multi-modal generalisation). Consequently on the semantic side, we adopt neighbourhood semantics as the most general semantic framework. For this semantics, Lewis [16] has already shown that non-iterative logics are complete with respect to the class of neighbourhood frames that are defined by their axioms. Here, completeness is understood with respect to a Hilbert-style system, where deduction is defined as the closure of propositional tautologies and axioms under substitution, modus ponens, and modal congruence. Here, we use the same classes of frames (that are defined by modal axioms), and show that our resolution systems are complete with respect to these frames. Considering the same semantics, this builds a bridge between syntactically defined logics, and the resolution systems that we introduce.

Our technical contribution is the definition, and analysis, of two different types of resolution calculi for each non-iterative logic. The first system that we call generative extends propositional resolution with modal rules that produce new clauses with possibly new modal literals. For example, the modal congruence rule above introduces the clause $\lnot \Box p \vee \Box q$, i.e. $\Box p \rightarrow \Box q$, in contrast to more standard calculi that are based on resolving conflicting literals. In these calculi that we call absorptive, the modal congruence rule would identify $\Box p$ and $\lnot \Box q$ as conflicting, and – assuming that p and q are equivalent – adds the clause $D \vee E$ if $D \vee \lnot \Box p$ and $E \vee \Box q$ are already derived. The reason for introducing both calculi is technical: generative calculi are much more suited to a canonical model construction that we use to prove completeness. In particular, maximally consistent sets behave in the expected way (they contain every literal or its negation). On the other hand, absorptive calculi are the calculi de rigeur, and transforming generative proofs to absorptive proofs, we obtain completeness for absorptive calculi by translation.

Methodologically, we make an interesting, but not entirely unexpected discovery. While in propositional logic, we can derive completeness of resolution directly from completeness of a cut-free sequent calculus (e.g. [10]), this method fails for modal logic: for example, the set $\varPhi = \lbrace p, \lnot p \vee q, \Box p, \lnot \Box q \rbrace$ is evidently satisfiable (at a world, in a neighbourhood or Kripke model), but $\varPhi \vdash _{\!\!} \bot$ in a sequent calculus for classical (or normal) modal logic where $\varDelta \in \varPhi$ are treated as additional axioms or initial sequents. Because the additional initial sequents $\varPhi$ play the role of global assumptions, $\varPhi \vdash _{\!\!} \varGamma$ means that $\varGamma$ is valid in all models where all $\varDelta \in \varPhi$ are true globally (at all worlds). Hence $\varPhi \vdash _{\!\!} \bot$ as there is no model where all $\phi \in \varPhi$ are globally true. Despite the fact that we do not obtain a resolution calculus directly from a sequent calculus (by forgetting the propositional rules), both calculi are still closely related. To ensure completeness of the resolution systems, we employ the same technical condition that guarantees cut elimination in sequent calculi: in both cases, we require that modal rules are cut-closed, i.e. two applications of modal rules, followed by a resolution step between their conclusions, can be replaced by a single modal rule (whose premisses are derivable from the premisses of the original rule). In cut-elimination proofs, this is what allows us to propagate cut towards the leaves of a proof tree. For resolution calculi, this property ensures that a consistent set remains consistent if we extend the language: an inconsistency in the larger system would involve new variables, and cut-closure allows us to eliminate them. We discuss this phenomenon more in the conclusion.

Related Work. As far as we are aware, our paper is the first to study the construction of resolution calculi from a more general perspective, i.e. focusing on properties such as non-iterative axioms rather than on concretely given logical systems. There is a large body of work on resolution calculi on normal modal logics [1,2,3, 7, 9, 12, 17, 18] but [20] appears to be the only paper on modal resolution for non-normal calculi. All of the above approaches focus on concretely given calculi in contrast to this paper that uniformly applies to all calculi with non-iterative axioms. The notion of cut-closure has been used to construct cut-free sequent calculi in [21]. Indeed, the results of op.cit. will give complete, cut-free sequent calculi that have precisely the same modal rules as our generative systems. Of course, we are not the first to observe this deep relationship between sequent calculi and resolution, although our paper appears to be the first that follows a semantic route to directly express completeness of resolution. Avron [4] has discussed the relationship between resolution and sequent calculi for propositional and first order logic, and Mints [17] has considered modal calculi; both from the perspective of syntactical translation. To our knowledge, there is no work that relates sequent calculi and resolution for non-normal modal logics, or on methods that apply to a range of logics in a uniform way.

2 Preliminaries

Definition 1

Let $\textsf{V}$ be a set of propositional variables that we fix throughout. The language $\mathcal {L}$ of modal logic is given by the grammar

$$ \mathcal {L}\ni \phi :\,\!:= p \mid \lnot \phi \mid \phi \vee \phi \mid \Box \phi $$

where $p \in \textsf{V}$. A substitution is a mapping $\sigma : \textsf{V}\rightarrow \mathcal {L}$, and we denote the result of uniformly substituting each $p \in \textsf{V}$ with $\sigma (p)$ in a formula $\phi$ by $\phi \sigma$. A global formula is of the form $\textsf{G}(\phi )$ where $\phi$ is a formula. Propositional and modal literals are given by $\textsf{PL}(\textsf{V}) = \bigcup \lbrace p, \lnot p \mid p \in \textsf{V}\rbrace$ and $\textsf{ML}(\textsf{V}) = \bigcup \lbrace \Box p, \lnot \Box p \mid p \in \textsf{V}\rbrace$, respectively. We denote the set of literals over $\textsf{V}$ by $\textsf{Lit}(\textsf{V}) = \textsf{PL}(\textsf{V}) \cup \textsf{ML}(\textsf{V})$. Two literals are disparate if the variables that occur in them are different. A clause is a finite disjunction of (propositional or modal) literals. We identify a clause with the set of its literals, and sometimes say that a literal is an element of a clause, or write $D_0 \subseteq D_1$ to indicate that clause $D_0$ is a subclause of $D_1$. In particular, we consider two clauses as equal if they have the same literals. A clause is propositional if all literals are propositional. We distinguish local clauses, written $l_1 \vee \dots \vee l_n$, and global clauses, written $\textsf{G}(l_1 \vee \dots \vee l_n)$. We sometimes refer to formulae and clauses as local formulae or local clauses to emphasise the distinction to their global counterparts. We write $\textsf{Cl}(\textsf{V}) = \lbrace l_1 \vee \dots \vee l_n \mid l_1, \dots , l_n \in \textsf{Lit}(\textsf{V}) \rbrace$ for the set of clauses with literals in $\textsf{Lit}(\textsf{V})$.

The following notion of truth distinguishes local and global clauses.

Definition 2

A neighbourhood frame is a pair (W, N) where W is a set (of worlds) and $N: W \rightarrow \mathcal {P}\mathcal {P}(W)$ is a (neighbourhood) function where $\mathcal {P}(X)$ denotes the powerset of a set X. A neighbourhood model is a triple $(W, N, \theta )$ where (W, N) is a neighbourhood frame, and $\theta : \textsf{V}\rightarrow \mathcal {P}(W)$ is a (valuation) function. We say that the model $(W, N, \theta )$ is based on the frame (W, N). Truth $w \models \phi$ of a formula $\phi$ at a world $w \in W$ is given by

$$\begin{aligned} w \models p & \text{ iff } w \in \theta (p) & w \models \lnot \phi & \text{ iff } w \not \models \phi \\ w \models \phi \vee \psi & \text{ iff } w \models \phi \text{ or } w \models \psi & w \models \Box \phi & \text{ iff } \llbracket \phi \rrbracket \in N(w) \end{aligned}$$

where $\llbracket \phi \rrbracket = \lbrace w \in W \mid w \models \phi \rbrace$ is the truth set of $\phi \in \mathcal {L}$. We occasionally write $M, w \models \phi$ or even $(M, N, \theta ), w \models \phi$ if we want to emphasise the (carrier of) the model. This defines the interpretation of local formulae and clauses. For global formulae and clauses, we have $w \models \textsf{G}(\phi ) \text{ iff } w' \models \phi$ for all $w' \in W$. We use standard terminology, and write $(W, N, \theta ) \models \phi$ if $(W, N, \theta ), w \models \phi$ for all $w \in W$, and $(W, N) \models \phi$ if $(W, N, \theta ) \models \phi$ for all $\theta : \textsf{V}\rightarrow \mathcal {P}(W)$. If $\textsf{F}$ is a class of neighbourhood frames, we write $\textsf{F}\models \phi$ if $F \models \phi$ for all frames $F \in \textsf{F}$. A formula $\phi$ is satisfiable in a class $\textsf{F}$ of neighbourhood frames if there is a neighbourhood model $(W, N, \theta )$ with $(W, N) \in \textsf{F}$, and $w \in W$ such that $(W, N, \theta ), w \models \phi$; otherwise, $\phi$ is unsatisfiable in $\textsf{F}$. The notion of (un)satisfiability is extended as usual to sets of formulae.

It is standard that every formula can be converted to an equi-satisfiable set of global and local clauses in linear time.

Proposition 3

(Normal Form [20]). Every (local or global) formula can be converted to an equisatisfiable set of (global and local) clauses.

Proof

Let $\phi \in \mathcal {L}$ be a formula and $p \in \textsf{V}$ be a fresh propositional variable (that does not occur in $\phi$). We write $R(p \!\equiv \!\phi )$ for $R(p)(\phi )$ where the function $R: \textsf{V}\rightarrow \mathcal {L}\rightarrow \textsf{Cl}(\textsf{V})$ is given by

$$\begin{aligned} R(p \!\equiv \!\phi _1 \wedge \phi _2) & = R(p_1 \!\equiv \!\phi _1) \cup R(p_2 \!\equiv \!\phi _2) \cup \lbrace \lnot p \vee p_1, \lnot p \vee p_2, \lnot p_1 \vee \lnot p_2 \vee p \rbrace \\ R(p \!\equiv \!\phi _1 \vee \phi _2) & = R(p_1 \!\equiv \!\phi _1) \cup R(p_2 \!\equiv \!\phi _2) \cup \lbrace \lnot p \vee p_1 \vee p_2, \lnot p_1 \vee p, \lnot p_2 \vee p \rbrace \\ R(p \!\equiv \!\Box \phi ) & = R(q \!\equiv \!\phi ) \cup \lbrace \lnot p \vee \Box q, \lnot \Box q \vee p \rbrace \\ R(p \!\equiv \!\lnot \phi ) & = R(q \!\equiv \!\phi ) \cup \lbrace \lnot p \vee q, \lnot q \vee p \rbrace \end{aligned}$$

where, in each of the clauses, $p_1, p_2$ and q are fresh. It is a routine induction to show that $\phi$ and $\lbrace p \rbrace \cup \lbrace \textsf{G}(D) \mid D \in R(p \!\equiv \!\phi ) \rbrace$ are equi-satisfiable when p does not occur in $\phi$. The same holds for $\textsf{G}(\phi )$ and $\lbrace \textsf{G}(p) \rbrace \cup \lbrace \textsf{G}(D) \mid D \in R(p \!\equiv \!\phi )\rbrace$.     $\square$

3 Non-iterative Logics and Their Calculi

Definition 4

A formula $\phi \in \mathcal {L}$ is non-iterative if, for every subformula $\Box \psi$ of $\phi$, the formula $\psi$ is purely propositional, i.e. does not contain a modal operator. If $\textsf{Ax}$ is a set of (not necessarily non-iterative) formulae, then $\textsf{Frm}(\textsf{Ax})$ is the class of neighbourhood frames (W, N) so that $(W, N) \models \phi$ for all $\phi \in \textsf{Ax}$.

A rule is an $n+1$-tuple $(\phi _1, \dots , \phi _n, \phi _0)$, written as $\phi _1 \dots \phi _n / \phi _0$ where the $\phi _i$ are formulae, and $\phi _1, \dots , \phi _n$ are the premisses, and $\phi _0$ is the conclusion. It is non-iterative if all the premisses are propositional clauses, and the conclusion is a (not necessarily propositional) clause. If $\textsf{Rl}$ is a set of (not necessarily non-iterative) rules, then the class of $\textsf{Frm}(\textsf{Rl})$ is the class (W, N) of neighbourhood frames such that $(W, N, \theta ) \models \phi _0$ whenever $(W, N, \theta ) \models \phi _i$ (all $i = 1, \dots , n)$, for all $\theta : \textsf{V}\rightarrow \mathcal {P}(W)$.

A set $\textsf{Ax}$ of formulae (thought of as axioms) and a set $\textsf{Rl}$ of rules are equivalent if they define the same frames, i.e. $\textsf{Frm}(\textsf{Ax}) = \textsf{Frm}(\textsf{Rl})$.

It is easy to convert between non-iterative rules and axioms [23].

Definition 5

We write $\textsf{cnf}(\phi )$ for a (chosen) conjunctive normal form of a formula $\phi$. The rules induced by the non-iterative axiom $\phi$ are the rules induced by the (non-iterative) clauses $\gamma _1, \dots , \gamma _n$ that constitute the conjunctive normal form of $\phi$, that is, $\textsf{cnf}(\phi ) = \gamma _1 \wedge \dots \wedge \gamma _n$.

A non-iterative clause $\gamma = l_1 \vee \ldots \vee l_n \vee \heartsuit \phi _1 \vee \dots \vee \heartsuit \phi _n$ induces the rule $\iota (\gamma ) = \delta _1 \dots \delta _k/ l_1 \vee \dots \vee l_n \vee \heartsuit p_1 \vee \dots \vee \heartsuit p_n$ where $p_1, \dots , p_n$ are pairwise distinct, fresh, propositional variables, $\heartsuit \in \lbrace \Box , \lnot \Box \rbrace$ and $\delta _1 \wedge \dots \wedge \delta _k$ is a conjunctive normal form of $(p_1 \leftrightarrow \phi _1) \wedge \dots \wedge (p_n \leftrightarrow \phi _n)$.

If on the contrary, $\rho = \gamma _1 \dots \gamma _n / \gamma _0$ is a non-iterative rule, the axiom induced by $\rho$ is $\iota (\rho ) = \gamma _0 \sigma$ where $\sigma$ is the most general unifier of $\gamma _1 \wedge \dots \wedge \gamma _n$.

The above construction ensures that induced axioms and rules are equivalent in the sense of Definition 4.

Proposition 6

Every set $\textsf{Ax}$ of axioms is equivalent to the set of $\bigcup \lbrace \iota (\alpha ) \mid \alpha \in \textsf{Ax}\rbrace$ of induced rules, and every set $\textsf{Rl}$ of non-iterative rules is equivalent to the set $\lbrace \iota (\rho ) \mid \rho \in \textsf{Rl}\rbrace$ of induced axioms.

In examples, the situation is as follows.

Example 7

The classical modal logic $\textsf{E}$ is defined by the empty set of (extra) axioms that induce an empty set of rules. The $\textsf{K}$-axiom $\Box (p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)$ induces the rule $\lnot r \vee \lnot p \vee q, p \vee r, \lnot q \vee r / \lnot \Box r \vee \lnot \Box p \vee \Box q$. In the presence of the congruence rule, necessitation can be replaced by the axiom $\Box \top$ which gives the rule $p / \Box p$. One can show that the (simplified) set of rules $N = \lbrace \lnot p \vee \lnot q \vee r / \lnot \Box p \vee \lnot \Box q \vee \Box r; p / \Box p\rbrace$, as well as the set $S = \lbrace \lnot p_1 \vee \dots \vee \lnot p_n \vee p_0 / \lnot \Box p_1 \vee \dots \vee \lnot \Box p_n \vee \Box p_0 \mid n \ge 0 \rbrace$ are equivalent to the $\textsf{K}$-axiom and $\Box \top$. We call N and S the non-standard and standard rules for $\textsf{K}$. As we are demonstrating in Example 19 the non-standard rules will not give us completeness as they are not cut-closed (Definition 20).

As our calculi apply to all non-iterative logics, we are parametric in a set of (non-iterative) rules. For a set $\textsf{Rl}$ of rules, we define an generative calculus that adds new clauses with possibly new literals, and an absorptive variant, where clauses are combined and conflicting literals are removed.

Definition 8

Let $\textsf{Rl}$ be a set of non-iterative rules. The rules

$$ \frac{D \vee l \quad D' \vee \lnot l}{D \vee D'} \qquad \frac{\textsf{G}(D)}{D} \qquad \frac{\textsf{G}(D \vee l) \quad \textsf{G}(D' \vee \lnot l)}{\textsf{G}(D \vee D')} \quad \frac{\lnot p \vee q \quad p \vee \lnot q}{\lnot \Box p \vee \Box q} $$

are called local resolution $(\textsf{LR})$, the global-local rule $(\textsf{GL})$, global resolution $(\textsf{GR})$, and the modal congruence rule $(\textsf{MC})$, respectively. We write $\textsf{Rl}^\textsf{C}= \textsf{Rl}\cup \lbrace (\textsf{MC}) \rbrace$ for the extension of $\textsf{Rl}$ with the modal congruence rule.

The generative calculus given by $\textsf{Rl}$ has the rules $(\textsf{GR})$, $(\textsf{GL})$, $(\textsf{LR})$ and all rules

$$\begin{aligned} \frac{\textsf{G}(D_1^s) \quad \dots \quad \textsf{G}(D_n^s)}{\textsf{G}(D_0)} \end{aligned}$$

for which $D_1 \dots D_n / D_0 \in \textsf{Rl}^\textsf{C}$ and $D_1^s, \dots , D_n^s$ are subclauses of $D_1, \dots , D_n$. The absorptive calculus defined by $\textsf{Rl}$ has the rules $(\textsf{GR})$, $(\textsf{GL})$, $(\textsf{LR})$ and the rules

$$\begin{aligned} \frac{\textsf{G}(D_1^s) \quad \dots \quad \textsf{G}(D_n^s) \quad \textsf{G}(E_1 \vee \lnot l_1) \quad \dots \quad \textsf{G}(E_k \vee \lnot l_k)}{\textsf{G}(E_1 \vee \dots \vee E_k)} \\ \frac{\textsf{G}(D_1^s) \quad \dots \quad \textsf{G}(D_n^s) \quad E_1 \vee \lnot l_1 \quad \dots \quad E_k \vee \lnot l_k}{E_1 \vee \dots \vee E_k} \end{aligned}$$

where $D_1 \dots D_n / D_0 \in \textsf{Rl}^\textsf{C}$ and $D_i^s \subseteq D_i$ is a subclause of $D_i$, for all $i = 1, \dots , n$.

If $\varGamma$ is a set of local and global clauses, we write $\varGamma \vdash _{\!\!G}$ (resp. $\varGamma \vdash _{\!\!A}$) for the least set of (local and global) clauses that contains $\varGamma$ and is closed under all instances of the rules of generative (resp. absorptive) rules defined by $\textsf{Rl}$. We write $\varGamma \vdash _{\!\!*}\gamma$ if $\gamma \in \varGamma \vdash _{\!\!*}$ for $* = G, A$.

Generative and absorptive calculi serve a different purpose: we are going to prove semantic completeness for generative calculi, and then show that derivation in absorptive calculi can be translated to generative calculi, thus establishing completeness for absorptive calculi as well. In particular, we only consider notions like maximal consistency for generative calculi.

Example 9

The modal logic $\textsf{E}$ just has the congruence rule. The generative and absorptive local version of the congruence rule are

$$ (\textsf{GC}) \frac{\textsf{G}(D_0) \quad \textsf{G}(D_1)}{\textsf{G}(\lnot \Box p \vee \Box q)} \qquad (\textsf{ACL}) \frac{\textsf{G}(D_0) \quad \textsf{G}(D_1) \quad C_1 \vee \Box p \quad C_2 \vee \lnot \Box q}{C_1 \vee C_2} $$

where $D_0 \subseteq \lnot p \vee q$ and $D_1 \subseteq \lnot q \vee p$ are subclauses. In the global version $(\textsf{ACG})$ of the absorptive rule, all clauses of the rightmost rule are under a global modality. For the standard rule set of modal $\textsf{K}$, the generative version looks like the sequent rule on the left

$$ \frac{\textsf{G}(D)}{\textsf{G}(\lnot \Box p_1 \vee \dots \vee \lnot \Box p_n \vee \Box p_0)} \quad \frac{\textsf{G}(D) \quad D_1 \vee \Box p_1 \quad \!\dots \! \quad D_n \vee \Box p_n \quad D_0 \vee \lnot \Box p_0}{D_1 \vee \dots \vee D_n \vee D_0} $$

with the local absorptive rule on the right. Again $D \subseteq \lnot p_1 \vee \dots \vee p_n \vee p_0$ is a subclause, and all clauses are under a global modality in the global absorptive variant of the rule.

It is easy to see that both the generative and the absorptive calculus are sound.

Proposition 10

(Soundness). Let $\textsf{Rl}$ be a set of non-iterative rules. Then $\varGamma \vdash _{\!\!*}\epsilon$ for both $* = G, A$ only if $\varGamma$ is unsatisfiable in the class $\textsf{Frm}(\textsf{Rl})$ of $\textsf{Rl}$-frames.

Proof

We show that $\gamma$ is satisfiable whenever $\varGamma$ is by induction on $\varGamma \vdash _{\!\!*}\gamma$.   $\square$

In particular, if $\textsf{Rl}$ is equivalent to a set $\textsf{Ax}$ of non-iterative axioms, the calculus $\vdash _{\!\!\textsf{Rl}}$ is sound with respect to $\textsf{Frm}(\textsf{Ax})$. We collect some elementary results on the calculi just introduced. The most important one is the trichotomy theorem for generative calculi:

Theorem 11

(Trichotomy). Let l be a modal or propositional literal, and let $\varPhi$ be a set of local and global clauses, and D a local clause with $\varPhi \cup \lbrace l \rbrace \vdash _{\!\!G} D$. Then (1) $D = l$ or (2) $\varPhi \vdash _{\!\!G} D$ or (3) $\varPhi \cup \lbrace \lnot l \rbrace \vdash _{\!\!G} D$.

Proof

By induction on the proof of $\varPhi \cup \lbrace l \rbrace \vdash _{\!\!G} D$. Note that the format of the rules guarantees us that $\varPhi \vdash _{\!\!G}\textsf{G}(D)$ whenever $\varPhi \cup \lbrace l \rbrace \vdash _{\!\!G} \textsf{G}(D)$, as rules with global conclusions only have global premisses.   $\square$

Remark 12

The trichotomy fails for absorptive calculi. Over the empty set of rules $\textsf{Rl}= \emptyset$, i.e. for the modal logic $\textsf{E}$, consider $\varPhi = \lbrace \textsf{G}(\lnot p \vee q), \textsf{G}(\lnot q \vee p), \lnot \Box q \rbrace$. Then $\varPhi \cup \lbrace \Box p \rbrace \vdash _{\!\!A} \epsilon$ but neither $\epsilon = \Box p$ nor $\varPhi \vdash _{\!\!A} \epsilon$ or $\varPhi \vdash _{\!\!A} \lnot \Box p$ hold.

The trichotomy property is a stepping stone to prove negation completeness for maximally consistent sets. As trichotomy fails for absorptive calculi, negation completeness only holds for generative calculi, too.

Definition 13

Let $\textsf{G}$ be a set of global clauses over a (finite or infinite) set $\textsf{V}$ of variables, and let $\varPhi$ be a set of local clauses over the same set of variables. Then $\varPhi$ is $\textsf{G}$-inconsistent if $\textsf{G}\cup \varPhi \vdash _{\!\!G} \epsilon$, and $\textsf{G}$-consistent, otherwise. The set $\varPhi$ is $\textsf{G}$-maximally consistent if $\varPhi$ is $\textsf{G}$-consistent, and for every clause $D \in \textsf{Cl}(\textsf{V})$ with $D \notin \varPhi$, we have that $\varPhi \cup \{D\}$ is $\textsf{G}$-inconsistent.

Technically speaking, it would be more appropriate to speak of generatively (maximally) consistent sets, but we elide the qualifier ‘generative’ as we never consider these notions for absorptive calculi.

Lemma 14

Let M be $\textsf{G}$-maximally consistent and l be a (propositional or modal) literal. Then $l \in M$ or $\lnot l \in M$.

Proof

If neither $l \in M$ nor $\lnot l \in M$, then $M \cup \lbrace l \rbrace \vdash _{\!\!G} \epsilon$ and $M \cup \lbrace \lnot l \rbrace \vdash _{\!\!G} \epsilon$. Using the trichotomy lemma, this entails that $M \vdash _{\!\!G} \epsilon$, contradiction to M being consistent.   $\square$

Moreover, this gives a characterisation of maximally consistent sets as given by a set of singleton clauses.

Lemma 15

Let $\textsf{G}$ be a set of global clauses over a set $\textsf{V}_0$ of propositional variables. Let $L \subset \textsf{V}_0 \cup \lbrace \Box p \mid p \in \textsf{V}\rbrace$ be a set of positive literals, and $L^\lnot = L \cup \{ \lnot l \mid l \in \textsf{Lit}(V_0) \setminus {} L \}$. Then there is a 1-1 correspondence

$$ \lbrace M \mid M\,\,\textsf{G}\text {-maximally consistent} \rbrace {\mathop {\longrightarrow }\limits ^{f}} \lbrace L \subseteq \textsf{V}_0 \mid L^\lnot \,\,\textsf{G}\text {-consistent} \rbrace $$

given by $f(M) = M \cap \textsf{Lit}(\textsf{V}_0)$ from left to right, and $f^{-1}(L) = \lbrace D \vee l \mid D \in \textsf{Cl}(\textsf{V}_0), l \in L^\lnot \rbrace$. Moreover, $\bigwedge M$ and $\bigwedge (f(M))$ are logically equivalent.

The trichotomy law also allows us to show a limited form of deductive completeness for propositional resolution which is known in the literature, consequence completeness [15], although our proof appears to be new. We state the theorem for the generative calculi of Definition 8. It evidently remains true for propositional resolution.

Lemma 16

Let $\varPhi$ be a set of local clauses, and let D be a local clause with pairwise disparate literals such that $\bigwedge \varPhi \rightarrow D$ is a propositional tautology. Then there is a subclause $D_0 \subseteq D$ of D such that $\varPhi \vdash _{\!\!G} D_0$.

Proof

We use completeness of propositional resolution (which is the only rule applicable) and assume that $D = l_1 \vee \dots \vee l_n$ with the $l_i$ pairwise disparate. If $\bigwedge \varPhi \rightarrow D$ is a tautology, then $\varPhi \cup \lbrace \lnot l_1, \dots , \lnot l_n \rbrace$ is unsatisfiable. By completeness of propositional resolution, $\varPhi \cup \lbrace \lnot l_1, \dots , \lnot l_n \rbrace \vdash _{\!\!G} \epsilon$. Repeated application of the trichotomy lemma yields a subclause $D_0 \subseteq D$ such that $\varPhi \vdash _{\!\!G} D_0$.   $\square$

Remark 17

The above theorem fails without the assumption that the literals that occur in D are pairwise disparate. Take for example $\varPhi = \emptyset$ and $D = q \vee \lnot q$. Then clearly $\bigwedge \varPhi \rightarrow q \vee \lnot q$ is a tautology, but $\varPhi \vdash _{\!\!G} q \vee \lnot q$ is false. The reason is that repeated application of the trichotomy lemma fails: we have $\varPhi \cup \lbrace q \rbrace \cup \lbrace \lnot q \rbrace \vdash _{\!\!G} \bot$. Hence by trichotomy, either $\varPhi \cup \lbrace q \rbrace \vdash _{\!\!G} \bot$, or $\varPhi \cup \lbrace q \rbrace \vdash _{\!\!G} q$ as $\lnot q = \epsilon$ is impossible. In the first case, we can apply trichotomy again. In the second, another application leaves the evident possibility that $q = q$.

4 Completeness

Throughout the section, we fix a set $\textsf{Rl}$ of non-iterative rules. Our first goal is to show completeness for the generative calculus. That is, if $\varPhi$ is a finite and consistent set of local and global clauses, then $\varPhi$ is satisfiable in $\textsf{Frm}(\textsf{Rl})$.

As $\varPhi$ is finite, only a finite number of variables will appear in (clauses in) $\varPhi$. Our construction has two stages. We start with a finite set $\textsf{V}_0$ of propositional variables. This allows us to consider maximally consistent sets of clauses over $\textsf{V}_0$. We then extend the language with new variables $\textsf{V}_1$. The purpose of these new variables is to give names to collections of maximally consistent sets. For example, for every maximally consistent set M, we will have a variable $p_M$ such that $p_M = \bigwedge M$, and for a set S of maximally consistent sets, we add a variable with the interpretation $p_S = \bigvee _{M \in S} \bigwedge M$.

Definition 18

Let $\textsf{V}_0$ be a finite set of variables, and $\textsf{G}_0$ be a finite set of global clauses over variables in $\textsf{V}_0$. The extension of $\textsf{V}_0$ and $\textsf{G}_0$ are the sets $\textsf{V}_1$ of variables, and $\textsf{G}_1$ of global clauses where the set $\textsf{V}_1$ extends $V_0$ with

• a variable $p_D$ for every clause D over $\textsf{V}_0$

• a variable $p_M$ for every set M of clauses over $\textsf{V}_0$

• a variable $p_S$ for every set of clause sets over $\textsf{V}_0$.

The set $\textsf{G}_1$ extends $\textsf{G}_0$ with the clauses $\textsf{G}(E)$ where E is in one of the following:

• $\lbrace \lnot p_S \vee \bigvee _{M \in S} p_M \rbrace \cup \lbrace \lnot p_M \vee p_S \mid M \in S \rbrace$, to express that $p_S \leftrightarrow \bigvee _{M \in S} p_M$;

• $\lbrace \bigvee _{D \in M} \lnot p_D \vee p_M \rbrace \cup \lbrace \lnot p_M \vee p_D \mid D \in M\rbrace$, to express $p_M \leftrightarrow \bigwedge _{D \in M} p_D$;

• $\lbrace \lnot p_D \vee p_M \rbrace \cup \lbrace \lnot l \vee p_D \mid l \in D \rbrace$, to express that $p_D \leftrightarrow D$.

We let $W_i = \lbrace M \subseteq \textsf{Cl}(\textsf{V}_i) \mid M\,\,\textsf{G}_0\text {-maximally consistent} \rbrace$, defining two sets of maximally consistent sets of clauses: $W_0$ are clauses over the original variables $\textsf{V}_0$ and $W_1$ are maximally consistent sets over the extended language.

To define the structure of the canonical model, we would like to extend every $\textsf{G}_0$-maximally consistent set M to a $\textsf{G}_1$-maximally consistent set $\hat{M}$, and define $N_0(M) = \lbrace S \subseteq W_0 \mid \Box p_S \in \hat{M} \rbrace$. While this will allow us to establish that the frame conditions (defined by the rules of the calculus) hold, it is not true that every $\textsf{G}_0$-consistent set is $\textsf{G}_1$-consistent.

Example 19

Let $\textsf{V}_0 = \lbrace p, q, r, s \rbrace$ and consider generative rules corresponding to the nonstandard rules for $\textsf{K}$ from Example 7, that is

$$ \frac{\textsf{G}(D)}{\textsf{G}(\lnot \Box p \vee \lnot \Box q \vee \Box r)} (D \subseteq \lnot p \vee \lnot q \vee r) \qquad \frac{\textsf{G}(D)}{\textsf{G}(\Box p)} (D \subseteq p) $$

Consider the set $\textsf{G}_0 = \lbrace \lnot p \vee \lnot q \vee \lnot r \vee s \rbrace$ and let $H = \lbrace \Box p, \Box q, \Box r, \lnot \Box s \rbrace$. Then H is $\textsf{G}_0$-consistent (no resolution rule can be applied), but it is not $\textsf{G}_1$-consistent. If $S = \lbrace M \in W_0 \mid \lbrace p, q \rbrace \subseteq M \rbrace$, then $p_S$ is equivalent to $p \wedge q$ under $\textsf{G}_1$. Hence we have that $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot p \vee \lnot q \vee p_S)$, and also $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot p_S \vee \lnot r \vee \ s)$. Applying the K-rule to both, we obtain $\textsf{G}(\lnot \Box p \vee \lnot \Box q \vee \Box p_S)$ and $\textsf{G}(\lnot \Box p_S \vee \lnot \Box r \vee \Box s)$. Applying resolution, and converting to a local clause, we have that $\textsf{G}_1 \vdash _{\!\!G} \lnot \Box p \vee \lnot \Box q \vee \lnot \Box r \vee \Box s$ so that H is clearly $\textsf{G}_1$-inconsistent.

The key here is that in $\textsf{G}_1$ we have more propositional variables and defining axioms that allow us to make more modal deductions. The crucial point in the above example is that we could apply the modal rule in two different ways, and the apply cut to the rule conclusions. Had we chosen the standard rules for $\textsf{K}$, i.e. $\lnot p_1 \vee \dots \vee \lnot p_n \vee p_0 / \lnot \Box p_1 \vee \dots \vee \lnot \Box p_n \vee \Box p_0$ for all $n \ge 0$, the above set H would not have been $\textsf{G}_0$-consistent. The requirement of cut-closure addresses this problem, and also ensures that $\textsf{G}_0$-consistency implies $\textsf{G}_1$-consistency.

Definition 20

Let $\textsf{Rl}$ be a set of non-iterative rules. Then $\textsf{Rl}$ is cut-closed if, for any two instances on the left

$$ \frac{D_1 \vee \dots \vee D_n}{l \vee D_0} \quad \frac{E_1 \vee \dots \vee E_m}{\lnot l \vee E_0} \qquad \leadsto \qquad \frac{F_1 \vee \dots \vee F_k}{D_0 \vee E_0} $$

there exists a rule instance in $\textsf{Rl}$ (on the right) such that $\lbrace D_1,\! \dots ,\! D_n,\!E_1,\! \dots ,\! E_m\rbrace \! \vdash _{\!\!}\! F_i$ in propositional resolution for all $i = 1, \dots , k$.

Clearly, the paradigmatic example is the rule set of $\textsf{K}$.

Example 21

The nonstandard set of rules for $\textsf{K}$ from Example 7 is not cut-closed: a cut between two instances of the binary K-rule gives a conclusion of the form $\lnot \Box p \vee \lnot \Box q \vee \lnot \Box r \vee \lnot \Box t$ which is clearly not an instance of any of the rules. We therefore need to generalise the rule to $\lnot p_1 \vee \dots \vee \lnot p_n \vee p_0 / \lnot \Box p_1 \vee \dots \vee \lnot \Box p_n \vee \Box p_0$, i.e. the standard set of rules is cut-closed.

Crucially, cut-closed sets guarantee preservation of consistency.

Lemma 22

Let $\textsf{Rl}$ be a cut-closed set of non-iterative rules, and let $\textsf{G}_0$ and $\textsf{G}_1$ be as in Definition 18. Then every $\textsf{G}_0$-consistent set is $\textsf{G}_1$-consistent.

Proof

We use the fact that resolution is confluent, i.e. that we can change the order of resolution steps ad libitum. That is, given clauses $D \vee l_1 \vee l_2$, $\lnot l_1 \vee E_1$ and $\lnot l_2 \vee E_2$, we can resolve with $\lnot l_1 \vee E_1$ first (to obtain $D \vee E_1 \vee l_2$) and then resolve with $\lnot l_2 \vee E_2$ to get $D \vee E_1 \vee E_2$, which we also obtain if we change the order of resolution steps.

Now assume that H is $\textsf{G}_0$-consistent, but $\textsf{G}_1$-inconsistent. Then the derivation of $\epsilon$ from $\textsf{G}_1 \cup H$ needs to contain a modal rule, as the extension $\textsf{G}_1$ of $\textsf{G}_0$ is purely definitional.

Using the confluence property of resolution, we may permute resolution steps so that cuts between conclusions of modal rules are performed first. Using cut-closure, we can replace modal rules, and the cuts between their conclusions, by a single modal rule. We now claim that the ensuing proof is already a proof in $\textsf{G}_0$. This follows, as we can establish by induction that every proof that uses at least one $\textsf{G}_1$-axiom (with variables in $\textsf{V}_1{\setminus }\textsf{V}_0$) has a clause with at least one variable in $\textsf{V}_0{\setminus }\textsf{V}_1$ as a conclusion.   $\square$

Definition 23

(Canonical Model). In the terminology of the previous definition and now assuming that $\textsf{Rl}$ is cut-closed, for $M \in W_0$, let $\hat{M} \in W_1$ be a maximally consistent extension of M, that is, we require that $M \subseteq \hat{M}$.

The canonical model over the set $\textsf{G}_0$ of global clauses and $\textsf{V}_0$ of variables is $\mathbb {M} = (W_0, N_0, \theta _0)$ where $\theta _0(p) = \lbrace M \in W_0 \mid p \in M \rbrace$ and $N_0(M) = \lbrace S \subseteq W_0 \mid \Box p_S \in \hat{M} \rbrace$.

In the sequel, we fix $\textsf{V}_0$ and $\textsf{G}_0$ and speak of the canonical model. Maximally consistent sets are closed under resolution:

Lemma 24

Let $\textsf{G}$ be a set of global clauses, and let M be a $\textsf{G}$-maximally consistent set. Then $D \in M \iff M \vdash _{\!\!G} D$ and $D_1 \vee D_2 \in M$ whenever both $D_1 \vee \lnot l$ and $D_2 \vee l \in M$.

Proof

The second item is immediate from the first. Assume for a contradiction that $M \vdash _{\!\!G} D$ but $D \notin M$. If $D = l_1 \vee \dots \vee l_n$, then $\lnot l_1, \dots , \lnot l_n \in M$. But then $M \vdash _{\!\!G} \epsilon$, contradicting the consistency of M.   $\square$

The truth lemma requires us to establish the premisses of the modal rules. This is split into two lemmas.

Lemma 25

Let $q \in \textsf{V}_0$ and let $S = \llbracket q \rrbracket = \lbrace M \in W_0 \mid q \in M \rbrace$. Then $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot p_S \vee q)$.

Proof

We have that $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot p_M \vee p_q)$ for all $M \in S$ by definition of S. We also have $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot p_S \vee \bigvee _{M \in S} p_M)$. By propositional resolution, we have $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot p_S \vee p_q)$. As we also have $\textsf{G}(\lnot p_q \vee q) \in \textsf{G}_1$ by construction, we apply resolution again to obtain $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot p_S \vee q)$.   $\square$

The reverse implication is more difficult, and we need the following which essentially capitalises on the fact that all our rules with global conclusions have global premisses only.

Lemma and Definition 26

Let $\textsf{G}$ be a set of global clauses. The global closure of $\textsf{G}$ is the set $\textsf{G}^G = \lbrace \textsf{G}(D) \mid \textsf{G}\vdash _{\!\!G} \textsf{G}(D) \rbrace$ of global clauses that are derivable from D. The boundary of $\textsf{G}$ is the set $\textsf{G}^B = \lbrace D \mid \textsf{G}(D) \in \textsf{G}^G \rbrace$ of local clauses that are derived from their global counterpart. With this terminology, $\textsf{G}^B = \lbrace D \mid \textsf{G}\vdash _{\!\!G} D \rbrace$.

Proof

This is immediate from the shape of the rules, as there are no rules with local premisses and global conclusions. It can be proved straightforwardly using induction on the derivation of $\textsf{G}\vdash _{\!\!G} D$.    $\square$

Lemma 27

Let $\textsf{G}$ be a set of global clauses, and suppose that $\textsf{G}\vdash _{\!\!G} D$, for a local clause D. Then also $\textsf{G}\vdash _{\!\!G} \textsf{G}(D)$.

Proof

By induction on the derivation of D. More precisely, we show that if $\textsf{G}\vdash _{\!\!G} C$, for a local or global clause C, then $\textsf{G}\vdash _{\!\!G} C_0$, where $C_0 = C$ if C is global, and $C_0 = \textsf{G}(C)$, if C is local. The key here is that all rules that only deal with local clauses (propositional resolution) have a global counterpart.   $\square$

The following is the companion to Lemma 25.

Lemma 28

Let $q \in \textsf{V}_0$ and let $S = \llbracket q \rrbracket = \lbrace M \in W_0 \mid q \in M \rbrace$. Then $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(D)$, for a subclause $D \subseteq \lnot q \vee p_S$.

Proof

The formula $q \rightarrow \bigvee \lbrace \bigwedge L^\lnot \mid q \in L \subseteq \textsf{V}_0 \rbrace$ is a tautology. As any $\textsf{G}_1$-inconsistent set is inconsistent with $\textsf{G}_1^B$, the same applies to $q \wedge \textsf{G}_1^B \rightarrow \bigvee \lbrace \bigwedge L^\lnot \mid q \in L \subseteq \textsf{V}_0 \textsf{G}_1\text {-consistent} \rbrace$. By Lemma 15 we get that $q \wedge \textsf{G}_1^B \rightarrow \bigvee \lbrace \bigwedge M \mid q \in M \in W_0 \rbrace$. As $p_S$ is equivalent to the last disjunction under $\textsf{G}_1^B$, we finally obtain that $q \wedge \textsf{G}_1^B \rightarrow p_S$ is a tautology. Lemma 26 then yields the claim.   $\square$

This gives us enough ammunition to establish the truth lemma:

Lemma 29

(Truth Lemma). In the canonical model, we have $D \in M \iff M \models D$, for all $M \in W_1$ and all local clauses D over $\textsf{V}_0$.

Proof

By Lemma 14 we just need to show the claim for singleton clauses. For propositional literals, this is immediate from the definition of the valuation $\theta$: we have $M \models p$ iff $M \in \theta (p)$ iff $p \in M$. For the modal case, we have to show that $\Box q \in M$ iff $\Box p_S \in \hat{M}$ where $S = \llbracket q \rrbracket = \lbrace M \in W_0 \mid q \in M \rbrace$.

By Lemma 25 and Lemma 28, we have that $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(D_0)$ and $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(D_1)$, where $D_0$ is a subclause of $\lnot p_S \vee q$ and $D_1$ is a subclause of $\lnot q \vee p_S$. The modal rule allows us to conclude that $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(\lnot \Box p_s \vee \Box q)$ as well as $\textsf{G}(\lnot \Box q \vee \Box p_s)$.

We can now argue that $\Box q \in M$ iff $\Box q \in \hat{M}$ (as M is $\textsf{G}_0$-maximally consistent and $M \subseteq \hat{M}$) iff $\Box p_S \in \hat{M}$ (by resolving with the derivable clauses $\lnot \Box p_s \vee \Box q$ and $\lnot \Box q \vee \Box p_s$).   $\square$

For completeness, we still need to establish that the canonical model satisfies all axioms in A. We use Lemma 15.

Lemma 30

Let $(W_0, N_0)$ be the frame of the canonical modal, and let $\theta : \textsf{V}\rightarrow \mathcal {P}(W_0)$ be any valuation. Moreover, let D be a local propositional clause such that $(W_0, N_0, \theta ) \models D$. Then there is a subclause $D_0 \subseteq D$ of D such that $\textsf{G}_1 \vdash _{\!\!G}\textsf{G}(D_0 \sigma )$ where $\sigma (q) = p_{\theta (q)}$.

Proof

This is similar in spirit to the proof of Lemma 28. We know that $\top \rightarrow \bigvee \lbrace \bigwedge L^\lnot \mid L \subseteq \textsf{V}_0 \rbrace$ is a tautology. As every $\textsf{G}_0$-inconsistent set is inconsistent with the boundary $\textsf{G}_1^B$, we obtain that $\textsf{G}_1^B \rightarrow \lbrace \bigwedge L^\lnot \mid q \in L \subseteq \textsf{V}_0$ $\textsf{G}_0$-inconsistent$\rbrace$. Using Lemma 15, we may replace $L^\lnot$ with maximally consistent sets, i.e. $\textsf{G}_1^B \rightarrow \bigvee \lbrace \bigwedge M \mid M \in W_0 \rbrace$ is a tautology. As $(W_0, N_0, \theta ) \models D$, any maximally consistent $M \in W_0$ is either an element of $\theta (q)$ for $q \in D$, or an element of $W_0 \setminus \theta (q)$, for $\lnot q \in D$. As $p_S$ is equivalent to $\bigvee \lbrace M \mid M \in S \rbrace$ under $\textsf{G}_1^B$, we obtain that $\lbrace \textsf{G}_1^B \rightarrow \bigvee p_{\theta (q)} \mid q \in D \rbrace \vee \bigvee \lbrace \lnot p_{\theta (q)} \mid \lnot q \in D \rbrace$ are tautologies, which entails the claim as in Lemma 28.   $\square$

The previous lemma has shown that we can derive the substituted premiss of a rule in A. The next lemma shows that derivability of the substituted conclusion turns into semantic validity in the canonical model.

Lemma 31

In the canonical model, for $M \in W_0$ and $S \subseteq W_0$, we have that $p_S \in \hat{M} \iff M \in S$ and $\Box p_S \in \hat{M} \iff S \in N_0(M)$.

This allows us to show that the canonical model is in the right frame class.

Lemma 32

Let $\textsf{Ax}$ be a set of non-iterative axioms and $\textsf{Rl}$ an equivalent set of rules. Then $\mathbb {M}\in \textsf{Frm}(A)$ for the canonical model $\mathbb {M}$ given by $\textsf{Rl}$.

Proof

Let $\theta$ be any valuation, and let $\pi / \gamma$ be a rule in $\textsf{Rl}$ such that $(W_0, N_0, \theta ) \models \pi$. We show that $(W_0, N_0, \theta ) \models \gamma$, and the result follows from Lemma 15. Assuming that $\pi = D_1 \dots D_n$, the previous lemma gives us subclauses $D_i^s \subseteq D_i$ such that $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(D_i^s \sigma )$ where $\sigma (q) = p_{\theta (q)}$. Applying the rule $\pi / \gamma \in A$, this gives $\textsf{G}_1 \vdash _{\!\!G} \textsf{G}(D_0 \sigma )$ where $D_0 = \gamma$ is the conclusion of the rule $\pi / \gamma$. Let $M \in W_0$, and showing that $(W_0, N_0, \theta ), M \models D_0$ implies the claim. As $\hat{M}$ is maximally consistent, there is a literal $l \in D_0 \sigma$ with $l \in \hat{M}$. It follows from Lemma 31 that $(W_0, N_0, \theta ) \models l$, hence $(W_0, N_0, \theta ) \models D_0$. As $D_0 = \gamma$ was the conclusion of the rule $\pi / \gamma$, this is all we had to show.   $\square$

Finally:

Theorem 33

(Generative Completeness). Let $\varPhi$ be a set of local and global clauses, and let $\textsf{Rl}$ be a set of non-iterative, cut-closed rules. If $\varPhi$ is unsatisfiable in $\textsf{Frm}(\textsf{Rl})$, then $\varPhi \vdash _{\!\!G} \epsilon$.

Proof

As usual, by contraposition: Let $\textsf{G}_0$ denote the global clauses of $\varPhi$, and let M be a maximally $\textsf{G}$-consistent set that contains all the local clauses of $\varPhi$. In the canonical model, we have that $M \models \phi$ for all $\phi \in \varPhi$, so $\varPhi$ is satisfiable. By the last lemma, we have $\mathbb {M}\in \textsf{Frm}(A)$ so that $\varPhi$ is satisfiable in $\textsf{Frm}(A)$.   $\square$

The criticism of generative calculi is that they are not very “resolution-like”. In particular, the “spirit” of resolution is the removal of conflicting literals, i.e. the absorptive calculi. We now show that both are equivalent.

Lemma 34

Suppose that $\varPhi$ is a set of local or global clauses, and assume that $\varPhi \vdash _{\!\!G} \epsilon$. Then $\varPhi \vdash _{\!\!A} \epsilon$ whenever $\vdash _{\!\!G}$ and $\vdash _{\!\!A}$ are induced by a cut-closed set of rules.

Proof

We demonstrate how to successively replace a generative instance of a rule in $\textsf{Rl}^\textsf{C}$ by an absorptive one. If the derivation $\varPhi \vdash _{\!\!G} \epsilon$ contains an instance of a modal rule (or the congruence rule), assume that there is no other modal rule further below. As the derivation ends in $\epsilon$, every literal must either be resolved against the conclusion of a modal rule (in which case, we can use cut-closure to replace the two rule instances with a new one), or it must be resolved against a clause that is not. Successively applying cut-closure, we are left with just the second case, i.e. with a proof tree of the following form if the last clause is local:

This proof tree can be replaced by its absorptive variant, i.e. the rule instance

$$ \frac{\textsf{G}(D_1^s) \quad \dots \quad \textsf{G}(D_n^s) \quad \lnot l_1 \vee E_1 \quad \dots \quad \lnot l_n \vee E_n}{E_1 \vee \dots \vee E_n} $$

thus reducing the number of applications of generative rules by one. If the conclusion of the cascade of cuts is global, we use the global variant of the absorptive rule instead.   $\square$

This gives us completeness for the absorptive calculus, too.

Theorem 35

(Absorptive Completeness). Let $\varPhi$ be a set of local and global clauses, and let $\textsf{Rl}$ be a set of cut-closed, non-iterative rules. If $\varPhi$ is unsatisfiable in $\textsf{Frm}(A)$, then $\varPhi \vdash _{\!\!A} \epsilon$.

Using Lewis’ theorem, i.e. completeness of a Hilbert system for non-iterative axioms over the class of neighbourhood frames defined by the axioms, we can now also close the loop between syntactically defined logics, and their resolution systems.

Theorem 36

Let $\textsf{Ax}$ be a set of non-iterative axioms, and let $\textsf{Rl}$ be a cut-closed, equivalent set of rules. If $\vdash _{\!\!H} \phi$ is the provability predicate in the Hilbert system given by $\textsf{Ax}$, and $\varPhi$ is the result of translating $\phi$ into an equisatisfiable set of clauses, then $\vdash _{\!\!H} \phi \rightarrow \bot$ iff $\varPhi \vdash _{\!\!A} \epsilon$ iff $\varPhi \vdash _{\!\!G} \epsilon$ iff $\phi$ is unsatisfiable in $\textsf{Frm}(\textsf{Ax})$.

Proof

Lewis [16] shows completeness of $\vdash _{\!\!H}$ with respect to $\textsf{Frm}(\textsf{Ax})$, and we apply Theorem 35 and Theorem 33.   $\square$

The task of finding a complete resolution calculus then boils down to exhibiting a cut-closed set of rules for a given modal logic. We demonstrate this using the example of functional roles in description logic, and role inclusions [5].

Example 37

We consider a modal logic with two normal operators, $\Box$ and $\blacksquare$. In description logic parlance, they correspond to two different roles. We assume that the role corresponding to $\blacksquare$ is functional ($R(i, j) \wedge R(i, k) \rightarrow j = k$). Axiomatically, this means that $\blacksquare$ is a $\textsf{K}$-modality and additionally satisfies $\blacklozenge p \wedge \blacklozenge q \rightarrow \blacklozenge (p \wedge q)$. The second modality, $\Box$, just satisfies the $\textsf{K}$-axioms. A role inclusion is expressed using a transfer axiom $\Box p \rightarrow \blacksquare p$. While the natural semantics here are Kripke frames (with two relations, the first functional, and a subset of the second), the semantics in terms of neighbourhood frames (with two neighbourhood functions) is equivalent (for weak completeness).

• 1. The axiom of functionality is equivalent to the rule

  $$ \frac{\lnot p \vee q \vee r}{\lnot \blacksquare p \vee \blacksquare q \vee \blacksquare r} \qquad \frac{\lnot p_0 \vee p_1 \vee \dots \vee p_n}{\lnot \blacksquare p_0 \vee \blacksquare p_1 \vee \dots \vee \blacksquare p_n} $$

  which readily generalises to the rule scheme (for $n \ge 1$) above. Note that the rule $p / \blacklozenge p$ is not an instance of functionality. Cuts between the conclusion of the K-rule and the above scheme yield the rule

  $$ (\dagger _1) \frac{\lnot a_1 \vee \dots \vee \lnot a_n \vee b_1 \vee \dots \vee b_k}{\lnot \blacksquare a_1 \vee \dots \vee \lnot \blacksquare a_n \vee \blacksquare b_1 \vee \dots \vee \blacksquare b_k} $$

  where $n \ge 0$ and $k \ge 1$. It is easy to see that this set is cut-closed.

• 2. The rule for the K-modality $\Box$ in Example 19, that is

  $$ (\dagger _2) \frac{\lnot a_1 \vee \dots \vee \lnot a_n \vee a_0}{\lnot \Box a_1 \vee \dots \vee \lnot \Box a_n \vee \Box a_0} $$

  is already cut-closed.

• 3. To incorporate the role inclusion axiom $\Box p \rightarrow \blacksquare p$, we need to modify the above rules by resolving their conclusions with the axiom $\lnot \Box p \vee \blacksquare p$. This changes the above rules to

  $$ (\dagger _3) \frac{\lnot a_1 \vee \dots \vee \lnot a_n \vee b_1 \vee \dots \vee b_k}{\lnot \bigcirc a_1 \vee \dots \vee \lnot \bigcirc a_n \vee \blacksquare b_1 \vee \dots \vee \blacksquare b_k} $$

  where n, k are as above and $\bigcirc \in \lbrace \Box , \blacksquare \rbrace$, and

  $$ (\dagger _4) \frac{\lnot a_1 \vee \dots \vee \lnot a_n \vee a_0}{\lnot \Box a_1 \vee \dots \vee \lnot \Box a_n \vee \bigcirc a_0} $$

  where $\bigcirc \in \lbrace \Box , \blacksquare \rbrace$. To this, we add the axiom as a rule without premiss, viz

  $$\begin{aligned} (\dagger _5) \frac{}{\lnot \Box p \vee \blacksquare q} \end{aligned}$$

• 4. One now checks that the rules $(\dagger _3), (\dagger _4)$ and $(\dagger _5)$ together are cut-closed and equivalent to the respective axioms. This means that we can apply Theorem 36 to obtain a complete resolution calculus.

5 Conclusion and Further Work

We have given a general method to construct complete resolution calculi for the class of all non-iterative modal logics. In doing so, we have defined, for each logic, a generative and an absorptive calculus that can be translated into one another. Conceptually, the generative calculus can be seen as a stripped-down sequent calculus that only consists of the modal rule and the cut rules, and we have proved completeness for this calculus, under the same condition, cut-closure, that would also give rise to cut elimination in a sequent calculus. The naive method to convert a sequent calculus to resolution (elide all propositional rules and just keep cut and the modal rules) is bound to fail. For example, consider the clauses (viewed as sequents) $\varPhi = \lbrace p, \Box p, \lnot \Box q, \lnot p \vee q \rbrace$. With sequents in $\varPhi$ as additional axioms in the sequent calculus for the modal logic $\textsf{E}$, we can derive the empty sequent (clause) using just cut, weakening and the congruence rule. However, $\varPhi$ is evidently satisfiable in the class of neighbourhood frames: we need a world that validates both p and q, where p and q have different truth sets in the model, and stipulate the truth set of p to be the only neighbourhood. The reason is that proving $\bot$ in a sequent calculus with additional assumptions $\varPhi$, means that $\bot$ is valid in all models that satisfy $\varPhi$ globally whereas the notion of consistency of interest in modal logic is local. A fortiori, this is the reason why we needed to distinguish between local and global clauses in the calculus we have given. This points to a deeper question on the relationship between sequent calculi and resolution systems. Can we just take any cut-free sequent calculus and turn it into a resolution system (with a suitable notion of global clause)? Can we use more liberal notions of cut-closure? Is there a purely syntactic way to translate between sequent calculi and resolution systems? Can we use this to lift the restriction to non-iterative axioms? Can we employ a more general notion of cut-closure, e.g. as in [21] which would immediately give resolution calculi for several conditional logics? We plan on discussing these questions in further work.