Curso completo de Lógica Proposicional

Perfil activo: classical.propositional

CPCclassical.propositionalGuía dedicada

Curso completo de Lógica Proposicional

La lógica proposicional clásica es el punto de partida para comprender todo ST. Aquí aprendemos a tratar enunciados completos como unidades de verdad, a combinarlos con conectivos y a verificar si un razonamiento es válido, satisfacible o equivalente.

Por qué importa

Sin dominar la proposicional, el resto de lógicas se vuelve opaco. La modal reutiliza la implicación y la negación. La deóntica y la epistémica heredan la lectura estructural de las fórmulas. La intuicionista discute precisamente qué partes de la clásica se mantienen y cuáles no.

Objetivos de aprendizaje

  • Reconocer qué es y qué no es una proposición dentro de ST.
  • Dominar el significado exacto de !, &, |, -> y <->.
  • Distinguir entre validez, satisfacibilidad, contradicción y contingencia.
  • Usar derive, truth_table, check valid, check satisfiable, check equivalent y countermodel con soltura.
  • Introducir aliases con let para volver más legible una teoría ejecutable.
  • Usar analyze y explain para convertir ejercicios lógicos en clases paso a paso.
  • Leer y construir demostraciones basadas en Modus Ponens, Modus Tollens y reglas estructurales.
  • Entender las equivalencias fundamentales que permiten reescribir fórmulas sin cambiar su valor lógico.

Accesos rápidos

Volver al índice STDescargar script completo Repositorio ST

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

  • La proposicional ahora clasifica fórmulas automáticamente y reconoce leyes conocidas cuando haces check valid o explain.
  • derive nombra el patrón de razonamiento, muestra el esquema formal y puede exportar la prueba en LaTeX con set output = latex.
  • explain despliega sub-fórmulas, NNF, CNF, DNF, cláusulas de resolución y completitud funcional.
  • analyze ya no se queda en dos o tres errores: el runtime activo detecta diez falacias formales en argumentos proposicionales.

Salida pedagógica completa en proposicional

Combina verbosidad, comparación entre sistemas, falacias y explicación estructural de una fórmula.

stejecutable
logic classical.propositional
set verbose = on
check valid (P -> (Q -> P))
analyze {P -> Q, Q} -> P
explain (P -> Q)

Cobertura exacta del perfil

El perfil proposicional es el más amplio del runtime: conecta operadores clásicos y extendidos, 27 esquemas clasificados automáticamente, 25 reglas derivativas nombradas y 10 detectores de falacia realmente implementados.

Operadores y aliases soportados

La sintaxis proposicional no se queda en los cinco conectivos clásicos. El parser y el runtime también aceptan operadores funcionalmente completos y sus aliases textuales o Unicode.

  • `!`, `&`, `|`, `->`, `<->`
  • `^`, `xor`, `⊕` para XOR
  • `!&`, `nand`, `↑` para NAND
  • `!|`, `nor`, `↓` para NOR
  • `formulaToUnicode()` y `formulaToLaTeX()` renderizan todos esos conectivos

Las 27 leyes que el clasificador reconoce hoy

Estas son las fórmulas base que el runtime etiqueta por nombre cuando coinciden por unificación estructural.

stejecutable
logic classical.propositional
check valid (P -> P)
check valid (P | !P)
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 -> !Q) -> (Q -> P))
check valid (!!P -> P)
check valid (P -> !!P)
check valid (((P -> Q) -> P) -> P)
check valid (!P -> (P -> Q))
check valid (((P -> Q) & (Q -> R)) -> (P -> R))
check valid ((P | Q) -> (Q | P))
check valid ((P & Q) -> (Q & P))
check valid (!(P & Q) <-> (!P | !Q))
check valid (!(P | Q) <-> (!P & !Q))
check valid ((P & (Q | R)) <-> ((P & Q) | (P & R)))
check valid ((P | (Q & R)) <-> ((P | Q) & (P | R)))
check valid ((P -> Q) <-> (!P | Q))
check valid ((P <-> Q) <-> ((P -> Q) & (Q -> P)))
check valid ((P & (P | Q)) <-> P)
check valid ((P | (P & Q)) <-> P)
check valid ((P & P) <-> P)
check valid ((P | P) <-> P)
check valid (((P & Q) -> R) <-> (P -> (Q -> R)))
check valid ((P <-> Q) <-> (Q <-> P))
check valid (!!P <-> P)

