Profondità modale

Nella logica modale, la profondità modale è il massimo livello di annidamento degli operatori modali (tipicamente $\Box$ e $\Diamond$). Le formule modali prive di operatori modali hanno profondità modale nulla.

Definizione

La profondità modale può essere definita nel modo seguente. Sia $MD(\phi )$ una funzione matematica che calcola la profondità modale della formula $\phi$:

1. $MD(p)=0$, dove $p$ è una formula atomica.
2. $MD(\top )=0$
3. $MD(\bot )=0$
4. $MD(\neg \varphi )=MD(\varphi )$
5. $MD(\varphi \wedge \psi )=max(MD(\varphi ),MD(\psi ))$
6. $MD(\varphi \vee \psi )=max(MD(\varphi ),MD(\psi ))$
7. $MD(\varphi \rightarrow \psi )=max(MD(\varphi ),MD(\psi ))$
8. $MD(\Box \varphi )=1+MD(\varphi )$
9. $MD(\Diamond \varphi )=1+MD(\varphi )$

Le formule sopra enunciate sono tra loro indipendenti.

Esempi

L'esempio seguente calcola la profondità modale della formula $\Box (\Box p\rightarrow p)$:

$MD(\Box (\Box p\rightarrow p))=$

dalla (8): $1+MD(\Box p\rightarrow p)=$

dalla (7): $1+max(MD(\Box p),MD(p))=$

dalla (8) e dalla (1): $1+max(1+MD(p),0)=$

dalla (1): $1+max(1+0,0)=$

$1+1=:2$

Profondità modale e semantica

La profondità modale di una formula indica 'quanto lontano' bisogna guardare in un modello di Kripke quando la formula è valida. Per ogni operatore modale è necessario passare da un mondo nel modello a un mondo accessibile attraverso la relazione di accessibilità. La profondità modale indica la "catena" più lunga di transizioni da un mondo all'altro necessaria per verificare la validità di una formula.

Ad esempio, per verificare se $M,w\models \Diamond \Diamond \varphi$, è necessario verificare se esiste un mondo accessibile $v$ per ogni $M,v\models \Diamond \varphi$. Se ciò è vero, è necessario verificare se esiste anche un mondo $u$ tale che $M,u\models \varphi$ e che $u$è accessibile da $v$. Si hano due passaggi dal mondo $w$ (da $w$ a $v$ e da $v$ a $u$) nel modello per determinare se la formula sia vera; e questo è per definizione la profondità modale di tale formula.

Una formula modale è anche vera ogni volta che un mondo non ha altri mondi accessibili (in simboli: $\Box \varphi$ è vera per ogni $\varphi$ in un mondo $w$ quando $\forall v\in W\ (w,v)\not \in R$, dove $W$ è l'insieme dei mondi possibili e $R$ è la relazione di accessibilità). Per verificare se $M,w\models \Box \Box \varphi$ sia vera, può essere necessario percorrere due passaggi nel modello, ovvero un numero minore, a seconda del modello stesso. Si supponga che non via siano mondi accessibili da $w$: banalmente, la formula è valida in base alla precedente osservazione sulle formule che hanno $\Box$ come operatore esterno.