In modal logic, the modal depth of a formula is the deepest nesting of modal operators (commonly ◻ {\displaystyle \Box } and ◊ {\displaystyle \Diamond } ). Modal formulas without modal operators have a modal depth of zero.
Definition Modal depth can be defined as follows. Let MD ( ϕ ) {\displaystyle \operatorname {MD} (\phi )} be a function that computes the modal depth for a modal formula ϕ {\displaystyle \phi } :
MD ( p ) = 0 {\displaystyle \operatorname {MD} (p)=0} , where p {\displaystyle p} is an atomic formula.
MD ( ⊤ ) = 0 {\displaystyle \operatorname {MD} (\top )=0}
MD ( ⊥ ) = 0 {\displaystyle \operatorname {MD} (\bot )=0}
MD ( ¬ φ ) = MD ( φ ) {\displaystyle \operatorname {MD} (\neg \varphi )=\operatorname {MD} (\varphi )}
MD ( φ ∧ ψ ) = max ( MD ( φ ) , MD ( ψ ) ) {\displaystyle \operatorname {MD} (\varphi \wedge \psi )=\max(\operatorname {MD} (\varphi ),\operatorname {MD} (\psi ))}
MD ( φ ∨ ψ ) = max ( MD ( φ ) , MD ( ψ ) ) {\displaystyle \operatorname {MD} (\varphi \vee \psi )=\max(\operatorname {MD} (\varphi ),\operatorname {MD} (\psi ))}
MD ( φ → ψ ) = max ( MD ( φ ) , MD ( ψ ) ) {\displaystyle \operatorname {MD} (\varphi \rightarrow \psi )=\max(\operatorname {MD} (\varphi ),\operatorname {MD} (\psi ))}
MD ( ◻ φ ) = 1 + MD ( φ ) {\displaystyle \operatorname {MD} (\Box \varphi )=1+\operatorname {MD} (\varphi )}
MD ( ◊ φ ) = 1 + MD ( φ ) {\displaystyle \operatorname {MD} (\Diamond \varphi )=1+\operatorname {MD} (\varphi )}
Example The following computation gives the modal depth of ◻ ( ◻ p → p ) {\displaystyle \Box (\Box p\rightarrow p)} :
MD ( ◻ ( ◻ p → p ) ) {\displaystyle \operatorname {MD} (\Box (\Box p\rightarrow p))}
= 1 + MD ( ◻ p → p ) {\displaystyle =1+\operatorname {MD} (\Box p\rightarrow p)}
= 1 + max ( MD ( ◻ p ) , MD ( p ) ) {\displaystyle =1+\max(\operatorname {MD} (\Box p),\operatorname {MD} (p))}
= 1 + max ( 1 + MD ( p ) , 0 ) {\displaystyle =1+\max(1+\operatorname {MD} (p),0)}
= 1 + max ( 1 + 0 , 0 ) {\displaystyle =1+\max(1+0,0)}
= 1 + 1 {\displaystyle =1+1}
= 2 {\displaystyle =2}
… excerpt ends here. Continue reading the full article.
