Sistemas formales, explicados con honestidad

Explorador de la Incompletitud de Gödel

Una página interactiva más clara sobre sistemas formales, axiomas, derivaciones, consistencia y por qué aparece la incompletitud.

Qué es realmente esta página

Este es un simulador de sistemas formales de juguete. No demuestra directamente los teoremas de Gödel. Te ayuda a ver qué hacen los axiomas, cómo crecen las derivaciones y por qué “añadir más axiomas” no elimina mágicamente la incompletitud.

Constructor del Sistema

Reglas Ejecutables

Controles de Derivación

Velocidad de animación 5x

Axiomas 0

Enunciados conocidos 0

Teoremas derivados 0

Profundidad de prueba 0

Consistencia Consistent

Línea Temporal de Derivación

0

Cada paso de abajo es un axioma inicial o un enunciado derivado producido por el motor de juguete.

Próximos Pasos Pendientes

Estos son los enunciados que el simulador puede derivar a continuación a partir de los axiomas actuales y los enunciados ya conocidos.

Cómo funciona “Añadir Axioma”

Un axioma personalizado se añade a la lista de premisas de la izquierda.
Si su fórmula coincide con una de las formas de regla admitidas, se vuelve operativa dentro del motor de juguete.
Si no coincide con un patrón admitido, sigue registrándose como axioma, pero no genera ningún teorema automático.
Si añades una afirmación y su negación, el sistema se vuelve inconsistente.

Patrones personalizados admitidos

Afirmación atómica: P o S(0) ∈ ℕ
Negación: ¬P
Implicación: P → Q

Comprobación de Consistencia

Por qué la incompletitud sigue importando

Un sistema formal en una frase

Un sistema formal comienza con axiomas y usa reglas de inferencia para derivar teoremas. La cuestión crucial no es solo qué puede derivarse, sino también qué no puede derivarse sin romper la consistencia.

El movimiento de Gödel

Gödel codificó fórmulas y pruebas como números, y luego construyó una oración que dice en efecto: “No soy demostrable en este sistema”. Si el sistema es consistente, esa oración no puede demostrarse dentro del sistema, y sin embargo es verdadera en la interpretación pretendida.

Qué puede y qué no puede hacer este simulador

Esta página modela un pequeño motor de reglas para que puedas ver cómo los axiomas expanden una teoría. No implementa aritmética de primer orden completa, numeración de Gödel ni verificación real de pruebas. Es un puente conceptual, no un asistente de pruebas.

Experimentos útiles

Empieza con “0 ∈ ℕ” y el axioma del sucesor, y avanza por los numerales derivados.
Añade P → Q y luego añade P para ver cómo modus ponens crea Q.
Añade tanto P como ¬P para ver cómo se detecta la inconsistencia.