Curso completo de Lógica Modal K
Modal K es la entrada al razonamiento sobre necesidad y posibilidad. Conserva los conectivos clásicos, pero añade una capa semántica nueva: los mundos posibles y la relación de accesibilidad entre ellos.
Por qué importa
Muchísimas lógicas especializadas —deóntica, epistémica, temporal— nacen de ideas modales. Si entiendes bien K, entiendes el lenguaje estructural del resto de familias.
Objetivos de aprendizaje
- Entender □ y ◇.
- Distinguir verdad actual de verdad necesaria.
- Comprender por qué K no fuerza reflexividad.
- Leer contramodelos en términos de mundos.
Accesos rápidos
Panorama del curso
Esta guía reúne la cobertura completa del perfil: conceptos, operadores, comandos, ejemplos largos, límites reales del motor y un script integral descargable para seguir probando fuera de la página. Los bloques de código se pueden ejecutar inline y abrir en el editor desplegable para probar variaciones sin salir de la documentación.
Capacidades nuevas de este perfil
- El perfil identifica axiomas modales reconocibles cuando una validez coincide con K, T, D, 4, 5 o B.
- La explicación del sistema deja visibles las propiedades del frame que sí o no están presentes.
- Los contramodelos muestran mundos, accesibilidad y valuación Kripke.
Axiomas y contramodelos en K
Muestra distribución modal válida y luego un caso que falla por falta de reflexividad.
logic modal.k
set verbose = on
check valid ([](P -> Q) -> ([]P -> []Q))
countermodel ([]P -> P)Cobertura exacta del perfil
Modal K cubre necesidad, posibilidad, dualidad, cuadros Kripke y reconocimiento de esquemas K/T/D/4/5/B cuando la fórmula coincide o falla por propiedades del frame.
Operadores y propiedades del frame
K trabaja con la relación de accesibilidad sin restricciones y usa esa falta de restricciones como contenido pedagógico explícito.
- `[]` / `□` para necesidad
- `<>` / `◇` para posibilidad
- Dualidades `[]P ≡ !<>!P` y `<>P ≡ ![]!P`
- El sistema explica por qué no valen reflexividad, serialidad, transitividad, simetría ni euclidianidad
Axiomas y contraejemplos reales de K
Esta batería deja ver lo que el sistema sí y no valida con el frame mínimo.
logic modal.k
set verbose = on
check valid ([](P -> Q) -> ([]P -> []Q))
check valid []P -> P
check valid []P -> <>P
check valid []P -> [][]P
check valid P -> []<>P
check valid <>P -> []<>P
check equivalent []P, !<>!P
check equivalent <>P, ![]!P
countermodel ([]P -> P)
countermodel (<>P -> []<>P)Conceptos fundamentales
1. Mundo actual y mundos posibles
Una fórmula modal no depende solo del estado actual; depende de qué mundos están accesibles desde él.
2. Necesidad y posibilidad
[]P significa que P vale en todos los mundos accesibles. <>P significa que P vale en al menos uno.
3. K como sistema mínimo
K valida la distribución de la necesidad sobre la implicación, pero no asume que todo mundo se accede a sí mismo.
4. Tableaux etiquetados
ST usa labeled tableau: razona sobre fórmulas y sobre el mundo donde deben cumplirse.
Operadores y formas expresivas
[]PNecesidad
P vale en todos los mundos accesibles.
logic modal.k
check valid [](P -> Q) -> ([]P -> []Q)<>PPosibilidad
P vale en al menos un mundo accesible.
logic modal.k
check equivalent <>(P), Comandos que debes dominar
Axioma K
Practica la ley central del sistema.
logic modal.k
check valid [](P -> Q) -> ([]P -> []Q)Dualidad modal
Comprueba la equivalencia entre posibilidad y negación de necesidad.
logic modal.k
check equivalent <>(P), Contramodelos modales
Ve por qué una fórmula falla en un frame no reflexivo.
logic modal.k
check valid []P -> P
countermodel <>P -> []PST como herramienta pedagógica en esta lógica
Esta sección no solo enseña la lógica, sino también cómo usar `ST` para explicarla mejor: con aliases semánticos, funciones reutilizables, condicionales, recorridos guiados y salidas legibles para clase, taller o autoestudio.
Axioma K explicado como clase interactiva
Usa una variable descriptiva, una función de revisión y un condicional para fijar la intuición de necesidad distribuida.
logic modal.k
let axiomaK = "Si necesariamente P implica Q, entonces si necesariamente P, necesariamente Q" : ([](P -> Q) -> ([]P -> []Q))
fn revisarTesis(F) {
explain F
return F
}
revisarTesis(axiomaK)
if valid ([](P -> Q) -> ([]P -> []Q)) {
print "la distribución modal se sostiene en K"
} else {
print "hay que revisar la accesibilidad"
}Comparador de intuiciones modales
Contrasta una ley válida de K con una ley que no pertenece al sistema, para enseñar por contraste.
logic modal.k
let valida = "Distribución necesaria" : ([](P -> Q) -> ([]P -> []Q))
let noValida = "Reflexividad" : ([]P -> P)
explain valida
explain noValida
if valid ([]P -> P) {
print "esto sería T o un sistema más fuerte"
} else {
print "K no garantiza reflexividad"
}Lecciones prácticas largas
Distribución necesaria
La ley característica de K.
logic modal.k
check valid [](P -> Q) -> ([]P -> []Q)Reflexividad ausente
Muestra por qué []P -> P no es teorema de K.
logic modal.k
check valid []P -> P
countermodel []P -> PPosibilidad compatible múltiple
Dos posibilidades distintas pueden coexistir.
logic modal.k
check satisfiable <>(P) & <>(Q)Errores frecuentes al estudiar esta lógica
- Creer que necesario significa verdadero aquí mismo.
- Confundir K con T o S5.
- Olvidar que la relación de accesibilidad puede no ser reflexiva.
Límites del motor y advertencias
- Tableau modal limitado a 200 nodos.
- No hay garantías de reflexividad, simetría ni transitividad.
Cómo conecta con otras lógicas
- La deóntica y la epistémica reinterpretan [] y <>.
- Temporal LTL conserva intuiciones modales pero con lectura temporal.