La teoría de la demostración es la rama de la lógica formal que estudia las demostraciones como objetos formales y sintácticos: analiza la estructura, las transformaciones y las propiedades de las derivaciones formales dentro de sistemas de prueba especificados (p. ej., normalización, eliminación de cortes, decidibilidad, consistencia), tratando las reglas, transformaciones de prueba y relaciones de derivabilidad como objetos primarios de investigación más que la semántica basada en modelos.

Principio

Las propiedades de las demostraciones formales (como la transformabilidad a forma normal o la admisibilidad de ciertas reglas) revelan relaciones meta-nivel entre sistemas y pueden usarse para extraer contenido computacional, comparar la fuerza de sistemas o establecer afirmaciones de consistencia y conservación sobre teorías.

Demostración

Escenario ilustrativo — Situación: En una presentación por deducción natural, una demostración contiene una introducción seguida inmediatamente por la eliminación del mismo conectivo (un rodeo). Reconocimiento: Una transformación prueba-teórica (normalización) identifica ese rodeo. Acción: Aplicar la normalización para eliminarlo y producir una demostración en forma normal, más corta. Consecuencia: La demostración transformada hace explícita la dependencia de las conclusiones respecto de las premisas y puede exponer contenido constructivo o reducir la complejidad de la prueba.

Aplicación incorrecta

Igualar la consecuencia prueba-teórica con la consecuencia semántica sin especificar el sistema y su relación con una semántica; el error es asumir que la derivabilidad sintáctica implica las mismas nociones que la verdad en todos los modelos pretendidos sin considerar la corrección (soundness).

Consecuencia

Los resultados de teoría de la demostración proporcionan información constructiva sobre la inferencia (p. ej., algoritmos vinculados a la normalización), clarifican la fuerza relativa de los sistemas y pueden mostrar consistencia o independencia; estas consecuencias son internas a los sistemas formales y su metateoría, no afirmaciones empíricas directas.

Inversión

Diferentes sistemas de demostración o cambios en principios lógicos subyacentes (clásico frente a constructivo) alteran qué propiedades prueba-teóricas se mantienen; una transformación válida en una formalización puede fallar o carecer de sentido en otra, por lo que las afirmaciones de teoría de la demostración son relativas al sistema y sensibles a supuestos estructurales.

Límite

Claro dentro: análisis sintáctico de derivaciones en sistemas formales y transformaciones entre pruebas. Caso límite: descripciones informales de estrategias de prueba que sugieren pero no formalizan pasos de normalización. Claro fuera: análisis semánticos o modelo-teóricos que tratan la verdad en estructuras más que los objetos de prueba sintácticos.

Tensión semántica

Sintaxis ↔ Semántica — la teoría de la demostración enfatiza objetos sintácticos manipulables (pruebas, reglas, transformaciones), mientras que la semántica investiga la verdad en modelos; ambas perspectivas se restringen mutuamente pero responden a preguntas distintas.

Síntesis

La teoría de la demostración trata las demostraciones como objetos matemáticos cuya manipulación aporta conocimientos sobre cómputo, constructividad y consistencia relativa; sus conclusiones son más firmes cuando el sistema formal y los compromisos interpretativos están claramente especificados.