Agora | Elenxos

FOLclassical.first_orderGuía dedicada

Curso completo de Lógica de Primer Orden

La lógica de primer orden extiende la proposicional para hablar de objetos, propiedades y relaciones. Aquí ya no dices solo P o Q, sino Humano(socrates), Ama(ana, musica) o forall x (Humano(x) -> Mortal(x)).

Por qué importa

Con FOL puedes formalizar conocimiento real: bases de datos, ontologías, reglas generales y excepciones parciales. Es la lógica natural para pasar de “algo ocurre” a “todos los individuos de cierto tipo cumplen cierta propiedad”.

Objetivos de aprendizaje

Leer correctamente forall y exists.
Distinguir predicados, constantes y variables.
Practicar derivaciones por instanciación de universales.
Evitar confundir existencia con universalidad.
Comprender el límite semidecidible del motor.

Accesos rápidos

Volver al índice ST Descargar 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

explain ahora distingue variables libres y ligadas, aridad de predicados, alcance de cuantificadores y alternancia ∀∃.
El motor puede mostrar forma prenex y skolemización cuando la fórmula lo requiere.
derive ya documenta pasos UI, EI, EG y UG con justificación numerada.
Los contramodelos incluyen dominio e interpretación concreta de predicados.

FOL con traza más rica

Este bloque deja ver tanto la derivación cuantificada como la lectura estructural de la regla universal.

stejecutable

logic classical.first_order
set verbose = on
axiom regla = forall x (Humano(x) -> Mortal(x))
axiom caso = Humano(socrates)
derive Mortal(socrates) from {regla, caso}
explain forall x (Humano(x) -> Mortal(x))

Cobertura exacta del perfil

FOL cubre cuantificadores, dualidades, prenex, skolemización, pasos UI/EI/UG/EG, dominio e interpretación en contramodelos. La sintaxis de igualdad existe, pero su semántica todavía no está cerrada pedagógicamente en el runtime actual.

Sintaxis realmente soportada

Además de cuantificadores y predicados, el parser acepta igualdad y conectivos clásicos completos.

`forall x`, `exists x`
Predicados de aridad variable como `P(x)`, `R(x, y)`
Conectivos `!`, `&`, `|`, `->`, `<->` dentro de fórmulas cuantificadas
Sintaxis de igualdad `x = y` y render formal de `=`
La igualdad se parsea y se formatea, pero hoy no tiene un tratamiento semántico fiable en `check valid`

Familias de fórmulas cubiertas

Estos son los patrones que el perfil trabaja bien hoy: instanciación, generalización, dualidad cuantificacional y contramodelos de orden superior sencillo.

stejecutable

logic classical.first_order
check valid ((forall x P(x)) -> P(a))
check valid (P(a) -> exists x P(x))
check valid ((forall x (P(x) -> Q(x))) -> ((forall x P(x)) -> (forall x Q(x))))
check valid ((forall x (P(x) -> Q(x))) -> ((exists x P(x)) -> (exists x Q(x))))
check equivalent !(exists x !P(x)), forall x P(x)
check equivalent !(forall x P(x)), exists x !P(x)
check satisfiable (forall x exists y R(x, y))
explain forall x exists y Relacion(x, y)
countermodel ((exists x P(x)) -> forall x P(x))
countermodel ((forall x exists y R(x, y)) -> (exists y forall x R(x, y)))

Igualdad y estado real del motor

La igualdad está en el AST y en el render, pero no debe documentarse como teorema semánticamente resuelto.

stejecutable

logic classical.first_order
let igualdad = (x = y)
print igualdad
explain forall x (x = x)

La documentación ahora la presenta como soporte sintáctico con semántica parcial, porque `check valid forall x (x = x)` no sale válida en el runtime actual.

Conceptos fundamentales

1. Dominio e individuos

Toda fórmula FOL se interpreta sobre un dominio de objetos. Los nombres como ana, socrates o c son constantes; las letras x, y, z suelen ser variables.

2. Predicados y relaciones

P(x) expresa una propiedad de x; R(x,y) expresa una relación entre x e y. Esta diferencia es esencial para modelar conocimiento no reducible a una sola variable.

3. Cuantificadores

forall x φ dice que φ vale para todo objeto. exists x φ dice que φ vale para al menos uno. Ambos cambian profundamente el alcance de la fórmula y exigen mucha atención a los paréntesis.

