Curso completo de Lógica Epistémica S5
La lógica epistémica permite formalizar qué sabe un agente y qué considera posible. En S5, el conocimiento es idealizado: verdadero, introspectivo y estructuralmente estable.
Por qué importa
Es clave para razonar sobre información, observación, agentes, juegos epistémicos y estados de conocimiento compartido.
Objetivos de aprendizaje
- Distinguir verdad, conocimiento y creencia/posibilidad epistémica.
- Comprender T, 4 y B.
- Leer S5 como marco idealizado.
- Practicar derivaciones sobre conocimiento cerrado.
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
- S5 ya documenta su relación de equivalencia y las simplificaciones pedagógicas de modalidades iteradas.
- El motor reconoce patrones de omnisciencia lógica, Moore e introspección negativa.
- Los modelos abiertos muestran con claridad cómo puede ser satisfacible P ∧ ¬K(P).
S5 con paradojas y accesibilidad
Combina un caso satisfacible tipo Moore con una explicación de introspección negativa.
logic epistemic.s5
set verbose = on
check satisfiable (P & ![]P)
explain (![]P -> [](![]P))Cobertura exacta del perfil
S5 cubre K/T/4/5/B, dualidades K/B, colapso de modalidades iteradas, Kripke de equivalencia y paradojas epistémicas como Moore y la omnisciencia lógica.
Cobertura axiomática y colapsos
El runtime documenta el marco S5 como equivalencia y explota ese hecho para simplificar fórmulas iteradas.
logic epistemic.s5
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 equivalent []P, !<>!P
check equivalent <>P, ![]!PParadojas y modelos abiertos
El perfil no se limita al cuadro axiomático: también ilustra fenómenos epistémicos no triviales.
logic epistemic.s5
set verbose = on
check satisfiable (P & ![]P)
check satisfiable ([]P & ![]Q)
check satisfiable (<>P & <>!P)
explain (![]P -> [](![]P))
explain (P & ![]P)
countermodel (<>P -> P)
countermodel ([]P -> []Q)Aquí quedan referenciados Moore, la introspección negativa y el comportamiento de modelos donde `P` es verdad sin ser sabido.
Conceptos fundamentales
1. Veridicidad
Si un agente sabe P, entonces P es verdadera. Esto es el axioma T.
2. Introspección positiva
Si el agente sabe P, sabe que sabe P. Ese es el axioma 4.
3. Introspección negativa
Si no sabe P, sabe que no sabe P. ST la refleja con la forma B implementada.
4. Universalidad S5
Todos los mundos son epistémicamente accesibles entre sí dentro del marco idealizado del sistema.
Operadores y formas expresivas
[](P)Conocimiento
P es conocido por el agente.
logic epistemic.s5
check valid [](P) -> P<>(P)Posibilidad epistémica
P es compatible con lo que el agente considera posible.
logic epistemic.s5
check satisfiable <>(P) & Comandos que debes dominar
Conocimiento verdadero
Comprueba el axioma T.
logic epistemic.s5
check valid [](P) -> PIntrospección positiva
El agente sabe que sabe.
logic epistemic.s5
check valid [](P) -> []([](P))Cierre epistémico
Si sabe una implicación y sabe el antecedente, sabe el consecuente.
logic epistemic.s5
axiom r1 : [](P -> Q)
axiom r2 = [](P)
derive [](Q) from {r1, r2}ST 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.
Mapa de conocimiento con alias descriptivos
Ayuda a enseñar la diferencia entre verdad, conocimiento y posibilidad epistémica con nombres semánticos visibles.
logic epistemic.s5
let verdad = "Si se sabe P, entonces P" : ([]P -> P)
let introspeccion = "Si se sabe P, se sabe que se sabe P" : ([]P -> []([]P))
fn revisarConocimiento(F) {
explain F
return F
}
revisarConocimiento(verdad)
revisarConocimiento(introspeccion)
if valid ([]P -> P) {
print "S5 mantiene veridicidad"
}Enseñar ignorancia sin colapso
Subraya que no saber algo no es lo mismo que saber su negación.
logic epistemic.s5
let ignorancia = "P es posible sin estar sabido" : (<>P & ![]P)
explain ignorancia
check satisfiable <>P & ![]P
if valid !([]P) -> [](!([]P)) {
print "la introspección negativa idealizada está disponible"
}Lecciones prácticas largas
Teoremas básicos de S5
Tríada mínima para empezar.
logic epistemic.s5
check valid [](P) -> P
check valid [](P) -> []([](P))
check valid !([](P)) -> [](!([](P)))Compatibilidad con ignorancia
Es posible que algo sea compatible sin estar sabido.
logic epistemic.s5
check satisfiable <>(P) & Errores frecuentes al estudiar esta lógica
- Leer S5 como psicología humana real.
- Confundir posibilidad epistémica con posibilidad física.
- Pensar que ignorar P equivale a conocer !P.
Límites del motor y advertencias
- Frame universal puede crecer rápido.
- Modelo idealizado: no representa límites cognitivos ni errores humanos finos.
Cómo conecta con otras lógicas
- Nace de la modal.
- Se conecta con agentes, coordinación y teoría de juegos.