Curso completo de Lógica Paraconsistente Belnap
Belnap-Dunn amplía la semántica clásica con cuatro valores: verdadero, falso, ambos y ninguno. Esto permite trabajar con información inconsistente o incompleta sin hacer explotar el sistema.
Por qué importa
Es especialmente útil para modelar bases de conocimiento ruidosas, fuentes conflictivas o sistemas donde no quieres que una contradicción vuelva trivial toda la teoría.
Objetivos de aprendizaje
- Entender T, F, B y N.
- Comprender por qué ex falso falla.
- Ver por qué P -> P puede dejar de ser válida.
- Aprender a leer contramodelos de 4 valores.
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
- explain dibuja el retículo A4 y marca los valores designados T y B.
- La salida compara explícitamente qué leyes clásicas fallan y cuáles sí sobreviven en Belnap.
- La doc ahora deja claro que P ∧ ¬P puede ser satisfacible sin que todo colapse.
Retículo y no explosión
La explicación de una contradicción controlada deja ver el corazón pedagógico de Belnap.
logic paraconsistent.belnap
set verbose = on
explain (P & !P)
check valid ((P & !P) -> Q)Cobertura exacta del perfil
Belnap cubre los cuatro valores T/F/B/N, designación T/B, retículo A4, comparación con clásica y un conjunto concreto de leyes que sobreviven o caen.
Semántica y designación reales
La documentación ahora referencia explícitamente qué significa cada valor y por qué no hay explosión.
- `T`: solo verdadero
- `F`: solo falso
- `B`: both, verdadero y falso a la vez
- `N`: none, ni verdadero ni falso
- Valores designados: `T` y `B`
Leyes que fallan y leyes que sobreviven
El propio `explain()` del perfil enumera estas diferencias; aquí quedan documentadas y ejecutables.
logic paraconsistent.belnap
set verbose = on
check satisfiable (P & !P)
check valid ((P & !P) -> Q)
check valid (P | !P)
check valid (P -> P)
check valid ((P & Q) -> P)
check equivalent (P -> Q), (!P | Q)
check equivalent !(P & Q), (!P | !Q)
check equivalent !(P | Q), (!P & !Q)
check equivalent !!P, P
explain (P & !P)
explain (P -> P)
countermodel (P | !P)
countermodel ((P & !P) -> Q)Con eso se cubren explícitamente explosión, LEM, identidad, De Morgan y doble negación en Belnap.
Conceptos fundamentales
1. Cuatro valores
T verdadero, F falso, B ambos, N ninguno. Los valores designados son T y B.
2. Paraconsistencia
Una contradicción no obliga a que cualquier fórmula sea válida.
3. Fallo del tercero excluido
Si P vale N, entonces P | !P también puede valer N y no quedar designada.
4. Implicación material no clásica
Como la implicación se define desde !P | Q, hereda fenómenos no clásicos cuando interviene N.
Operadores y formas expresivas
P & !PContradicción tolerada
Puede ser satisfacible cuando P toma valor B.
logic paraconsistent.belnap
check satisfiable P & !PP | !PTercero excluido fallido
Ya no siempre resulta designado.
logic paraconsistent.belnap
check valid P | !PP -> PReflexividad material fallida
Puede fallar si P toma N.
logic paraconsistent.belnap
check valid P -> PComandos que debes dominar
Contradicción satisfacible
Experimenta con P y no-P simultáneamente.
logic paraconsistent.belnap
check satisfiable P & !PEx falso quodlibet
Observa cómo deja de ser una ley válida.
logic paraconsistent.belnap
check valid (P & !P) -> Q
countermodel (P & !P) -> QEquivalencias que sí se conservan
Algunas leyes de reescritura siguen funcionando.
logic paraconsistent.belnap
check equivalent P -> Q, !P | Q
check equivalent !(P & Q), !P | !QST 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.
Contradicción sin explosión, explicada
Perfecta para clase: un alias nombra la inconsistencia y el if muestra por qué Belnap no colapsa en trivialidad.
logic paraconsistent.belnap
let choque = "Hay evidencia a favor y en contra" : (P & !P)
fn revisarChoque(F) {
explain F
return F
}
revisarChoque(choque)
if valid ((P & !P) -> Q) {
print "habría explosión clásica"
} else {
print "Belnap tolera la inconsistencia sin trivializar"
}
check satisfiable P & !PComparador con intuición clásica
Sirve para mostrar que varias fórmulas que parecen obvias dejan de ser válidas cuando aparece el valor N.
logic paraconsistent.belnap
for Caso in { P -> P, P | !P, (P & !P) -> Q } {
explain Caso
}
if valid P -> P {
print "la reflexividad material sobrevivió"
} else {
print "en Belnap incluso eso puede fallar"
}Lecciones prácticas largas
Tres sorpresas de Belnap
Lo que más desconcierta a quien viene de la clásica.
logic paraconsistent.belnap
check valid P -> P
check valid P | !P
check valid (P & !P) -> QLo que sí se puede hacer
Equivalencias y satisfacibilidad útiles.
logic paraconsistent.belnap
check satisfiable P & !P
check equivalent P -> Q, !P | Q
check equivalent !(P | Q), !P & !QErrores frecuentes al estudiar esta lógica
- Esperar automáticamente todas las leyes clásicas.
- Confundir valor designado con valor estrictamente verdadero.
- Pensar que una contradicción destruye todo el sistema.
Límites del motor y advertencias
- El espacio crece como 4^n.
- Hay fórmulas clásicamente obvias que dejan de ser válidas.
Cómo conecta con otras lógicas
- Excelente contraste con la clásica.
- Prepara discusión sobre inconsistencia controlada y razonamiento robusto.