Lógica modal no normal

Una lógica modal no normal es una variante de la lógica modal que se desvía de los principios básicos de las lógicas modales normales .

Las lógicas modales normales se adhieren al axioma de distributividad ( ) y al principio de necesidad que establece que "una tautología debe ser necesariamente verdadera" ( implica ). ^[1] Por otro lado, las lógicas modales no normales no siempre tienen tales requisitos. La variante mínima de las lógicas modales no normales es la lógica E , que contiene la regla de congruencia en su cálculo de Hilbert o la regla E en su cálculo consecuente sobre los sistemas de prueba correspondientes para la lógica proposicional clásica . Se pueden agregar axiomas adicionales, a saber, los axiomas M , C y N , para formar sistemas lógicos más fuertes. Con los tres axiomas agregados a la lógica E , se obtiene un sistema lógico equivalente a la lógica modal normal K . ^[2]${\displaystyle \Caja (p\a q)\a (\Caja p\a \Caja q)}$${\displaystyle \vdash A}$${\displaystyle \vdash \Cuadro A}$

Si bien la semántica de Kripke es la semántica formal más común para las lógicas modales normales (por ejemplo, la lógica K ), las lógicas modales no normales a menudo se interpretan con la semántica de vecindad .

La sintaxis de los sistemas de lógica modal no normal se asemeja a la de las lógicas modales normales, que se basan en la lógica proposicional. Un enunciado atómico se representa con variables proposicionales (por ejemplo, ); los conectores lógicos incluyen la negación ( ), la conjunción ( ), la disyunción ( ) y la implicación ( ). Las modalidades se representan más comúnmente con el recuadro ( ) y el rombo ( ).${\estilo de visualización p,q,r}$${\estilo de visualización \neg}$${\displaystyle \tierra}$${\displaystyle \lor}$${\displaystyle \to}$${\displaystyle \Cuadro}$${\displaystyle \Diamond }$

Una gramática formal para esta sintaxis se puede definir mínimamente utilizando solo los símbolos de negación, disyunción y caja. En un lenguaje de este tipo, donde es cualquier nombre proposicional. ^[3] La conjunción puede entonces definirse como equivalente a . Para cualquier fórmula modal , la fórmula se define por . Alternativamente, si el lenguaje se define primero con el rombo, entonces la caja se puede definir análogamente por . ^[4]${\displaystyle \varphi ,\psi :=p\ |\ \neg \varphi \ |\ \Box \varphi \ |\ \varphi \lor \psi }$${\displaystyle p}$${\displaystyle \varphi \land \psi }$${\displaystyle \neg (\neg \varphi \lor \neg \psi )}$${\displaystyle \varphi }$${\displaystyle \Diamond \varphi }$${\displaystyle \neg \Box \neg \varphi }$${\displaystyle \Box \varphi \equiv \neg \Diamond \neg \varphi }$

Para cualquier nombre proposicional , las fórmulas y se consideran literales proposicionales, mientras que y se consideran literales modales .${\displaystyle p}$${\displaystyle p}$${\displaystyle \neg p}$${\displaystyle \Box p}$${\displaystyle \neg \Box p}$

La lógica E , la variante mínima de las lógicas modales no normales, incluye la regla de congruencia RE en su cálculo de Hilbert o la regla E en su cálculo secuente.

El cálculo de Hilbert para lógica E se basa en el de lógica proposicional clásica con la regla de congruencia ( RE ): . Alternativamente, la regla puede definirse por . Las lógicas que contienen esta regla se denominan congruenciales .${\displaystyle {\frac {A\leftrightarrow B}{\Box A\leftrightarrow \Box B}}}$${\displaystyle {\frac {A\leftrightarrow B}{\Diamond A\leftrightarrow \Diamond B}}}$

El cálculo secuencial para lógica E , otro sistema de prueba que opera con secuenciales , consiste en las reglas de inferencia para lógica proposicional y la regla E de inferencia: .${\displaystyle {\frac {A\vdash B\qquad B\vdash A}{\Gamma ,\Box A\vdash \Box B,\Delta }}}$

El consecuente significa , siendo el antecedente (una conjunción de fórmulas como premisas) y siendo el precedente ( una disyunción de fórmulas como conclusión).${\displaystyle \Gamma \vdash \Delta }$${\displaystyle \Gamma }$${\displaystyle \Delta }$${\displaystyle \Gamma }$${\displaystyle \Delta }$

