Curso completo de Lógica Intuicionista
La lógica intuicionista conserva parte importante del razonamiento clásico, pero rechaza la idea de que toda fórmula deba ser verdadera o falsa sin una construcción efectiva.
Por qué importa
Es esencial para teoría de la demostración, fundamentos constructivos, programación funcional y semánticas de tipos.
Objetivos de aprendizaje
- Entender por qué falla P | !P.
- Comprender la no validez de !!P -> P.
- Leer contramodelos intuicionistas.
- Distinguir no demostrable de falso.
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 intuicionista ya venía fuerte y conserva forcing completo, lectura BHK y comparación IPC vs CPC.
- Los contramodelos Kripke muestran la persistencia intuicionista, no solo una fila falsa aislada.
- La documentación nueva aclara que aquí “no válido” no equivale a “refutado”.
Forcing y límites de la clásica
Se ve una ley constructiva que sí vale y dos principios clásicos que el perfil rechaza con contramodelo.
logic intuitionistic.propositional
check valid (P -> !!P)
countermodel (P | !P)
countermodel (!!P -> P)Cobertura exacta del perfil
IPC mantiene forcing Kripke, lectura BHK y contraste con clásica. También acepta los conectivos extendidos del parser, siempre bajo semántica intuicionista.
Conectivos y lectura constructiva
La sintaxis soportada incluye los conectivos clásicos y extendidos, pero la validez se decide con forcing intuicionista.
- `!`, `&`, `|`, `->`, `<->`
- `^`, `xor`, `⊕`
- `!&`, `nand`, `↑`
- `!|`, `nor`, `↓`
- La salida explica BHK, persistencia y diferencia entre no demostrable y falso
Fórmulas que distinguen IPC de CPC
Este bloque referencia de forma explícita las leyes válidas y las caídas clásicas más importantes.
logic intuitionistic.propositional
check valid (P -> P)
check valid (P -> (Q -> P))
check valid ((P -> (Q -> R)) -> ((P -> Q) -> (P -> R)))
check valid ((P -> Q) -> (!Q -> !P))
check valid ((P & !P) -> Q)
check valid (P -> !!P)
check valid !(P | Q) -> (!P & !Q)
check valid (P | !P)
check valid (!!P -> P)
check valid (((P -> Q) -> P) -> P)
check equivalent (P !& Q), !(P & Q)
check equivalent (P !| Q), !(P | Q)
countermodel (P | !P)
countermodel (!!P -> P)Las tres últimas fórmulas muestran el límite constructivo real: LEM, DNE y Peirce no salen válidas aquí.
Conceptos fundamentales
1. Verdad constructiva
Afirmar P no es solo asignarle V; es disponer de una construcción o prueba de P.
2. Persistencia de Kripke
Si algo es verdadero en un mundo intuicionista, sigue siéndolo en mundos futuros accesibles.
3. Tercero excluido
P | !P no es una ley general en IPC. Puede haber mundos donde aún no tengamos ni P ni una refutación de P.
4. Doble negación
Que sea imposible refutar P no basta para afirmar constructivamente P. Por eso !!P -> P falla.
Operadores y formas expresivas
!PNegación intuicionista
No hay forma de obtener P en ningún mundo accesible.
logic intuitionistic.propositional
check valid P -> !!PP -> QImplicación constructiva
Una transformación efectiva de pruebas de P en pruebas de Q.
logic intuitionistic.propositional
check valid (P -> Q) -> (P -> Q)Comandos que debes dominar
Validez constructiva
Compara principios aceptados y rechazados.
logic intuitionistic.propositional
check valid P -> !!P
check valid P | !P
check valid !!P -> PContramodelos
Observa por qué fallan ciertas leyes clásicas.
logic intuitionistic.propositional
countermodel P | !P
countermodel !!P -> PSatisfacibilidad
Que una ley no sea válida no significa que nunca pueda cumplirse.
logic intuitionistic.propositional
check satisfiable 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.
Clase por contraste con leyes clásicas
Usa variables descriptivas y condicionales para mostrar qué se conserva y qué se pierde al pasar a IPC.
logic intuitionistic.propositional
let conservada = "Toda prueba de P implica doble negación" : (P -> !!P)
let clasica = "Tercero excluido" : (P | !P)
fn revisarFormula(F) {
explain F
return F
}
revisarFormula(conservada)
revisarFormula(clasica)
if valid (P | !P) {
print "seguimos en clásica"
} else {
print "en intuicionista no todo enunciado está decidido"
}Pequeño guion constructivo
Ofrece un patrón para ejercicios donde el docente quiere separar no-refutabilidad de prueba efectiva.
logic intuitionistic.propositional
let pasoSeguro = "De P obtenemos !!P" : (P -> !!P)
let pasoFallido = "De !!P obtenemos P" : (!!P -> P)
explain pasoSeguro
explain pasoFallido
if valid (!!P -> P) {
print "esto ya sería lectura clásica"
} else {
print "ST mantiene la diferencia constructiva"
}Lecciones prácticas largas
Lo que sí se conserva
Ejemplos de fórmulas válidas intuicionistamente.
logic intuitionistic.propositional
check valid P -> !!P
check valid ((P -> Q) -> (!Q -> !P))
check valid (P & Q) -> PLo que no se conserva
Ejemplos clásicos que fallan en IPC.
logic intuitionistic.propositional
check valid P | !P
check valid !!P -> P
check valid ((!P -> !Q) -> (Q -> P))Errores frecuentes al estudiar esta lógica
- Pensar que una fórmula no válida queda refutada.
- Aplicar leyes clásicas sin mirar el perfil activo.
- Olvidar que la semántica usa mundos persistentes.
Límites del motor y advertencias
- Máximo 4 mundos Kripke.
- Con más átomos el motor reduce mundos para mantener tractabilidad.
Cómo conecta con otras lógicas
- Se entiende mucho mejor después de la proposicional clásica.
- Conecta con teoría de tipos, lambda cálculo y semántica de programación.