Solidez de las lógicas modales que contienen la regla de reflexión

Question

Dejemos que $ML$ sea una lógica modal que contenga la Regla de Reflexión (de $\vdash\Box F$ infiere $\vdash F$ ). Para una fórmula modal $F$ , dejemos que $H(F)=\{\ \Box G\rightarrow G~|~\Box G$ es una subfórmula de $F\}$ . Un modelo de Kripke para $ML$ se llama $F$ -sonido si la raíz del modelo satisface $H(F)$ .

Solidez . Si $ML\vdash F$ entonces $F$ es válido en cada $F$ -el modelo de Kripke de $ML$ .

La prueba de solidez es por inducción en la derivación de $F$ .

Mi pregunta es sobre la prueba de solidez en el paso de inducción cuando $F$ se obtiene por Modus Ponens a partir de $G$ y $G\rightarrow F$ . Desde $F$ -los modelos de sonido no son necesariamente $G$ -sonido y $(G\rightarrow F)$ -Modelos de sonido, no sé cómo manejar este caso.

Answer 1

No creo que tu estrategia de pruebas funcione tal y como está. Aquí hay una manera de demostrar el resultado. Supongamos que $\vdash_{ML}A$ y que $M$ sea un modelo con una raíz $r$ tal que $r\models\bigwedge H(A)$ . Dejemos que $M^\circ$ sea el modelo que difiere de $M$ sólo en ese $r$ se hace reflexivo (accesible desde sí mismo). Demostrar por inducción en la longitud de la prueba que $A$ tiene en $M^\circ$ . Entonces, utilizando el hecho de que $M,r\models H(A)$ , demuestran por inducción en la longitud de $B$ que para cada subfórmula $B$ de $A$ y cada $x\in M$ tenemos $$M,x\models B\iff M^\circ,x\models B.$$ Tomando $B=A$ entonces da que $A$ tiene en $M$ .

No has especificado la lógica de base $L$ sobre el que se añade el $\Box B\mathbin/B$ regla. El argumento anterior funciona siempre que $L$ es una lógica modal normal completa de Kripke cuya clase de marcos es cerrada bajo la operación de reflexivización que acabo de describir. (El supuesto de completitud de Kripke puede relajarse trabajando con marcos generales en su lugar). El resultado es en realidad falso para las lógicas modales normales en general. Por ejemplo, dejemos que $L=K\oplus\Box\bot$ . Entonces $L$ y la regla de la reflexión demuestra $\bot$ (es decir, es incoherente). Sin embargo, como $\bot$ no tiene ninguna subfórmula en caja, cada arraigada $L$ -El modelo es $\bot$ -Sonido.

Nótese que la mayoría de las lógicas modales definidas naturalmente $L$ de hecho ya están cerradas bajo la regla de la reflexión (es decir, la regla de la reflexión es $L$ -admisible). Aparte de las extensiones de T (obviamente), esto es válido, por ejemplo, para la lógica normal mínima K, así como para K4, D, GL, etc. En estos casos, simplemente se obtiene que una fórmula $A$ demostrable mediante la regla de la reflexión es válida en todo modelos, ya sea $A$ -sano o no. Una forma de demostrar la admisibilidad de $\Box B\mathbin/B$ en una lógica $L$ es utilizar una modificación de la construcción anterior, donde en lugar de cambiar la reflexividad de $r$ , se adjunta un nuevo punto reflexivo $s$ que ve $r$ y todos sus sucesores. Para lógicas como GL que no permiten puntos reflexivos en absoluto, se puede adjuntar a $r$ una cadena descendente infinita de puntos irreflexivos; entonces se demuestra que toda fórmula demostrable mediante la regla de reflexión es verdadera en el nuevo modelo (y por tanto en el modelo antiguo, que es su submodelo generado) por inducción en la longitud de la prueba.