Aquí están las 27 fórmulas realmente presentes en `formula-classifier.ts`, no una versión resumida.

Las 25 reglas de derivación activas

El derivador BFS del perfil clásico nombra estas reglas cuando logra construir la meta o un paso intermedio relevante.

  • Modus Ponens
  • Modus Tollens
  • Introducción de conjunción
  • Eliminación de conjunción
  • Introducción de disyunción
  • Silogismo hipotético
  • Silogismo disyuntivo
  • Introducción de bicondicional
  • Eliminación de bicondicional
  • Dilema constructivo
  • Dilema destructivo
  • Dilema simple
  • Resolución
  • Explosión
  • Doble negación
  • Introducción de doble negación
  • Introducción de implicación
  • Contraposición
  • Absorción
  • Exportación
  • Importación
  • De Morgan (AND)
  • De Morgan (OR)
  • Reducción al absurdo (RAA)
  • Prueba condicional

Falacias realmente implementadas

El changelog menciona once, pero el runtime activo registra diez detectores explícitos en `fallacies.ts`. La doc queda alineada con el código real.

  • Afirmación del consecuente
  • Negación del antecedente
  • Medio no distribuido
  • Falacia de composición
  • Posible falso dilema
  • Petición de principio (Petitio Principii)
  • Conversión ilícita
  • Generalización apresurada
  • Falacia de cuatro términos (Quaternio terminorum)
  • Falacia de división
stejecutable
logic classical.propositional
analyze {P -> Q, Q} -> P
analyze {P -> Q, !P} -> !Q
analyze {P -> P} -> (P -> P)

La “falacia del consecuente” del changelog queda absorbida por la afirmación del consecuente en la implementación actual.

Conceptos fundamentales

1. Proposición, átomo y fórmula

Una proposición es un enunciado declarativo que puede ser verdadero o falso. En ST esto se representa con átomos como P, Q, R o nombres más expresivos como Humo, Fuego o Aprueba. Una fórmula es cualquier expresión construida a partir de esos átomos usando conectivos. Ejemplos: P, !P, P & Q, (P -> Q) & P.

2. Bivalencia clásica

El perfil classical.propositional solo admite dos valores: verdadero y falso. No hay un tercer estado. El motor explora todas las valuaciones posibles de los átomos para decidir si una fórmula siempre vale, a veces vale o nunca vale. Por eso las tablas de verdad son la semántica central de este curso.

3. Validez, satisfacibilidad y contingencia

Una fórmula es válida si es verdadera en toda valuación. Es satisfacible si existe al menos una valuación donde sale verdadera. Es contradictoria si no hay ninguna valuación que la haga verdadera. Es contingente si es satisfacible pero no válida. Esta distinción es clave porque muchos estudiantes confunden “posible” con “siempre verdadero”.

4. Forma lógica frente a contenido

En ST no importa si P significa “llueve” o “2+2=4”; importa cómo se relaciona con otras fórmulas. La lógica proposicional abstrae el contenido material y se concentra en la arquitectura del razonamiento: si P y P -> Q, entonces Q. Esa estructura permanece sin importar el tema.

5. Semántica del motor de ST

El motor proposicional de ST combina una tabla de verdad exhaustiva con un derivador BFS. Primero puede intentar probar metas mediante reglas sintácticas; si no logra cerrar la derivación, puede comprobar semánticamente si toda valuación que satisface las premisas también satisface la meta. Así se enseña a la vez prueba e interpretación.

6. Reescritura lógica

Dos fórmulas pueden verse distintas y significar exactamente lo mismo. Por ejemplo, P -> Q equivale a !P | Q. Esta idea permite normalizar expresiones, encontrar versiones más intuitivas y detectar si dos razonamientos son realmente el mismo bajo otra forma.

Operadores y formas expresivas

!P

Negación

Invierte el valor de verdad. Si P es verdadera, !P es falsa; si P es falsa, !P es verdadera.

Práctica ST
stejecutable
logic classical.propositional
check valid !(P & !P)
check equivalent !!P, P
truth_table !P
P & Q

