Une relation entre théories formelles par laquelle les preuves ou théorèmes d'une théorie T1 peuvent être simulés, reconstruits ou traduits à l'intérieur d'une autre théorie T2, souvent en montrant que les dérivations dans T1 correspondent à des dérivations dans T2 éventuellement avec des dispositifs supplémentaires bornés.

Principe

La règle organisatrice est la simulabilité des dérivations : une réduction preuve-théorique fournit une traduction systématique des preuves (ou une transformation de preuve) de T1 vers T2 qui préserve la démontrabilité et, le cas échéant, des bornes sur des mesures proof-théoriques telles que la force ordinale ou les principes d'induction.

Démonstration

Une démonstration concrète consiste à montrer qu'un sous-système S de l'arithmétique est réduit preuve-théoriquement à un système plus faible R en donnant une méthode qui prend toute preuve dans S d'une phrase du langage commun et produit une preuve dans R, par exemple en éliminant certaines règles d'inférence ou en interprétant les principes de S dans R via une transformation de preuve.

Mauvaise application

Confondre la conservativité des théorèmes avec la réduction preuve-théorique sans exhiber de traductions constructives de preuves, ou supposer que la réduction implique une interprétabilité sémantique des modèles plutôt qu'une reconstructibilité syntaxique des preuves.

Conséquence

Quand elle est établie, une telle réduction apporte un éclairage sur la force relative des théories, permet le transfert de bornes proof-théoriques (consistance, ordinaux) et peut montrer qu'une théorie n'établit pas de nouveaux types de phrases de certaines classes syntaxiques par rapport à une autre.

Inversion

Inverser la direction (essayer de simuler T2 dans T1) modifie généralement quelle théorie est plus forte ; des réductions mutuelles peuvent indiquer une équivalence de force preuve-théorique, tandis qu'une réduction unidirectionnelle montre un enfermement preuve-théorique relatif.

Limite

S'applique aux systèmes de preuve formels et aux preuves syntaxiques ; exclut les relations purement sémantiques comme l'interprétabilité modèle-théorique sauf si elles s'accompagnent de traductions effectives de preuves, et dépend du formalisme de preuve choisi et des schémas admissibles pour la traduction.

Tension sémantique

La réduction preuve-théorique est proche mais distincte de l'interprétabilité et de la conservativité : l'interprétabilité se concentre souvent sur la traduction des modèles et du langage tandis que la conservativité considère les ensembles de théorèmes ; la réduction proof-théorique exige des transformations explicites au niveau des preuves.

Synthèse

La réduction preuve-théorique est la simulation syntaxique d'une théorie dans une autre par des traductions explicites de preuves ou des reconstructions, fournissant une mesure directe de la puissance déductive relative et clarifiant quels principes d'inférence d'une théorie sont éliminables ou reproductibles dans une autre.