One thing we were discussing in class was which modal operators distributed over which connectives. One can quickly persuade oneself that when all instances of this schema are theorems of a modal system:
\(\operatorname{\script O}(\phi \mathbin{\star}\psi) \cond (\operatorname{\script O}\phi \mathbin{\star}\operatorname{\script O}\psi)\)
where \(\operatorname{\script O}\) is a modal operator (\(\Box\) or \(\Diamond\)) and \(\mathbin{\star}\) is any truth-functional connective, and the modal system includes classical sentential logic, that's equivalent to all instances of the following schema being theorems:
\((\operatorname{\hat{\script O}}\phi \mathbin{\hat\star}\operatorname{\hat{\script O}}\psi) \cond \operatorname{\hat{\script O}}(\phi \mathbin{\hat\star}\psi)\)
where \(\operatorname{\hat{\script O}}\) is the dual operator to \(\operatorname{\script O}\), and \(\mathbin{\hat\star}\) is the dual connective to \(\mathbin{\star}\) (\(\wedge\) and \(\vee\) being duals, and \(\cond\) and \(\not\subset\) also being duals). You should be able to prove this with only a little effort.
Let's call the first sort of schema a "distribution" of the relevant operator; and the second sort of schema an "undistribution" of the operator.
Any modal system that includes the \(K\) axioms will make \(\Box\) distribute over \(\cond\). Sider shows us the proofs that \(\Box\) will also distribute over \(\wedge\) (Example 6.6); and that \(\Box\) will undistribute over \(\vee\) (Example 6.7) and \(\wedge\) (Example 6.8). Using the equivalences stated above, that permits us to draw some conclusions about the distribution behavior of \(\Diamond\). Using that and other techniques, I worked out the following results --- I believe it's correct but if you find a mistake, let me know. "D" in a cell means that that modal operator distributes over that connective; the absence of a "D" means it doesn't. Similarly for "U" which indicates undistribution.
| \(\Box\) | \(\Diamond\) | ||
|---|---|---|---|
| \(\vee\) | .U | DU | |
| \(\wedge\) | DU | D. | |
| \(\cond\) | D. | .U |
The second thing I'll address is to give you a roadmap of how the Soundness proofs for these modal systems go. Consult Sider's text for the details; these remarks try to step back a bit and give a wide-angle overview of how he's proceeding.
We want to show, for some modal system \(S\), that: if \(\proves_S\phi\) then \(\models_S\phi\). The \({}_S\) subscript in the antecedent refers to the axiomatic system \(S\); in the consequent it refers to the class of "\(S\)-models". The Soundness and Completeness proofs for "system S" are what earn us the right to call these by the same name.
An important step towards proving Soundness is Sider's Theorem 6.1. Before stating that Theorem, let's describe the lemmas he uses to prove it.
Lemma 6.2 has two components, which we can call (6.2a) and (6.2b). Sider doesn't give them separate names. (6.2a) says that all classical sentential logic (PL) axioms are "valid" in all sentential modal models (what Sider calls "MPL models"). If you look on p. 141, you'll see that a modal formula is called "valid" in a specific model (as opposed to the more familiar notion of being valid in a system) when that model makes the formula true in every world. This parallels the notion of a predicate logic formula being true under every assignment in a specific model; but the latter notion is called being "true" in the model, rather than being "valid" in the model. (See Sider p. 95.) This is just a quirk in the customary vocabulary. Anyway, with this understood, (6.2a) is saying that any classical sentential logic axiom will be true in every world in all modal models. Sider proves this on p. 174.
(6.2b) says that every axiom specific to the modal system \(K\) is also valid in all modal models, that is, true in every world in all modal models. The proof of this is left as Exercise 6.12.
Lemma (6.3) says that the rules Modus Ponens and NEC preserve validity in all modal models. This is left as exercise 6.13.
Given those lemmas, Sider proves:
Theorem 6.1. If every wff in a set \(\Gamma\) is valid in sentential modal model \(\script M\), then every theorem of the modal system \(K+\Gamma\) will also be valid in \(\script M\).
This proof (on p. 174) is short enough to summarize here. Any theorem of modal system \(K+\Gamma\) will have an axiomatic proof. Each line of the proof will either be (i) an axiom of classical sentential logic; or (ii) an instance of the \(K\) axiom schema; or (iii) a member of \(\Gamma\); or (iv) will follow from previous lines by an application of MP or NEC. By lemma (6.2a) we know that a line of type (i) will be valid in \(\script M\). By lemma (6.2b) we know that a line of type (ii) will be valid in \(\script M\). By the antecedent of Theorem 6.1, we know that a line of type (iii) will be valid in \(\script M\). Finally, by lemma (6.3) we know that a line of type (iv) will be valid in \(\script M\). So every line of the proof --- including its conclusion --- will be valid in \(\script M\).
Once Theorem 6.1 is established, to establish Soundness for modal system \(S\), one only needs to show that the axioms that \(S\) adds to the \(K\) axioms are valid in all models whose accessibility relations are constrained in the way models called "\(S\)-models" are. Then our Theorem 6.1 will tell us that every theorem of the axiomatic system \(S\) will be valid in all those same models.
This is demonstrated for the modal systems \(K\), \(T\), and \(B\) on pp. 174--5.
I also want to give you a wide-angle overview of the Completeness proofs. This will take longer.
What we're trying to show is that: if \(\models_S\phi\), then \(\proves_S\phi\). The \({}_S\) subscript in the antecedent means "in any \(S\)-model", and in the consequent it means "in axiomatic system \(S\)".
We build what we call a "canonical model" for \(S\), which I'll abbreviate as \(canon(S)\). One of the things we have to prove is that such a model does count as an \(S\)-model; that is, that its accessibility relation is constrained in the way that \(S\)-models are. That will be a substantial result.
One of the things we have to get clear on when talking about a modal system \(S\) is how to understand the notion of an "\(S\)-proof from premises"; this isn't straightforward because the modal rule NEC only applies to formulas that are already in themselves theorems, not to all formulas that are consequences of some assumed premises. Sider introduces the way we should understand an \(S\)-proof from premises on p. 176. In short:
\(\Gamma \proves_S \phi\) means there is some finite subset \(\set{\gamma_1,\dots,\gamma_n}\) of \(\Gamma\), such that \(\proves_S (\gamma_1\wedge\dots\wedge\gamma_n) \cond \phi\).
Next we introduce the notion of a set of modal formulas \(\Gamma\) being \(S\)-consistent (\(\Gamma\not\proves_S\bot\)) and maximal (that is, deductively complete: for every \(\phi\), either \(\phi\in\Gamma\) or \(\neg\phi\in\Gamma\)).
Next we introduce the notion of the \(\operatorname{stripone}\) operation on a set of formulas. This discards all the formulas in the set that don't start with \(\Box\), and then for each formula that's left, gives us the formula that's embedded inside the outermost \(\Box\).
Given those tools, any model \(canon(S)\) will have worlds that are maximal \(S\)-consistent sets of wffs. It will have an accessibility relation \(\script R\) such that \(\script Ruv\) iff \(\operatorname{stripone} u \se v\). And it will have an interpretation function that assigns an atomic formula \(\phi\) the value \(\True\) at a world \(w\) iff \(\phi\in w\).
The reason we're not yet in a position to claim that this is an "\(S\)-model" is that the construction doesn't explicitly tell us what the formal properties of its accessibility relation are (that is, whether it's serial, reflexive, symmetric, transitive).
By its construction, though, we can immediately see that for atomic formulas \(\phi\), \(\interp{\phi}_{canon(S)\,w}\) will be \(\True\) iff \(\phi\in w\). We'll need to prove that this is true for all formulas \(\phi\). That will be Theorem (Corollary) 6.8.
To get to that result, Sider first proves:
Theorem 6.4. Every \(S\)-consistent set of wffs has a maximal \(S\)-consistent superset (proved on p. 177; compare Theorem 2.3 proved on p. 63).
Theorem 6.5. If \(\Gamma\) is a maximal \(S\)-consistent set of wffs, then:
- exactly one of \(\phi\) and \(\neg\phi\) is \(\!{}\in\Gamma\) (that is, \(\Gamma\) is deductively complete)
- \(\phi\cond\psi \in \Gamma\) iff \(\phi\not\in\Gamma\) or \(\psi\in\Gamma\)
- if \(\proves_S\phi\) then \(\phi\in\Gamma\) (proved on p. 178)
- if \(\proves_S \phi\cond\psi\) and \(\phi\in\Gamma\) then \(\psi\in\Gamma\) (can be proved using (b) and (c))
Parts (a) and (b) of this theorem parallel Lemma 2.4 on p. 65. Proving them requires showing that the new notion of an "\(S\)-proof from premises" has some of the same formal properties as \(\proves\) in classical sentential logic. The least straightforward of these properties is satisfying a Deduction Theorem; but Sider proves that the new notion has this property on p. 178.
Another thing Sider needs to show is that: if \(\Box\phi \in w\) and \(\script Rwu\) then \(\phi\in u\). This follows straightforwardly from the definition of \(canon(S)\)'s accessibility relation \(\script R\). Sider also needs to show an analogous result for \(\Diamond\phi\). He gets the effect of that by instead proving the following about \(\neg\Box\psi\):
Lemma 6.6. If \(\neg\Box\psi \in\) a maximal \(S\)-consistent set \(w\), then \(\neg\psi \in\) some maximal \(S\)-consistent superset of \(\operatorname{stripone} w\) (proved on pp. 179--80)
Sider is now in a position to prove the important Theorem 6.7, which is a tool he uses to prove our target Theorem (Corollary) 6.8. Here is 6.7:
Theorem 6.7. If \(canon(S) = \tuple{\script W, \script R, \script I}\) is a model for modal system \(K+\Gamma\), then for all wff \(\phi\) and for all \(w\in\script W\), \(\interp{\phi}_{canon(S)\,w}\) is \(\True\) iff \(\phi\in w\).
Sider proves this by induction on the complexity of \(\phi\). The base case is clear by the definition of \(\script I\) for \(canon(S)\). We then have to prove that if it holds for some wffs \(\phi\) and \(\psi\), it also holds for (i) \(\neg\phi\); for (ii) \(\psi\cond\psi\); and for (iii) \(\Box\phi\).
The proofs of (i) and (ii) use Theorem (6.5a) and (6.5b) in a way that parallels the proofs of corresponding claims on p. 66, in Sider's completeness proof for classical sentential logic.
The proof of (iii) is given on p. 180. Here is the left-to-right direction: Assume \(\interp{\Box\phi}_{canon(S)\,w}\) is \(\True\). Then \(\interp{\phi}_{canon(S)\,v}\) is \(\True\) for every \(v\) where \(\script Rwv\). Then by our inductive hypothesis about \(\phi\), \(\phi\in v\). Now assume for reductio that \(\Box\phi\not\in w\). Then since \(w\) is maximal, \(\neg\Box\phi\in w\). Then by Lemma 6.6, \(\neg\phi \in\) some maximal \(S\)-consistent superset \(u\) of \(\operatorname{stripone} w\). Then by definition of \(\script R\), \(\script Rwu\). Then since, as we said, \(\phi\in\) every \(v\) where \(\script Rwv\), \(\phi\in u\). But now we have both \(\neg\phi\in u\) and \(\phi\in u\), contradicting \(u\)'s consistency. So our reductio assumption is false: \(\Box\phi\in w\), after all.
Here is the right-to-left-direction: Assume \(\Box\phi\in w\). Then by definition of \(\script R\), \(\phi\in\) every \(v\) where \(\script Rwv\). Then by our inductive hypothesis about \(\phi\), \(\interp{\phi}_{canon(S)\,v}\) for every such \(v\). But then by the semantic rule for \(\Box\), \(\interp{\Box\phi}_{canon(S)\,w}\) is \(\True\).
With Theorem 6.7 in hand, Sider can prove Theorem (Corollary) 6.8:
Theorem 6.8. For every wff \(\phi\): \(\phi\) is valid in \(canon(S)\) iff \(\proves_S\phi\).
The proof is on p. 181. Here is the left-to-right direction: Suppose \(\not\proves_S\phi\). Then if \(\neg\phi\) were \(S\)-inconsistent, then \(\proves_S\neg\phi\cond\bot\) and so \(\proves_S\phi\). Hence \(\neg\phi\) is \(S\)-consistent. By Theorem 6.4, it follows that \(\set{\neg\phi}\) has a maximal \(S\)-consistent superset \(w\). By Theorem 6.7, it follows that \(\interp{\neg\phi}_{canon(S)\,w}\) is \(\True\). So \(\phi\) would not be valid in \(canon(S)\).
Here is the right-to-left direction: Suppose \(\proves_S\phi\). By Theorem (6.5c), it follows that \(\phi\in\) every world \(w\) in \(canon(S)\). By Theorem 6.7, it follows that \(\interp{\phi}_{canon(S)\,w}\) is \(\True\) in every such \(w\). So \(\phi\) is valid in \(canon(S)\).
Once Theorem 6.8 is established, finishing the Completeness proof for a given modal system \(S\) just requires showing that in \(canon(S)\), the accessibility relation does have the properties necessary for being an "\(S\)-model" (that it's serial, reflexive, or whatever). Once you do that, you can reason:
Suppose \(\models_S{\phi}\).
That means that \(\phi\) is valid in every modal model with an accessibility relation with properties so-and-so.
But \(canon(S)\) is such a model. (Sider demonstrates this for systems \(K\), \(D\), and \(B\) on p. 181.)
By Theorem 6.8, it follows that \(\proves_S\phi\).
Which gives us Completeness for system \(S\).