Eine Beziehung zwischen formalen Theorien, bei der Beweise oder Theoreme einer Theorie T1 innerhalb einer anderen Theorie T2 simuliert, rekonstruiert oder übersetzt werden können, oft indem man zeigt, dass Ableitungen in T1 entsprechenden Ableitungen in T2 entsprechen, eventuell mit beschränkter zusätzlicher Mechanik.

Prinzip

Das ordnende Prinzip ist die Simulierbarkeit von Ableitungen: eine beweistheoretische Reduktion liefert eine systematische Übersetzung von Beweisen (oder eine Beweistransformation) von T1 nach T2, die die Beweisbarkeit erhält und gegebenenfalls Schranken auf beweistheoretische Maße wie Ordinalstärke oder Induktionsprinzipien beachtet.

Demonstration

Eine konkrete Demonstration besteht darin, zu zeigen, dass ein Untersystem S der Arithmetik beweistheoretisch auf ein schwächeres System R reduzierbar ist, indem man ein Verfahren angibt, das jeden S-Beweis eines Satzes der gemeinsamen Sprache in einen R-Beweis überführt, etwa durch Eliminierung bestimmter Inferenzregeln oder durch Interpretation von S-Prinzipien in R mittels Beweistransformation.

Fehlanwendung

Konfudierung der Konservativität von Theoremen mit beweistheoretischer Reduktion ohne konstruktive Beweistranslationen aufzuzeigen, oder die Annahme, Reduktion impliziere semantische Interpretierbarkeit von Modellen statt syntaktischer Rekonstruktionsfähigkeit von Beweisen.

Konsequenz

Ist eine solche Reduktion etabliert, liefert sie Einsicht in die relative Stärke von Theorien, erlaubt den Transfer beweistheoretischer Schranken (Konsistenz, Ordinale) und kann zeigen, dass eine Theorie gegenüber einer anderen keine neuen Sätze bestimmter syntaktischer Klassen beweist.

Umkehrung

Kehren man die Richtung um (T2 in T1 zu simulieren), ändert sich in der Regel, welche Theorie stärker ist; wechselseitige Reduktionen können auf Gleichheit in beweistheoretischer Stärke hinweisen, während eine einseitige Reduktion relative beweistheoretische Einschließung zeigt.

Abgrenzung

Gilt innerhalb formaler Beweissysteme und für syntaktische Beweise; schließt rein semantische Beziehungen wie modelltheoretische Interpretierbarkeit aus, sofern sie nicht durch konkrete Beweistranslationen begleitet werden, und hängt vom gewählten Beweisformalismus und zulässigen Übersetzungsschemata ab.

Semantische Spannung

Beweistheoretische Reduktion steht nahe bei, ist aber verschieden von Interpretierbarkeit und Konservativität: Interpretierbarkeit fokussiert oft auf Modell- und Sprachübersetzungen, Konservativität auf Theorem-Mengen; beweistheoretische Reduktion verlangt explizite Transformationen auf Beweisebene.

Synthese

Beweistheoretische Reduktion ist die syntaktische Simulation einer Theorie in einer anderen durch explizite Beweistranslationen oder Rekonstruktionen, sie liefert ein direktes Maß für relative deduktive Macht und macht deutlich, welche Inferenzprinzipien einer Theorie in einer anderen eliminierbar oder reproduzierbar sind.