syntactic properties of a normal modal logic
Let be any normal modal logic. We write to mean , or wff , or is a theorem of . In addition, for any set , means there is a finite sequence of wff’s such that each wff is either a theorem, a member of , or obtained either by modus ponens or necessitation from earlier wff’s in the sequence, and is the last wff in the sequence. The sequence is called a deduction (of ) from .
Below are some useful meta-theorems of :
By assumption and by necessitation, , by schema K and by modus ponens, we have the result. ∎
As a result, implies .
(substitution theorem). If for , then
where is the tuple of all the propositional variables in listed in order.
For most of the proof, consult this entry (http://planetmath.org/SubstitutionTheoremForPropositionalLogic) for more detail. What remains is the case when has the form . We do induction on the number of ’s in . The case when means that is a wff of PL, and has already been proved. Now suppose has ’s. Then has ’s, and so by induction, , and therefore by 2. This means that . ∎
By assumption, tautology , and modus ponens, we get . By 1, . By another instance of the above tautology and modus ponens, and the definition of , we get the result. ∎
Since , we have , so . By the tautology , we have , or , and therefore . ∎
By assumption and 1, . Since is a theorem (see here (http://planetmath.org/SomeTheoremSchemasOfNormalModalLogic)), we get by the law of syllogism. ∎
(RK) More generally, implies , where the case is the necessitation rule.
Cases are meta-theorems 1 and 6. If , or , then by 6. But , the result follows. ∎
We will check the case when and and leave the rest to the reader. We do induction on . If , then we have the tautology . Suppose . Then , by applying the induction case on wff . Since is a tautology, by the substitution theorem. By the definition of , we have . ∎
Let . Then implies .
Induct on the length of deduction of from . If , then either , in which case by necessitation, or , in which case . In either case, . Next suppose the property holds for all deductions of length , and there is a deduction of of length . If is obtained from by necessitation, say is , where is in , then a subsequence of is a deduction of of length , from . So by induction, , or . By necessitation, . Finally, if is obtained by modus ponens, then there is a wff such that are both in . By induction, and , which, by K and modus ponens, , and as a result, by modus ponens. ∎
Noticeably absent is the deduction theorem, for the necessitation rule says , but this does not imply . In fact, the wff is not a theorem in general, unless of course the logic includes the entire schema. All we can say is the following:
(deduction theorem) If and is not of the form , then .
Remark. It can be shown that conversely, if a modal logic obeys meta-theorem 7 above as an inference rule, then it is normal. For more detail, see here (http://planetmath.org/EquivalentFormulationsOfNormality).
|Title||syntactic properties of a normal modal logic|
|Date of creation||2013-03-22 19:34:18|
|Last modified on||2013-03-22 19:34:18|
|Last modified by||CWoo (3771)|