Cathoristic Logic

Abstract

Cathoristic logic is a multi-modal logic where negation is replaced by a novel operator allowing the expression of incompatible sentences. We present the syntax and semantics of the logic including complete proof rules, and establish a number of results such as compactness, a semantic characterisation of elementary equivalence, the existence of a quadratic-time decision procedure, and Brandom’s incompatibility semantics property. We demonstrate the usefulness of the logic as a language for knowledge representation.

Appendices

A Alternative Semantics for Cathoristic Logic

We use state-labelled transition systems as models for cathoristic logic. The purpose of the labels on states is to express constraints, if any, on outgoing actions. This concern is reflected in the semantics of !A.

$$ \begin{array}{lclcl} ((S, \rightarrow , \lambda ), s)\models & {} !A&\quad \text{ iff }\quad&\lambda (s) \subseteq A \end{array} $$

There is an alternative, and in some sense even simpler approach to giving semantics to !A which does not require state-labelling: we simply check if all actions of all outgoing transitions at the current state are in A. As the semantics of other formula requires state-labelling in its satisfaction condition, this means we can use plain labelled transition systems (together with a current state) as models. This gives rise to a subtly different theory that we now explore, albeit not in depth.

1.1 A.1 Pure Cathoristic Models

Definition 32

By a pure cathoristic model, ranged over by $\mathfrak {P}, \mathfrak {P}', ...$, we mean a pair $(\mathcal {L}, s)$ where $\mathcal {L}= (S, \rightarrow )$ is a deterministic labelled transition system and $s \in S$ a state.

Adapting the satisfaction relation to pure cathoristic models is straightforward.

Definition 33

Using pure cathoristic models, the satisfaction relation is defined inductively by the following clauses, where we assume that $\mathfrak {M}= (\mathcal {L}, s)$ and $\mathcal {L}= (S, \rightarrow )$.

$$ \begin{array}{lclcl} \mathfrak {M}&{} \models &{} \top \\ \mathfrak {M}&{} \models &{} \phi \wedge \psi &{}\ \text{ iff } &{} \mathfrak {M}\models \phi \text{ and } \mathfrak {M}\models \psi \\ \mathfrak {M}&{} \models &{} \langle a \rangle \phi &{} \text{ iff } &{} \text {there is a } s \xrightarrow {a} t \text{ such } \text{ that } (\mathcal {L}, t) \models \phi \\ \mathfrak {M}&{} \models &{} A &{} \text{ iff } &{} \{a\ |\ \exists t.s {\mathop {\longrightarrow }\limits ^{a}} t \} \subseteq A \end{array} $$

Note that all but the last clause are unchanged from Definition 4.

In this interpretation, !A restricts the out-degree of the current state s, i.e. it constraints the ‘width’ of the graph. It is easy to see that all rules in Fig. 12 are sound with respect to the new semantics. The key advantage pure cathoristic models have is their simplicity: they are unadorned labelled transition systems, the key model of concurrency theory [26]. The connection with concurrency theory is even stronger than that, because, as we show below (Theorem 11), the elementary equivalence on (finitely branching) pure cathoristic models is bisimilarity, one of the more widely used notions of process equivalence. This characterisation even holds if we remove the determinacy restriction in Definition 32.

1.2 A.2 Relationship Between Pure and Cathoristic Models

The obvious way of converting an cathoristic model into a pure cathoristic model is by forgetting about the state-labelling:

$$ ((S, \rightarrow , \lambda ), s ) \qquad \mapsto \qquad ((S, \rightarrow ), s ) $$

Let this function be $\mathsf {forget}(\cdot )$. For going the other way, we have two obvious choices:

• $((S, \rightarrow ), s ) \mapsto ((S, \rightarrow , \lambda ), s )$ where $\lambda (t) = \varSigma$ for all states t. Call this map $\mathsf {max}(\cdot )$.

• $((S, \rightarrow ), s ) \mapsto ((S, \rightarrow , \lambda ), s )$ where $\lambda (t) = \{a \ |\ \exists t'. t {\mathop {\longrightarrow }\limits ^{a}} t'\}$ for all states t. Call this map $\mathsf {min}(\cdot )$.

