Es posible representar enunciados simples que involucran posibilidad y necesidad en la lógica modal alética y la semántica del mundo posible. Pero considere una afirmación como "Es posible que le resulte imposible ir a Walmart sin cruzar la interestatal". Si tradujeras ciegamente esa declaración a una lógica modal alética, sería equivalente a "es imposible que vayas a Walmart sin cruzar la interestatal", lo que obviamente es muy diferente del significado real de la declaración.
El problema es que las dos instancias de la palabra "posible" corresponden a diferentes conjuntos de mundos posibles. La declaración se traduciría a la semántica del mundo posible como "Existe un mundo posible x, que tiene un montón de diferentes submundos posibles que comparten la misma configuración de carreteras, y existe uno de esos submundos en el que vas a Walmart y no cruzas el Interestatal."
Entonces mi pregunta es, ¿hay algún sistema de lógica modal que permita modalidades aléticas anidadas como esta? ¿Y existe una versión de la semántica del mundo posible que haga que tales declaraciones sean significativas? Lo que imagino es que tienes un montón de mundos posibles que difieren no solo en qué proposiciones simples (sin modalidad) son verdaderas y falsas, sino que también difieren en qué mundos posibles existen o no. La semántica del mundo imposible puede ser relevante aquí.
Idealmente, querría un sistema que pueda representar no solo dos modalidades aléticas anidadas en una declaración, sino números arbitrarios de modalidades aléticas anidadas. Por ejemplo, declaraciones como "Hay un mundo posible donde no hay mundos posibles que satisfagan la propiedad de que existe un mundo posible tal que..."
En la lógica modal S4, las modalidades anidadas del mismo tipo colapsan, por lo que □□A ↔ □A y ◇◇A ↔ ◇A. En la lógica modal S5, todas las modalidades anidadas colapsan hacia la más a la derecha, por lo que □◇A ↔ ◇A y ◇□A ↔ □A. Si quiere poder decir que es posible que algo sea imposible, es decir, ◇□ ¬A, sin que esto se colapse en □¬A, necesita usar una lógica modal más débil que S5.
sofie selnes