Una relación entre teorías formales por la cual las pruebas o teoremas de una teoría T1 pueden ser simulados, reconstruidos o traducidos dentro de otra teoría T2, a menudo mostrando que las derivaciones en T1 corresponden a derivaciones en T2 posiblemente con maquinaria adicional limitada.

Principio

La regla organizadora es la simulabilidad de derivaciones: una reducción prueba-teórica proporciona una traducción sistemática de pruebas (o una transformación de prueba) de T1 a T2 que preserva la demostrabilidad y, cuando procede, acota medidas prueba-teóricas como la fuerza ordinal o los principios de inducción.

Demostración

Una demostración concreta es mostrar que un subsistema S de la aritmética es reducible prueba-teóricamente a un sistema más débil R dando un método que toma cualquier prueba en S de una oración del lenguaje común y produce una prueba en R, quizá eliminando ciertas reglas de inferencia o interpretando los principios de S en R mediante una transformación de pruebas.

Aplicación incorrecta

Tratar la conservatividad de teoremas como equivalente a la reducción prueba-teórica sin exhibir traducciones constructivas de pruebas, o asumir que la reducción implica interpretabilidad semántica de modelos en lugar de reconstruibilidad sintáctica de pruebas.

Consecuencia

Cuando se establece, tal reducción ofrece comprensión sobre la fuerza relativa de teorías, permite transferir cotas prueba-teóricas (consistencia, ordinales) y puede mostrar que una teoría no demuestra nuevos tipos de oraciones de ciertas clases sintácticas en relación con otra.

Inversión

Invertir la dirección (intentar simular T2 dentro de T1) normalmente cambia qué teoría es más fuerte; reducciones mutuas pueden indicar equivalencia en fuerza prueba-teórica, mientras que una reducción unidireccional muestra contención prueba-teórica relativa.

Límite

Se aplica dentro de sistemas de prueba formales y a pruebas sintácticas; excluye relaciones puramente semánticas como interpretabilidad modelo-teórica a menos que vayan acompañadas de traducciones concretas de pruebas, y depende del formalismo de prueba elegido y de los esquemas permitidos para la traducción.

Tensión semántica

La reducción prueba-teórica está próxima pero es distinta de la interpretabilidad y la conservatividad: la interpretabilidad a menudo se centra en traducir modelos y lenguaje, mientras la conservatividad considera conjuntos de teoremas; la reducción prueba-teórica exige transformaciones explícitas a nivel de pruebas.

Síntesis

La reducción prueba-teórica es la simulación sintáctica de una teoría dentro de otra mediante traducciones explícitas de pruebas o reconstrucciones, ofreciendo una medida directa de la potencia deductiva relativa y aclarando qué principios inferenciales de una teoría son eliminables o reproducibles en otra.