Me han llegado a través de estudios que comparan la lógica modal para forzar (por Hamkins et al). Tiene algo similar ha hecho que muestra las equivalencias entre la lógica temporal y obligando? Sería muy interesante para mí, ya forzando a veces es explicado de una manera que parece implicar el paso del tiempo (es decir, un "antes" el uso de un filtro genérico y "después").
Respuestas
¿Demasiados anuncios?La lógica Temporal es sólo un sabor particular de la lógica modal, por lo que los mismos modelos S4 (árboles, realmente; finito de los árboles en el proposicional caso) que dan naturales ", obligando a la semántica" para intuitionistic la lógica puede ser entendida como la ramificación temporal S4 fluye con el adicional de la herencia de la condición, que dice que: lo que se ve obligado en cualquier instante t es obligado en todos los instantes t' > t.
Otra forma natural de pensar de los modelos es en epistémica lógica de términos, que a su vez, es sólo otro sabor de la lógica modal. Así que la lógica epistémica correspondiente a S4, agregar la herencia condición, y tienes epistémica obligando a los modelos para intuitionistic lógica.
Por supuesto, nada de esto es exacto, así que echa un vistazo CSLI Notas de la Conferencia #199, Ch. 20 para los detalles básicos.
Me acabo de dar cuenta de esta pregunta. Hay ciertas afinidades entre la lógica modal de la coerción y la lógica temporal, sobre todo cuando uno tiene al alza de la modalidad de expresar que algo es cierto en algunas forzando la extensión (como en el futuro), pero también la doble modalidad de para cuando algo es cierto en algunas modelo de terreno (como el pasado). En un trabajo conjunto, Benedikt Loewe y he estudiado esta mezcla de lógica modal de forzar en nuestro papel
- J. D. Hamkins, B. Loewe, se Mueve arriba y abajo en el genérico multiverso Lógica y sus aplicaciones, ICLA 2013 LNCS, vol. 7750, pp 139-147, 2013.
Es fácil ver (véase la nota de pie de página $7$ en nuestro papel) para la mezcla de lógica modal de obligar a que cualquier declaración de $p$ implica que el $p$ es necesariamente hacia arriba hacia abajo posible. Este es también un hecho básico en la mayoría de los temporales lógicas, afirmando que $p$ implica que a partir de ahora en el futuro, $p$ fue cierto en algún momento en el pasado. Del mismo modo, es fácil probar para forzar a ese $p$ implica que en todos los modelos, $p$ es forceable. Y en la lógica temporal, si $p$ es cierto, entonces en cada punto en el pasado, es posible que $p$ mantiene en el futuro.