Lemma 14

Let $\mathfrak {M}$ be an cathoristic model, and $\mathfrak {P}$ a pure cathoristic model.

• 1. $\mathfrak {M}\models \phi$ implies $\mathsf {forget}(\mathfrak {M}) \models \phi$. The reverse implication does not hold.

• 2. $\mathsf {max}(\mathfrak {P}) \models \phi$ implies $\mathfrak {P}\models \phi$. The reverse implication does not hold.

• 3. $\mathsf {min}(\mathfrak {P}) \models \phi$ if and only if $\mathfrak {P}\models \phi$.

Proof

The implication in (1) is immediate by induction on $\phi$. A counterexample for the reverse implication is given by the formula $\phi = !\{a\}$ and the cathoristic model $\mathfrak {M}= ( \{s, t\}, s {\mathop {\longrightarrow }\limits ^{a}} t, \lambda ), s)$ where $\lambda (s) = \{a, b, c\}$: clearly $\mathsf {forget}(\mathfrak {M}) \models \phi$, but $\mathfrak {M}\not \models \phi$.

The implication in (2) is immediate by induction on $\phi$. To construct a counterexample for the reverse implication, assume that $\varSigma$ is a strict superset of $\{a\}$ a. The formula $\phi = !\{a\}$ and the pure cathoristic model $\mathfrak {P}= ( \{s, t\}, s {\mathop {\longrightarrow }\limits ^{a}} t ), s)$ satisfy $\mathfrak {P}\models \phi$, but clearly $\mathsf {max}(\mathfrak {P}) \not \models \phi$.

Finally, (3) is also straightforward by induction on $\phi$.   $\square$

1.3 A.3 Non-determinism and Cathoristic Models

Both, cathoristic models and pure cathoristic models must be deterministic. That is important for the incompatibility semantics. However, formally, the definition of satisfaction makes sense for non-deterministic models as well, pure or otherwise. Such models are important in the theory of concurrent processes. Many of the theorems of the precious section either hold directly, or with small modifications for non-deterministic models. The rules of inference in Fig. 12 are sound except for [Determinism] which cannot hold in properly non-deterministic models. With this omission, they are also complete. Elementary equivalence on non-deterministic cathoristic models also coincides with mutual simulation, while elementary equivalence on non-deterministic pure cathoristic models is bisimilarity. The proofs of both facts follow those of Theorems 1 and 11, respectively. Compactness by translation can be shown following the proof in Sect. 8, except that the constraint $\phi _{det}$ is unnecessary.

We have experimented with a version of cathoristic logic in which the models are non-deterministic labelled-transition systems. Although non-determinism makes some of the constructions simpler, non-deterministic cathoristic logic is unable to express incompatibility properly. Consider, for example, the claim that Jack is married¹⁸ to Jill In standard deterministic cathoristic logic this would be rendered as:

$$\begin{aligned} \langle jack \rangle \langle married \rangle (\langle jill \rangle \wedge !\{jill\}) \end{aligned}$$

There are three levels at which this claim can be denied. First, we can claim that Jack is married to someone else - Joan, say:

$$\begin{aligned} \langle jack \rangle \langle married \rangle (\langle joan \rangle \wedge !\{joan\}) \end{aligned}$$

Second, we can claim that Jack is unmarried (specifically, that being unmarried is Jack’s only property):

$$\begin{aligned} \langle jack \rangle !\{unmarried\} \end{aligned}$$

Third, we can claim that Jack does not exist at all. Bob and Jill, for example, are the only people in our domain:

$$\begin{aligned} !\{bob, jill\} \end{aligned}$$

Now we can assert the same sentences in non-deterministic cathoristic logic, but they are no longer incompatible with our original sentence. In non-deterministic cathoristic logic, the following sentences are compatible (as long as there are two separate transitions labelled with married, or two separate transitions labelled with jack):

