We want our deduction rules to be sound, that is ⊢ φ+ ⇒ ⊨ φ+. This can be shown by induction over the length of the deduction. First we show that the axioms are valid and then that the rules preserve validity.
In all cases let M be an arbitrary model, and s a world in that model. The validity of our axioms is trivial,
For each rule we will show that it preserves validity; if the premises are valid then so is the conclusion. So if we have a rule
We need to show that if M,s ⊨ Γ then also M,s ⊨ Δ.
For the negation rule this is simple,
Slightly more interesting are the disjunction
and conjunction rules,
Note that we only show the proof of one of each kind of rule, since the other rules are simply the De Morgan duals.
Since we have made no assumptions about M and s, the axioms and rules are valid in all possible models and worlds. This means that all propositional rules preserve semantic validity. If the premises are valid, then so is the conclusion.
Now given a derivation of ⊢ φ+, by induction over the structure of this derivation it holds that ⊨ φ+.
Recall that we added a copying mechanism to all rules. This does not affect validity and hence soundness, since X ∨ X is equivalent to X. See for example the disjunction rule:
The key to the modal proof system is deep rule application. This was formulated as three meta-rules.
To show that a transformed rule “deep R for i” preserves validity first assume that rule "R" does. That is to say, if M,t ⊨ Γ then M,t ⊨ Δ, for all worlds t (and all models M). The the “deep R for i” rule will also preserve validity:
The proof for the case with zero and with two sequents above the line is analogous.
Now let us look at the modal rules. First the box rule. Validity is simple, because the semantics of [φ+]i are exactly the same as those of □iφ+.
The diamond rule is harder, it states that if in each world Δ or φ+ holds, then either Δ holds everywhere, or there is a world in which Δ does not hold and where hence φ+ holds.
Again, soundness holds by induction over derivations.
We have also introduced rules for classes of models such as those were relations are reflexive or transitive. These rules are not valid in all models, but only in those models that have these extra properties.
A relation R is serial if ∀x ∃y xRy, there is always an outgoing relation. Let M be a serial model, then the D rule is valid:
A relation R is reflexive if ∀x xRx. For all reflexive models M the T rule preserves validity:
A relation R is transitive if ∀x,y,z (xRy ∧ yRz) → xRz. Let M be a transitive model, then the 4 rule preserves validity:
And finally, a relation R is euclidean if ∀x,y,z (xRy ∧ xRz) → yRz. Let M be a euclidean model, then the 5 rule preserves validity:
We have now shown that all rules we have introduced preserve semantic validity. If the assumptions are valid, then so is the conclusion. Now given a derivation of φ, by induction over the structure of that derivation it must be the case that φ is valid, possibly with respect to a class of Kripke models.