¿Por qué es $\square\square=\square$ $\Diamond\Diamond=\Diamond$ en el S5 lógica modal?

Question

Estoy leyendo acerca de la lógica modal en la Stanford Encyclopedia of Philosophy. Ellos definen la lógica modal S5 como lógica proposicional aumentada con los operadores modales $\square$ $\Diamond=\lnot\square\lnot$ y los axiomas

$$\begin{align} \square(A\to B)&\to(\square A\to\square B), \tag{K} \\ \square A&\to A, \tag{M} \\ \Diamond A&\to\square\Diamond A. \tag{5} \end{align}$$

Entonces el estado sin la prueba de que en el S5 cualquier cadena de operadores modales es el equivalente a la última operador en la cadena. Es decir, $00\cdots0\square=\square$ $00\cdots0\Diamond=\Diamond$ donde cada una de las $0$ es $\square$ o $\Diamond$.

Esta afirmación no es en absoluto obvio para mí, así que me gustaría tener una prueba. Supongo que solo tenemos que mostrar que $\Diamond\square=\square=\square\square$$\square\Diamond=\Diamond=\Diamond\Diamond$. La aplicación de $(\mathrm M)$ $\Diamond A$los rendimientos de la inversa de $(5)$, mostrando que el $\square\Diamond=\Diamond$; contrapositively, $\Diamond\square=\square$. Asimismo, la aplicación de $(\mathrm M)$ $\square A$muestra que $\square\square A\to\square A$$\Diamond A\to\Diamond\Diamond A$.

Sin embargo, no veo cómo establecer el conversar $\square A\to\square\square A$$\Diamond\Diamond A\to\Diamond A$. Ha sido un tiempo desde que hice la lógica. Ayuda?

Answer 1

Observación preliminar: el interdefinability de $\square$ $\Diamond$ el uso de la negación no es específico para S5.

Ahora a la pregunta. No sé de improviso cómo las derivaciones dentro del sistema, pero si usted quiere que su reclamo sea "obvio" creo que quiere una explicación que hace que sea intuitiva. Tal explicación puede ser dada en términos de la semántica de Kripke y constituye un punto de vista semántico basado en la prueba.

De manera informal...

Básicamente S5 supone un conjunto de mundos posibles donde cualquier mundo posible es accesible desde cualquier otro mundo posible. (Esto no es técnicamente muy correcto, pero lo suficientemente cerca.) A continuación, $\square A$ significa "En cualquier mundo posible, $A$ es verdadero," y $\Diamond A$ significa que "Hay un mundo posible donde $A$ es verdadero". Entonces, si tenemos que recorrer y escribir $\square \Diamond A$, estamos diciendo que, desde el punto de vista de cualquier mundo posible, un mundo donde la $A$ es cierto.

Pero, como cada mundo posible es accesible desde todas las de otro mundo posible, no hay ninguna diferencia entre decir eso y decir que, desde el punto de vista de este mundo, hay un mundo posible donde $A$ es cierto. Que es sólo $\Diamond A.$ por Lo que el adicional $\square$ operador no cambie la instrucción.

Una historia similar va para agregar el $\Diamond$ donde $\Diamond$ o $\square$ ya está presente.

En otras palabras, si queremos cambiar nuestro mundo de evaluación de la actual (este mundo) a otro, el conjunto de modal verdades "ve" no cambia, aunque el conjunto de los no-modal verdades de curso. Vemos exactamente la misma modal verdades, porque el carácter universal de la accesibilidad de la relación se asegura de que siempre estamos mirando el mismo conjunto de mundos posibles.

¿Eso ayuda?

EDIT: En respuesta a la OP de comentarios de abajo, aquí está la respuesta deseada (reunido después de la paginación a través de Hughes y Cresswell).

1. Desde que se acordó que $\Diamond \square = \square$,$\square A \rightarrow \Diamond \square A$.
2. Sustituto $\square A$ $A$ (5) para obtener el $\Diamond \square A \rightarrow \square \Diamond \square A$. Así que, a continuación, $\square A \rightarrow \square \Diamond \square A$
3. Reemplace $\Diamond \square A$ $\square A$ en el consiguiente para obtener el $\square A \rightarrow \square \square A$.
4. Y, a continuación, en sustitución de $A$ $\neg A$ y la realización de contraposición, de $\square A \rightarrow \square \square A$ obtenemos $\Diamond\Diamond A \rightarrow \Diamond A$.

Answer 2

Me gusta pruebas:

ps yo uso ligeramente diferente para los nombres de los axiomas, y nos ethe reglas

Modus ponens |-A | - - > B => |- B

y Necessitation |-A => |- []Un

K |-|- [](A -> B) -> ([]A -> []B) 
T |-|- []A -> A 
E |-|- <>A -> []<> A  

1 |- ~[]<>~A -> ~<>~A    contra positive of Axiom E, [A/~A]
2 |- <>[]A -> []A        1 modal exchange
3 |- ~~[]A -> ~[]~[]A    contra positive of Axiom T, [A/~[]A] 
4 |- []A -> <>[]A.       3 modal exchange
5 |- <>[]A ->[]<>[]A     Axiom E [A/[]A] 
6 |- []A -> []<>[]A      4,5 modus ponens       
7 |- [](<>[]A -> []A)    2 necessitation
8 |- []<>[]A -> [][]A    7 rule K
9 |- []A -> [][]A        7,8 modus ponens