El cálculo de resolución para lógicas modales no normales introduce el concepto de modalidades globales y locales. La fórmula denota la modalidad global de la fórmula modal , lo que significa que es válida en todos los mundos de un modelo de vecindad. Para la lógica E , el cálculo de resolución consta de las reglas LRES, GRES, G2L, LERES y GERES. ^[3]${\displaystyle {\mathsf {G}}(\varphi )}$${\displaystyle \varphi }$${\displaystyle \varphi }$

La regla LRES se parece a la regla de resolución para la lógica proposicional clásica, donde se eliminan todos los literales proposicionales y : .${\displaystyle p}$${\displaystyle \neg p}$${\displaystyle {\frac {D\lor l\qquad D'\lor \neg l}{D\lor D'}}}$

La regla LERES establece que si dos nombres proposicionales y son equivalentes, entonces y pueden eliminarse. La regla G2L establece que cualquier fórmula globalmente verdadera también es localmente verdadera. Las reglas de inferencia GRES y GERES, aunque son variantes de LRES y LERES, se aplican a fórmulas que presentan la modalidad global.${\displaystyle p}$${\displaystyle p'}$${\displaystyle \Box p}$${\displaystyle \neg \Box p'}$

Dada cualquier fórmula modal, el proceso de demostración con este cálculo de resolución se realiza renombrando recursivamente una fórmula modal compleja como un nombre proposicional y usando la modalidad global para afirmar su equivalencia.

Si bien la semántica de Kripke se aplica a menudo como la semántica de las lógicas modales normales, la semántica de las lógicas modales no normales se define comúnmente con modelos de vecindad. Un modelo de vecindad estándar se define con la tripleta donde: ^{[5] [6]}${\displaystyle {\mathcal {M}}}$${\displaystyle \langle {\mathcal {W}},{\mathcal {N}},{\mathcal {V}}\rangle }$

• ${\displaystyle {\mathcal {W}}}$es un conjunto no vacío de mundos .
• ${\displaystyle {\mathcal {N}}:{\mathcal {W}}\to {\mathcal {PP}}({\mathcal {W}})}$es la función de vecindad que asigna cualquier mundo a un conjunto de mundos. La función denota un conjunto potencia .${\displaystyle {\mathcal {P}}}$
• ${\displaystyle {\mathcal {V}}:Atm\to {\mathcal {P}}({\mathcal {W}})}$es la función de valoración que, dado cualquier nombre proposicional , genera un conjunto de mundos donde es verdadero.${\displaystyle p}$${\displaystyle p}$

La semántica puede generalizarse aún más como semántica de bi-vecindario. ^[7]

El cubo clásico de la lógica modal no normal considera los axiomas M, C y N que pueden agregarse a la lógica E definida de la siguiente manera. ^[6]

Axiomas adicionales para lógicas modales no normales

Axioma	Definición	Definición alternativa	Semántica de vecindad correspondiente
METRO	${\displaystyle \Box (A\land B)\to \Box A}$	${\displaystyle \Diamond A\to \Diamond (A\land B)}$	Si y , entonces .${\displaystyle \alpha \in {\mathcal {N}}(w)}$${\displaystyle \alpha \subseteq \beta }$${\displaystyle \beta \in {\mathcal {N}}(w)}$
do	${\displaystyle \Box A\land \Box B\to \Box (A\land B)}$	${\displaystyle \Diamond (A\lor B)\to \Diamond A\lor \Diamond B}$	Si , entonces .${\displaystyle \alpha ,\beta \in {\mathcal {N}}(w)}$${\displaystyle \alpha \cap \beta \in {\mathcal {N}}(w)}$
norte	${\displaystyle \Box \top }$	${\displaystyle \neg \Diamond \bot }$	${\displaystyle {\mathcal {W}}\in {\mathcal {N}}(w)}$.

Un sistema lógico que contiene el axioma M es monótono . Con los axiomas M y C, el sistema lógico es regular . Incluyendo los tres axiomas, el sistema lógico es normal .

Con estos axiomas se incluyen reglas adicionales en sus sistemas de prueba correspondientes.