4. Tableau FOL

El motor usa un tableau analítico con instanciaciones y constantes de Skolem. Eso le da potencia, pero también explica por qué algunas búsquedas pueden cerrarse con unknown si el espacio crece.

Operadores y formas expresivas

forall x φ

Universal

Afirma que φ se cumple para todo individuo del dominio.

Práctica ST

stejecutable

logic classical.first_order
check valid forall x (P(x) -> P(x))

exists x φ

Existencial

Afirma que al menos un individuo cumple φ.

Práctica ST

stejecutable

logic classical.first_order
check satisfiable exists x (P(x) & Q(x))

P(x)

Predicado

Describe una propiedad o condición del individuo x.

Práctica ST

stejecutable

logic classical.first_order
axiom caso = Estudiante(ana)

R(x,y)

Relación

Describe una relación entre dos individuos.

Práctica ST

stejecutable

logic classical.first_order
check satisfiable Ama(ana, musica)

Comandos que debes dominar

Universal a caso concreto

Registra una regla universal y un hecho para derivar una consecuencia individual.

stejecutable

logic classical.first_order
axiom regla : forall x (Estudiante(x) -> Lee(x))
axiom caso = Estudiante(ana)
derive Lee(ana) from {regla, caso}

Validez elemental

Comprueba principios básicos del cuantificador universal.

stejecutable

logic classical.first_order
check valid forall x (P(x) -> P(x))
check valid (forall x P(x)) -> P(a)

Existencia

Explora el paso entre casos particulares y existencia.

stejecutable

logic classical.first_order
check valid P(a) -> exists x P(x)
countermodel exists x P(x) -> forall x P(x)

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.

Instanciación guiada con alias semánticos

Hace visible el paso desde una regla universal a un caso particular usando variables nombradas y explicación intermedia.

stejecutable

logic classical.first_order
let regla = "Todo estudiante de lógica practica" : forall x (Estudiante(x) -> Practica(x))
let caso = "Ana estudia lógica" : Estudiante(ana)

fn revisarCaso(F) {
  explain F
  return F
}

revisarCaso(regla)
derive Practica(ana) from {regla, caso}

if valid (forall x (Estudiante(x) -> Practica(x))) -> (Estudiante(ana) -> Practica(ana)) {
  print "la instanciación universal quedó clara"
}

Pequeño laboratorio de cuantificadores

Agrupa varias fórmulas para que la clase compare qué se conserva y qué no al pasar de universal a existencial.

stejecutable

logic classical.first_order
fn revisarFormula(F) {
  explain F
  return F
}

for Formula in { forall x (Humano(x) -> Mortal(x)), P(a) -> exists x P(x) } {
  revisarFormula(Formula)
}

if valid P(a) -> exists x P(x) {
  print "el paso a existencia es válido"
}

Lecciones prácticas largas

Todos los humanos son mortales

La derivación canónica de la tradición lógica.

stejecutable

logic classical.first_order
axiom regla : forall x (Humano(x) -> Mortal(x))
axiom caso = Humano(socrates)
derive Mortal(socrates) from {regla, caso}

Propiedad universal no invertible

Muestra que de “existe alguien con P” no se sigue “todos tienen P”.

stejecutable

logic classical.first_order
countermodel exists x P(x) -> forall x P(x)

Compatibilidad con conjunciones

Combina cuantificación y conectivos clásicos.

stejecutable

logic classical.first_order
check satisfiable exists x (Estudiante(x) & Lee(x))
check valid forall x ((P(x) -> Q(x)) -> (P(x) -> Q(x)))

Errores frecuentes al estudiar esta lógica

Olvidar el alcance del cuantificador.
Leer exists x P(x) como si hablara de un individuo específico ya nombrado.
Usar derive con fórmulas no registradas en axioms o theorems.
Suponer que todo problema FOL tendrá decisión rápida.

Límites del motor y advertencias

El tableau FOL del motor usa profundidad máxima 50.
Puede devolver unknown en fórmulas complejas.
No es un sistema completo para toda la práctica matemática avanzada; está orientado a docencia y experimentación guiada.

Cómo conecta con otras lógicas

Viene después de proposicional.
Prepara muy bien el paso a silogística aristotélica y a modelados normativos con entidades.
También ayuda a leer mejor fórmulas de Text Layer cuando formalizas documentos.