Profundidad modal

En lógica modal , la profundidad modal de una fórmula es el anidamiento más profundo de operadores modales (comúnmente y ). Las fórmulas modales sin operadores modales tienen una profundidad modal de cero. ${\ Displaystyle \ Box}$ ${\ Displaystyle \ Diamond}$

La profundidad modal se puede definir de la siguiente manera. ^[1] Sea una función que calcula la profundidad modal para una fórmula modal : ${\ Displaystyle MD (\ phi)}$ ${\ Displaystyle \ phi}$

El siguiente cálculo da la profundidad modal de : ${\ Displaystyle \ Box (\ Box p \ rightarrow p)}$

La profundidad modal de una fórmula indica 'qué tan lejos' se necesita mirar en un modelo de Kripke al verificar la validez de la fórmula. Para cada operador modal, es necesario pasar de un mundo en el modelo a un mundo que es accesible a través de la relación de accesibilidad . La profundidad modal indica la 'cadena' más larga de transiciones de un mundo al siguiente que se necesita para verificar la validez de una fórmula.

Por ejemplo, para comprobar si es necesario comprobar si existe un mundo accesible para el cual . Si ese es el caso, es necesario comprobar si también existe un mundo tal y desde el que se puede acceder . Hemos realizado dos pasos desde el mundo (desde hacia y desde hacia ) en el modelo para determinar si la fórmula es válida; esta es, por definición, la profundidad modal de esa fórmula. ${\ Displaystyle M, w \ modelos \ Diamante \ Diamante \ varphi}$ ${\ Displaystyle v}$ ${\ Displaystyle M, v \ modelos \ Diamante \ varphi}$ ${\ Displaystyle u}$ ${\ Displaystyle M, u \ modelos \ varphi}$ ${\ Displaystyle u}$ ${\ Displaystyle v}$ ${\ Displaystyle w}$ ${\ Displaystyle w}$ ${\ Displaystyle v}$ ${\ Displaystyle v}$ ${\ Displaystyle u}$

La profundidad modal es un límite superior (inclusivo) en el número de transiciones como para los cuadros, una fórmula modal también es cierta siempre que un mundo no tiene mundos accesibles (es decir, se aplica a todos en un mundo cuando , dónde está el conjunto de mundos y es la relación de accesibilidad). Para comprobar si , puede ser necesario realizar dos pasos en el modelo, pero podría ser menos, dependiendo de la estructura del modelo. Supongamos que no hay mundos accesibles en ; la fórmula ahora se sostiene trivialmente por la observación anterior sobre la validez de fórmulas con un cuadro como operador externo. ${\ Displaystyle \ Box \ varphi}$ ${\ Displaystyle \ varphi}$ ${\ Displaystyle w}$ ${\ Displaystyle \ forall v \ in W \ (w, v) \ not \ in R}$ ${\ Displaystyle W}$ ${\ Displaystyle R}$ ${\ Displaystyle M, w \ modelos \ Box \ Box \ varphi}$ ${\ Displaystyle w}$