$$\begin{aligned} \langle jack \rangle \langle married \rangle (\langle jill \rangle \wedge !\{jill\}) \qquad \langle jack \rangle \langle married \rangle (\langle joan \rangle \wedge !\{joan\}) \end{aligned}$$

Similarly, the following sentences are fully compatible as long as there are two separate transitions labelled with jack:

$$\begin{aligned} \langle jack \rangle \langle married \rangle \qquad \langle jack \rangle !\{unmarried\} \end{aligned}$$

Relatedly, non-deterministic cathoristic logic does not satisfy Brandom’s incompatibility semantics property:

$$ \phi \models \psi \; \text{ iff } \; \mathcal {I}(\psi ) \subseteq \mathcal {I}(\phi ) $$

To take a simple counter-example, $\langle a \rangle \langle b \rangle$ implies $\langle a \rangle$, but not conversely. But in non-deterministic cathoristic logic, the set of sentences incompatible with $\langle a \rangle \langle b \rangle$ is identical with the set of sentences incompatible with $\langle a \rangle$.

1.4 A.4 Semantic Characterisation of Elementary Equivalence

In Sect. 6.1 we presented a semantic analysis of elementary equivalence, culminating in Theorem 1 which showed that elementary equivalence coincides with $\simeq$, the relation of mutual simulation of models. We shall now carry out a similar analysis for pure cathoristic models, and show that elementary equivalence coincides with bisimilarity, an important concept in process theory and modal logics [25]. Bisimilarity is strictly finer on non-deterministic transition systems than $\simeq$, and more sensitive to branching structure. In the rest of this section, we allow non-deterministic pure models, because the characterisation is more interesting that in the deterministic case.

Definition 34

A pure cathoristic model $(\mathcal {L}, s)$ is finitely branching if its underlying transition system $\mathcal {L}$ is finitely branching.

Definition 35

A binary relation $\mathcal {R}$ is a bisimulation between pure cathoristic models $\mathfrak {P}_i = (\mathcal {L}_i), s_i)$ for $i = 1, 2$ provided (1) $\mathcal {R}$ is a bisimulation between $\mathcal {L}_1$ and $\mathcal {L}_2$, and (2) $(s_1, s_2) \in \mathcal {R}$. We say $\mathfrak {P}_1$ and $\mathfrak {P}_2$ are bisimilar, written $\mathfrak {P}_1 \sim \mathfrak {P}_2$ if there is a bisimulation between $\mathfrak {P}_1$ and $\mathfrak {P}_2$.

Definition 36

The theory of $\mathfrak {P}$, written $\mathsf {Th}(\mathfrak {P})$, is the set $\{\phi \ |\ \mathfrak {P}\models \phi \}$.

Theorem 11

