syntactic properties of a normal modal logic

Recall that a normal modal logic is a logic containing all tautologiesMathworldPlanetmath, the schema K


and closed underPlanetmathPlanetmath modus ponensMathworldPlanetmath and necessitation rules. Also, the modal operator diamond is defined as


Let Λ be any normal modal logic. We write A to mean ΛA, or wff AΛ, or A is a theorem of Λ. In addition, for any set Δ, ΔA means there is a finite sequencePlanetmathPlanetmath 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 A is the last wff in the sequence. The sequence is called a deductionMathworldPlanetmathPlanetmath (of A) from Δ.

Below are some useful meta-theorems of Λ:

  1. 1.

    (RM) AB implies AB


    By assumption and by necessitation, (AB), by schema K and by modus ponens, we have the result. ∎

  2. 2.

    As a result, AB implies AB.

  3. 3.

    (substitution theorem). If BiCi for i=1,,m, then


    where p¯:=(p1,,pm) is the tuple of all the propositional variables in A listed in order.


    For most of the proof, consult this entry ( for more detail. What remains is the case when A has the form D. We do inductionMathworldPlanetmath on the number n of ’s in A. The case when n=0 means that A is a wff of PLc, and has already been proved. Now suppose A has n+1 ’s. Then D has n ’s, and so by induction, D[B/p]D[C/p], and therefore D[B/p]D[C/p] by 2. This means that A[B/p]A[C/p]. ∎

  4. 4.

    AB implies AB


    By assumption, tautology (AB)(¬B¬A), and modus ponens, we get ¬B¬A. By 1, ¬B¬A. By another instance of the above tautology and modus ponens, and the definition of , we get the result. ∎

  5. 5.

    AB implies AB


    Since AB(¬AB), we have ¬AB, so ¬AB. By the tautology C¬¬C, we have ¬¬¬AB, or ¬AB, and therefore AB. ∎

  6. 6.

    (RR) ABC implies ABC


    By assumption and 1, (AB)C. Since AB(AB) is a theorem (see here (, we get ABC by the law of syllogism. ∎

  7. 7.

    (RK) More generally, A1AnA implies A1AnA, where the case n=0 is the necessitation rule.


    Cases n=1,2 are meta-theorems 1 and 6. If A1AnAn+1A, or (A1An)An+1A, then (A1An)An+1A by 6. But (A1An)A1An, the result follows. ∎

  8. 8.

    Define a function s on {¬,λ}, where λ is the empty wordPlanetmathPlanetmathPlanetmath, such that s(¬)=λ, the empty word, and s(λ)=¬. Then for any wff A, and ϵ1,ϵ2{¬,λ}:


    Technically speaking, this is really an infiniteMathworldPlanetmath collectionMathworldPlanetmath of theorem schemas.


    We will check the case when ϵ1=¬ and ϵ2=λ and leave the rest to the reader. We do induction on n. If n=0, then we have the tautology ¬A¬A. Suppose ¬nAn¬A. Then ¬n+1An¬A, by applying the induction case on wff A. Since A¬¬A is a tautology, ¬n+1An¬¬¬A by the substitution theorem. By the definition of , we have ¬n+1An+1¬A. ∎

  9. 9.

    Let Δ:={AAΔ}. Then ΔA implies ΔA.


    Induct on the length n of deduction of A from Δ. If n=0, then either A, in which case A by necessitation, or AΔ, in which case AΔ. In either case, ΔA. Next suppose the property holds for all deductions of length n, and there is a deduction of A of length n+1. If A is obtained from Δ by necessitation, say A is B, where B is in , then a subsequence of is a deduction of B of length n, from Δ. So by induction, ΔB, or ΔA. By necessitation, ΔA. Finally, if A is obtained by modus ponens, then there is a wff B such that B,BA are both in . By induction, ΔB and Δ(BA), which, by K and modus ponens, ΔBA, and as a result, ΔA by modus ponens. ∎

Noticeably absent is the deduction theoremMathworldPlanetmath, for the necessitation rule says AA, but this does not imply AA. In fact, the wff AA is not a theorem in general, unless of course the logic includes the entire schema. All we can say is the following:

  1. 10.

    (deduction theorem) If Δ,AB and B is not of the form C, then ΔAB.

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 (

Title syntactic properties of a normal modal logic
Canonical name SyntacticPropertiesOfANormalModalLogic
Date of creation 2013-03-22 19:34:18
Last modified on 2013-03-22 19:34:18
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 24
Author CWoo (3771)
Entry type Definition
Classification msc 03B45