Conjunción

Es verdadera solo cuando ambas partes son verdaderas. Modela el “y” inclusivo.

Práctica ST
stejecutable
logic classical.propositional
check satisfiable P & Q
check satisfiable P & !P
truth_table P & Q
P | Q

Disyunción

Es verdadera cuando al menos una parte es verdadera. Solo falla si ambas son falsas.

Práctica ST
stejecutable
logic classical.propositional
check valid P | !P
derive P | Q from {base}
truth_table P | Q
P -> Q

Implicación material

Solo es falsa cuando P es verdadera y Q es falsa. En todos los demás casos es verdadera.

Práctica ST
stejecutable
logic classical.propositional
check equivalent P -> Q, !P | Q
check valid P -> Q
countermodel P -> Q
P <-> Q

Bicondicional

Es verdadera cuando ambos lados tienen el mismo valor de verdad. Equivale a (P -> Q) & (Q -> P).

Práctica ST
stejecutable
logic classical.propositional
check equivalent P <-> Q, (P -> Q) & (Q -> P)
check valid P <-> P
truth_table P <-> Q

Comandos que debes dominar

Validez

Usa check valid para preguntar si una fórmula es tautológica.

stejecutable
logic classical.propositional
check valid P | !P
check valid (P & (P -> Q)) -> Q

Satisfacibilidad

Usa check satisfiable para saber si existe al menos una valuación donde la fórmula sale verdadera.

stejecutable
logic classical.propositional
check satisfiable P & Q
check satisfiable P & !P

Equivalencia

Usa check equivalent para confirmar que dos formas distintas expresan la misma condición lógica.

stejecutable
logic classical.propositional
check equivalent P -> Q, !P | Q
check equivalent !(P & Q), !P | !Q

Derivación

Usa derive para obtener una conclusión a partir de premisas registradas como axiomas.

stejecutable
logic classical.propositional
axiom regla : P -> Q
axiom base = P
derive Q from {regla, base}

Tabla de verdad

Usa truth_table para ver el comportamiento exacto de una fórmula en todas las valuaciones.

stejecutable
logic classical.propositional
truth_table P -> Q
truth_table (P & (P -> Q)) -> Q

Contramodelo

Usa countermodel cuando una fórmula no es válida y quieres ver por qué falla.

stejecutable
logic classical.propositional
countermodel P -> Q
countermodel P <-> Q

Variables lógicas con let

Usa let para nombrar reglas, hechos y descripciones, y luego reutilizarlos en derivaciones y verificaciones.

stejecutable
logic classical.propositional
let regla = "Si estudio, apruebo" : (E -> A)
let hecho = "Estudio hoy" : E
derive A from {regla, hecho}
print regla

Analizar y explicar inferencias

Usa analyze para evaluar una inferencia completa y explain para desplegar lectura pedagógica de una fórmula.

stejecutable
logic classical.propositional
analyze {E, E -> A} -> A
explain (E -> A)

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.

Clase guiada con variables y función explicativa

Convierte un argumento simple en una mini lección ejecutable donde cada paso tiene nombre, explicación y cierre condicional.

stejecutable
logic classical.propositional
let regla = "Si leo a Frege, entiendo la inferencia" : (L -> I)
let hecho = "Hoy leo a Frege" : L

fn revisarPaso(F) {
  explain F
  return F
}

revisarPaso(regla)
derive I from {regla, hecho}

if valid ((L & (L -> I)) -> I) {
  print "modus ponens comprendido"
} else {
  print "conviene revisar la forma del argumento"
}

Formalización filosófica mínima reutilizable

Usa aliases descriptivos para que el estudiante vea al mismo tiempo el lenguaje natural y su forma lógica.

stejecutable
logic classical.propositional
let P = "Pienso"
let E = "Existo"
let cogito = "Si pienso, existo" : (P -> E)

fn mostrarInferencia(F) {
  explain F
  return F
}

mostrarInferencia(cogito)
analyze {P, P -> E} -> E
if valid ((P & (P -> E)) -> E) {
  print "la estructura inferencial es estable"
}

Lecciones prácticas largas

Ejemplo 1 · Razonamiento encadenado