Let $\mathfrak {P}$ and $\mathfrak {P}'$ be two finitely branching pure cathoristic models. Then: $\mathfrak {P}\sim \mathfrak {P}'$ if and only if $\mathsf {Th}(\mathfrak {P}) = \mathsf {Th}(\mathfrak {P}')$.

Proof

Let $\mathfrak {P}= (\mathcal {L}, w)$ and $\mathfrak {P}' = (\mathcal {L}', w')$ be finitely branching, where $\mathcal {L}= (W, \rightarrow )$ and $(W', \rightarrow ')$. We first show the left to right direction, so assume that $\mathfrak {P}\sim \mathfrak {P}'$.

The proof is by induction on formulae. The only case which differs from the standard Hennessy-Milner theorem is the case for !A, so this is the only case we shall consider. Assume $w \sim w'$ and $w \models !A$. We need to show $w' \models !A$. From the semantic clause for !, $w \models !A$ implies $\lambda (w) \subseteq A$. If $w \sim w'$, then $\lambda (w) = \lambda '(w')$. Therefore $\lambda '(w') \subseteq A$, and hence $w' \models !A$.

The proof for the other direction is more involved. For states $x \in W$ and $x' \in W$, we write

$$ x \equiv x' \qquad \text {iff}\qquad \mathsf {Th}((\mathcal {L}, x)) = \mathsf {Th}((\mathcal {L}', x')). $$

We define the bisimilarity relation:

$$ Z = \{(x,x') \in \mathcal {W} \times \mathcal {W}' \ | \ x \equiv x' \} $$

To prove $w \sim w'$, we need to show:

• $(w,w') \in Z$. This is immediate from the definition of Z.

• The relation Z respects the transition-restrictions: if $(x,x') \in Z$ then $\lambda (x) = \lambda '(x')$

• The forth condition: if $(x,x') \in Z$ and $x \xrightarrow {a} y$, then there exists a $y'$ such that $x' \xrightarrow {a} y'$ and $(y, y') \in Z$.

• The back condition: if $(x,x') \in Z$ and $x' \xrightarrow {a} y'$, then there exists a y such that $x \xrightarrow {a} y$ and $(y, y') \in Z$.

To show that $(x,x') \in Z$ implies $\lambda (x) = \lambda '(x')$, we will argue by contraposition. Assume $\lambda (x) \ne \lambda '(x')$. Then either $\lambda '(x') \nsubseteq \lambda (x)$ or $\lambda (x) \nsubseteq \lambda '(x')$. If $\lambda '(x') \nsubseteq \lambda (x)$, then $x' \nvDash !\lambda (x)$. But $x \models !\lambda (x)$, so x and $x'$ satisfy different sets of propositions and are not equivalent. Similarly, if $\lambda (x) \nsubseteq \lambda '(x')$ then $x \nvDash !\lambda '(x')$. But $x' \models !\lambda '(x')$, so again x and $x'$ satisfy different sets of propositions and are not equivalent.

We will show the forth condition in detail. The back condition is similar. To show the forth condition, assume that $x \xrightarrow {a} y$ and that $(x,x') \in Z$ (i.e. $x \equiv x'$). We need to show that $\exists y'$ such that $x' \xrightarrow {a} y'$ and $(y,y') \in Z$ (i.e. $y \equiv y'$).

Consider the set of $y'_i$ such that $x' \xrightarrow {a} y'_i$. Since $x \xrightarrow {a} y$, $x \models \langle a \rangle \top$, and as $x \equiv x'$, $x' \models \langle a \rangle \top$, so we know this set is non-empty. Further, since $(\mathcal {W}', \rightarrow ')$ is finitely-branching, there is only a finite set of such $y'_i$, so we can list them $y'_1, ..., y'_n$, where $n >= 1$.

Now, in the Hennessy-Milner theorem for Hennessy-Milner logic, the proof proceeds as follows: assume, for reductio, that of the $y'_1, ..., y'_n$, there is no $y'_i$ such that $y \equiv y'_i$. Then, by the definition of $\equiv$, there must be formulae $\phi _1, ..., \phi _n$ such that for all i in 1 to n:

$$ y'_i \models \phi _i \text{ and } y \nvDash \phi _i $$

Now consider the formula:

$$ [a] (\phi _1 \vee ... \vee \phi _n) $$

As each $y'_i \models \phi _i$, $x' \models [a] (\phi _1 \vee ... \vee \phi _n)$, but x does not satisfy this formula, as each $\phi _i$ is not satisfied at y. Since there is a formula which x and $x'$ do not agree on, x and $x'$ are not equivalent, contradicting our initial assumption.

But this proof cannot be used in cathoristic logic because it relies on a formula $[a] (\phi _1 \vee ... \vee \phi _n)$ which cannot be expressed in cathoristic logic: Cathoristic logic does not include the box operator or disjunction, so this formula is ruled out on two accounts. But we can massage it into a form which is more amenable to cathoristic logic’s expressive resources:

$$\begin{aligned}{}[a] (\phi _1 \vee ... \vee \phi _n)= & {} \lnot \langle a \rangle \lnot (\phi _1 \vee ... \vee \phi _n) \\= & {} \lnot \langle a \rangle (\lnot \phi _1\wedge ... \wedge \lnot \phi _n) \end{aligned}$$

Further, if the original formula $[a] (\phi _1 \vee ... \vee \phi _n)$ is true in $x'$ but not in x, then its negation will be true in x but not in $x'$. So we have the following formula, true in x but not in $x'$:

$$ \langle a \rangle (\lnot \phi _1\wedge ... \wedge \lnot \phi _n) $$

The reason for massaging the formula in this way is so we can express it in cathoristic logic (which does not have the box operator or disjunction). At this moment, the revised formula is still outside cathoristic logic because it uses negation. But we are almost there: the remaining negation is in innermost scope, and innermost scope negation can be simulated in cathoristic logic by the ! operator.

We are assuming, for reductio, that of the $y'_1, ..., y'_n$, there is no $y'_i$ such that $y \equiv y'_i$. But in cathoristic logic without negation, we cannot assume that each $y'_i$ has a formula $\phi _i$ which is satisfied by $y'_i$ but not by y - it might instead be the other way round: $\phi _i$ may be satisfied by y but not by $y'_i$. So, without loss of generality, assume that $y'_1, ..., y'_m$ fail to satisfy formulae $\phi _1, ..., \phi _m$ which y does satisfy, and that $y'_{m+1}, ..., y'_n$ satisfy formulae $\phi _{m+1}, ..., \phi _n$ which y does not:

$$\begin{aligned} y \models \phi _i \text{ and } y'_i \nvDash \phi _i&i = 1 \text{ to } m \\ y \nvDash \phi _j \text{ and } y'_j \models \phi _j&j = m+1 \text{ to } n \end{aligned}$$

The formula we will use to distinguish between x and $x'$ is:

$$ \langle a \rangle ( \bigwedge _{i=1}^m \phi _i \; \wedge \; \bigwedge _{j=m+1}^n \mathsf {neg}(y, \phi _j)) $$

Here, $\mathsf {neg}$ is a meta-language function that, given a state y and a formula $\phi _j$, returns a formula that is true in y but incompatible with $\phi _j$. We will show that, since $y \nvDash \phi _j$, it is always possible to construct $\mathsf {neg}(y, \phi _j)$ using the ! operator.

Consider the possible forms of $\phi _j$:

• $\top$: this case cannot occur since all models satisfy $\top$.

• $\phi _1 \wedge \phi _2$: we know $y'_j \models \phi _1 \wedge \phi _2$ and $y \nvDash \phi _1 \wedge \phi _2$. There are three possibilities:

  • 1. $y \nvDash \phi _1$ and $y \models \phi _2$. In this case, $\mathsf {neg}(y, \phi _1 \wedge \phi _2) = \mathsf {neg}(y, \phi _1) \wedge \phi _2$.

  • 2. $y \models \phi _1$ and $y \nvDash \phi _2$. In this case, $\mathsf {neg}(y, \phi _1 \wedge \phi _2) = \phi _1 \wedge \mathsf {neg}(y, \phi _2)$.

  • 3. $y \nvDash \phi _1$ and $y \nvDash \phi _2$. In this case, $\mathsf {neg}(y, \phi _1 \wedge \phi _2) = \mathsf {neg}(y, \phi _1) \wedge \mathsf {neg}(y, \phi _2)$.

• !A: if $y \nvDash !A \text{ and } y'_j \models !A$, then there is an action $a \in \varSigma -A$ such that $y \xrightarrow {a} z$ for some z but there is no such z such that $y'_j \xrightarrow {a} z$. In this case, let $\mathsf {neg}(y, \phi _j) = \langle a \rangle \top$.

• $\langle a \rangle \phi$. There are two possibilities:

  • 1. $y \models \langle a \rangle \top$. In this case, $\mathsf {neg}(y, \langle a \rangle \phi ) = \bigwedge \limits _{y \xrightarrow {a} z} \langle a \rangle \mathsf {neg}(z, \phi )$.

  • 2. $y \nvDash \langle a \rangle \top$. In this case, $\mathsf {neg}(y, \langle a \rangle \phi ) = !\{ b \ | \ \exists z. y \xrightarrow {b} z\}$. This set of bs is finite since we are assuming the transition system is finitely-branching.

   $\square$

We continue with a worked example of $\mathsf {neg}$. Consider y and $y'_j$ as in Fig. 16. One formula that is true in $y'_j$ but not in y is

$$ \langle a \rangle (\langle b \rangle \top \wedge \langle c \rangle \top ) $$

Fig. 16.

Worked example of $\mathsf {neg}$. Note that the transition system on the left is non-deterministic.

Now:

$$\begin{aligned}&\mathsf {neg}(y, \langle a \rangle (\langle b \rangle \top \wedge \langle c \rangle \top )) \\&\qquad \qquad \qquad \; = \bigwedge \limits _{y \xrightarrow {a} z} \langle a \rangle \mathsf {neg}(z, \langle b \rangle \top \wedge \langle c \rangle \top ) \\&\qquad \qquad \qquad \; = \langle a \rangle \mathsf {neg}(z_1, \langle b \rangle \top \wedge \langle c \rangle \top ) \wedge \langle a \rangle \mathsf {neg}(z_2, \langle b \rangle \top \wedge \langle c \rangle \top ) \\&\qquad \qquad \qquad \; = \langle a \rangle (\langle b \rangle \top \wedge \mathsf {neg}(z_1, \langle c \rangle \top )) \wedge \langle a \rangle \mathsf {neg}(z_2, \langle b \rangle \top \wedge \langle c \rangle \top ) \\&\qquad \qquad \qquad \; = \langle a \rangle (\langle b \rangle \top \wedge \mathsf {neg}(z_1, \langle c \rangle \top )) \wedge \langle a \rangle (\mathsf {neg}(z_2, \langle b \rangle \top ) \wedge \langle c \rangle \top ) \\&\qquad \qquad \qquad \; = \langle a \rangle (\langle b \rangle \top \wedge !\{b\}) \wedge \langle a \rangle (\mathsf {neg}(z_2, \langle b \rangle \top ) \wedge \langle c \rangle \top ) \\&\qquad \qquad \qquad \; = \langle a \rangle (\langle b \rangle \top \wedge !\{b\}) \wedge \langle a \rangle (!\{c\} \wedge \langle c \rangle \top ) \end{aligned}$$

The resulting formula is true in y but not in $y'_j$.

B Omitted Proofs

1.1 B.1 Proof of Lemma 5

If $\mathfrak {M}\models \phi$ then $\mathfrak {M}\preceq \mathsf {simpl}(\phi )$.

Proof

We shall show $\mathsf {Th}(\mathsf {simpl}(\phi )) \subseteq \mathsf {Th}(\mathfrak {M})$. The desired result will then follow by applying Theorem 1. We shall show that

$$ \text {If } \mathfrak {M}\models \phi \text { then } \mathsf {Th}(\mathsf {simpl}(\phi )) \subseteq \mathsf {Th}(\mathfrak {M}) $$

by induction on $\phi$. In all the cases below, let $\mathsf {simpl}(\phi ) = (\mathcal {L}, w)$ and let $\mathfrak {M}= (\mathcal {L}', w')$. The case where $\phi = \top$ is trivial. Next, assume $\phi = \langle a \rangle \psi$. We know $\mathfrak {M}\models \langle a \rangle \psi$ and need to show that $\mathsf {Th}(\mathsf {simpl}(\langle a \rangle \psi )) \subseteq \mathsf {Th}(\mathfrak {M})$. Since $(\mathcal {L}', w') \models \langle a \rangle \psi$, there is an $x'$ such that $w' \xrightarrow {a} x'$ and $(\mathcal {L}', x') \models \psi$. Now from the definition of $\mathsf {simpl}()$, $\mathsf {simpl}(\langle a \rangle \psi )$ is a model combining $\mathsf {simpl}(\psi )$ with a new state w not appearing in $\mathsf {simpl}(\psi )$ with an arrow $w \xrightarrow {a} x$ (where x is the start state in $\mathsf {simpl}(\psi )$), and $\lambda (w) = \varSigma$. Consider any sentence $\xi$ such that $\mathsf {simpl}(\langle a \rangle \psi ) \models \xi$. Given the construction of $\mathsf {simpl}(\langle a \rangle \psi )$, $\xi$ must be a conjunction of $\top$ and formulae of the form $\langle a \rangle \tau$. In the first case, $(\mathcal {L}', x')$ satisfies $\top$; in the second case, $(\mathcal {L}', x') \models \tau$ by the induction hypothesis and hence $(\mathcal {L}', w') \models \langle a \rangle \tau$.

Next, consider the case where $\phi = !A$, for some finite set $A \subset \varSigma$. From the definition of $\mathsf {simpl}()$, $\mathsf {simpl}(!A)$ is a model with one state s, no transitions, with $\lambda (s) = A$. Now the only formulae that are true in $\mathsf {simpl}(!A)$ are conjunctions of $\top$ and !B, for supersets $B \supseteq A$. If $\mathfrak {M}\models !A$ then by the semantic clause for !, $\lambda '(w') \subseteq A$, hence $\mathfrak {M}$ models all the formulae that are true in $\mathsf {simpl}(!A)$.

Finally, consider the case where $\phi = \psi _1 \wedge \psi _2$. Assume $\mathfrak {M}\models \psi _1$ and $\mathfrak {M}\models \psi _2$. We assume, by the induction hypothesis that $\mathsf {Th}(\mathsf {simpl}(\psi _1)) \subseteq \mathsf {Th}(\mathfrak {M})$ and $\mathsf {Th}(\mathsf {simpl}(\psi _2)) \subseteq \mathsf {Th}(\mathfrak {M})$. We need to show that $\mathsf {Th}(\mathsf {simpl}(\psi _1\wedge \psi _2)) \subseteq \mathsf {Th}(\mathfrak {M})$. By the definition of $\mathsf {simpl}()$, $\mathsf {simpl}(\psi _1 \wedge \psi _2) = \mathsf {simpl}(\psi _1) \sqcap \mathsf {simpl}(\psi _2)$. If $\mathsf {simpl}(\psi _1)$ and $\mathsf {simpl}(\psi _2)$ are $\mathsf {inconsistent}$ (see the definition of $\mathsf {inconsistent}$ in Sect. 6.4) then $\mathfrak {M}= \bot$. In this case, $\mathsf {Th}(\mathsf {simpl}(\psi _1) \wedge \mathsf {simpl}(\psi _2)) \subseteq \mathsf {Th}(\bot )$. If, on the other hand, $\mathsf {simpl}(\psi _1)$ and $\mathsf {simpl}(\psi _2)$ are not $\mathsf {inconsistent}$, we shall show that $\mathsf {Th}(\mathsf {simpl}(\psi _1 \wedge \psi _2)) \subseteq \mathsf {Th}(\mathfrak {M})$ by reductio. Assume a formula $\xi$ such that $\mathsf {simpl}(\psi _1 \wedge \psi _2) \models \xi$ but $\mathfrak {M}\nvDash \xi$. Now $\xi \ne \top$ because all models satisfy $\top$. $\xi$ cannot be of the form $\langle a \rangle \tau$ because, by the construction of $\mathsf {merge}$ (see Sect. 6.4), all transitions in $\mathsf {simpl}(\psi _1 \wedge \psi _2)$ are transitions from $\mathsf {simpl}(\psi _1)$ or $\mathsf {simpl}(\psi _2)$ and we know from the inductive hypothesis that $\mathsf {Th}(\mathsf {simpl}(\psi _1)) \subseteq \mathsf {Th}(\mathfrak {M})$ and $\mathsf {Th}(\mathsf {simpl}(\psi _2)) \subseteq \mathsf {Th}(\mathfrak {M})$. $\xi$ cannot be !A for some $A \subset \varSigma$, because, from the construction of $\mathsf {merge}$, all state-labellings in $\mathsf {simpl}(\psi _1 \wedge \psi _2)$ are no more specific than the corresponding state-labellings in $\mathsf {simpl}(\psi _1)$ and $\mathsf {simpl}(\psi _2)$, and we know from the inductive hypothesis that $\mathsf {Th}(\mathsf {simpl}(\psi _1)) \subseteq \mathsf {Th}(\mathfrak {M})$ and $\mathsf {Th}(\mathsf {simpl}(\psi _2)) \subseteq \mathsf {Th}(\mathfrak {M})$. Finally, $\xi$ cannot be $\xi _1 \wedge xi_2$ because the same argument applies to $xi_1$ and $xi_2$ individually. We have exhausted the possible forms of $\xi$, so conclude that there is no formula $\xi$ such that $\mathsf {simpl}(\psi _1 \wedge \psi _2) \models \xi$ but $\mathfrak {M}\nvDash \xi$. Hence $\mathsf {Th}(\mathsf {simpl}(\psi _1\wedge \psi _2)) \subseteq \mathsf {Th}(\mathfrak {M})$.   $\square$

1.2 B.2 Proof of Lemma 6

If $\phi \models \psi \text{ then } \mathsf {simpl}(\phi ) \preceq \mathsf {simpl}(\psi )$

Proof

By Theorem 1, $\mathsf {simpl}(\phi ) \preceq \mathsf {simpl}(\psi )$ iff $\mathsf {Th}(\mathsf {simpl}(\psi )) \subseteq \mathsf {Th}(\mathsf {simpl}(\phi ))$. Assume $\phi \models \psi$, and assume $\xi \in \mathsf {Th}(\mathsf {simpl}(\psi ))$. We must show $\xi \in \mathsf {Th}(\mathsf {simpl}(\phi ))$. Now $\mathsf {simpl}($) is constructed so that:

$$ \mathsf {simpl}(\psi ) = \bigsqcup \{ \mathfrak {M}\; | \; \mathfrak {M}\models \psi \} $$

So $\xi \in \mathsf {Th}(\mathsf {simpl}(\psi ))$ iff for all models $\mathfrak {M}$, $\mathfrak {M}\models \psi$ implies $\mathfrak {M}\models \xi$. We must show that $\mathfrak {M}\models \phi$ implies $\mathfrak {M}\models \xi$ for all models $\mathfrak {M}$. Assume $\mathfrak {M}\models \phi$. Then since $\phi \models \psi$, $\mathfrak {M}\models \psi$. But since $\xi \in \mathsf {Th}(\mathsf {simpl}(\psi ))$, $\mathfrak {M}\models \xi$ also.   $\square$

1.3 B.3 Proof of Lemma 7

If $\mathcal {I}(\psi ) \subseteq \mathcal {I}(\phi ) \text{ then } \mathcal {J}(\mathsf {simpl}(\psi )) \subseteq \mathcal {J}(\mathsf {simpl}(\phi ))$

Proof

Assume $\mathcal {I}(\psi ) \subseteq \mathcal {I}(\phi )$ and $\mathfrak {M}\sqcap \mathsf {simpl}(\psi ) = \bot$. We need to show $\mathfrak {M}\sqcap \mathsf {simpl}(\phi ) = \bot$. If $\mathcal {I}(\psi ) \subseteq \mathcal {I}(\phi )$ then for all formulae $\xi$, if $\mathsf {simpl}(\xi ) \sqcap \mathsf {simpl}(\psi ) = \bot$ then $\mathsf {simpl}(\xi ) \sqcap \mathsf {simpl}(\phi ) = \bot$. Let $\xi$ be $\mathsf {char}(\mathfrak {M})$. Given that $\mathfrak {M}\sqcap \mathsf {simpl}(\psi ) = \bot$ and $\mathsf {simpl}(\mathsf {char}(\mathfrak {M})) \preceq \mathfrak {M}$, $\mathsf {simpl}(\mathsf {char}(\mathfrak {M})) \sqcap \mathsf {simpl}(\psi ) = \bot$. Then as $\mathcal {I}(\psi ) \subseteq \mathcal {I}(\phi )$, $\mathsf {simpl}(\mathsf {char}(\mathfrak {M})) \sqcap \mathsf {simpl}(\phi ) = \bot$. Now as $\mathfrak {M}\preceq \mathsf {simpl}(\mathsf {char}(\mathfrak {M}))$, $\mathfrak {M}\sqcap \mathsf {simpl}(\phi ) = \bot$.   $\square$