Encadena dos implicaciones con un hecho inicial. Es la mejor puerta de entrada para entender Modus Ponens aplicado varias veces.

stejecutable
logic classical.propositional
axiom r1 : Estudia -> Aprueba
axiom r2 : Aprueba -> Celebra
axiom hecho = Estudia
derive Aprueba from {r1, hecho}
derive Celebra from {r1, r2, hecho}

Ejemplo 2 · Tautología y contingencia

Contrasta una verdad lógica universal con una fórmula que solo vale a veces.

stejecutable
logic classical.propositional
check valid P | !P
check valid P -> Q
check satisfiable P -> Q
countermodel P -> Q

Ejemplo 3 · Equivalencias fundamentales

Practica tres equivalencias que aparecen una y otra vez en lógica, programación y especificación.

stejecutable
logic classical.propositional
check equivalent P -> Q, !P | Q
check equivalent !(P & Q), !P | !Q
check equivalent P <-> Q, (P -> Q) & (Q -> P)

Ejemplo 4 · Reglas que implementa el motor

Este bloque toca varias reglas del derivador de ST: introducción y eliminación de conjunción, doble negación y bicondicional.

stejecutable
logic classical.propositional
axiom both : P & Q
derive P from {both}
derive Q from {both}

axiom dbl : !!R
derive R from {dbl}

axiom iff : P <-> Q
axiom have = P
derive Q from {iff, have}

Ejemplo 5 · Mini teoría completa

Un guion más largo que combina teoría, validez, equivalencia, tabla de verdad y contramodelo en un mismo flujo.

stejecutable
logic classical.propositional
axiom regla1 : Humo -> Fuego
axiom regla2 : Fuego -> Evacuar
axiom hecho = Humo

derive Fuego from {regla1, hecho}
derive Evacuar from {regla1, regla2, hecho}

check valid (Humo & (Humo -> Fuego) & (Fuego -> Evacuar)) -> Evacuar
check equivalent Humo -> Fuego, !Humo | Fuego
truth_table (Humo & (Humo -> Fuego)) -> Fuego
countermodel Humo -> Evacuar

Ejemplo 6 · Clase guiada con ST moderno

Combina aliases, análisis, explicación y control condicional ligero para convertir una inferencia en material pedagógico ejecutable.

stejecutable
logic classical.propositional

let regla = "Si estudio, apruebo" : (E -> A)
let hecho = "Estudio hoy" : E

derive A from {regla, hecho}
analyze {E, E -> A} -> A
explain (E -> A)

if valid (P | !P) {
  print "tautología detectada"
} else {
  print "esto no debería ocurrir"
}

Errores frecuentes al estudiar esta lógica

  • Creer que P -> Q significa relación causal fuerte. En clásica es un conectivo veritativo, no una teoría de causa.
  • Confundir “satisfacible” con “válida”. Una contingencia puede ser satisfacible y sin embargo fallar en muchas valuaciones.
  • Olvidar que la única fila falsa de P -> Q es P=V y Q=F.
  • Pensar que countermodel muestra un error del motor, cuando en realidad muestra exactamente por qué la fórmula no es tautológica.
  • No distinguir entre tener una equivalencia semántica y tener una derivación explícita en una teoría dada.
  • Suponer que una contradicción nunca puede aparecer en premisas; en clásica puede aparecer, pero trivializa si se combina con principios fuertes como explosión.

Límites del motor y advertencias

  • truth_table admite hasta 20 variables proposicionales.
  • El derivador BFS usa un límite de 100 iteraciones y una guardia de 500 fórmulas conocidas.
  • La semántica es completamente clásica: no hay tercer valor, ni inconsistencia tolerada, ni persistencia intuicionista.
  • Si quieres cuantificadores, necesitas pasar a classical.first_order.

Cómo conecta con otras lógicas

  • Desde aquí pasas a Primer Orden para introducir individuos y cuantificadores.
  • También pasas a Modal K para conservar conectivos clásicos y sumar mundos posibles.
  • La Intuicionista te enseña qué principios clásicos dejan de estar disponibles.
  • Belnap muestra qué pasa cuando abandonas la bivalencia.
  • La Probabilística reusa la clásica dentro de mundos, pero mide grados de probabilidad.