Eine Verstärkung der Interpolation, die verlangt, dass für jede Formel φ und jede gewählte Teilsprache (Menge nicht-logischer Symbole) Σ eine Formel ψ existiert, die nur Symbole aus Σ benutzt und genau die Σ-Folgerungen von φ einfängt; ψ ist uniform im Sinne, dass sie für alle Folgerungen von φ in der Teilsprache wirkt.

Prinzip

Das ordnende Prinzip ist die Symbolelimination mittels eines einzigen Interpolanten: Anstatt für jede spezifische Konsequenz einen angepassten Interpolanten zu liefern, verlangt die uniforme Interpolation eine kanonische Formel, die alle Konsequenzen im eingeschränkten Vokabular einheitlich repräsentiert.

Demonstration

Beispiel: Die Aussagenlogik besitzt uniforme Interpolation durch Variablenelimination (Forgetting): Gegeben eine Formel φ und eine Menge zu bewahrender atomarer Propositionen, konstruiert man eine Formel ψ in der kleineren Sprache, die genau die Konsequenzen von φ in dieser Sprache charakterisiert.

Fehlanwendung

Die uniforme Interpolation mit der Craig-Interpolation zu verwechseln ist eine Fehlanwendung: Craig-Interpolation liefert für jedes Entailmentpaar φ ⊨ χ einen Interpolanten, sichert jedoch nicht die Existenz einer einzigen ψ, die alle Σ-Folgerungen von φ erfasst; aus Craig-Interpolation uniforme Interpolation zu folgern ist falsch.

Konsequenz

Besitzt eine Logik uniforme Interpolation, so ermöglicht dies robustes modulares Schließen, komponentenspezifische Spezifikation und effektive Symbolelimination; häufig impliziert es verwandte Definierbarkeitseigenschaften und unterstützt algorithmische Abstraktionsverfahren.

Umkehrung

Das Fehlen uniformer Interpolation bedeutet, dass es Formeln gibt, deren Konsequenzen in einer Teilsprache nicht durch eine einzelne Formel in dieser Teilsprache erfasst werden können, was uniforme Symbolelimination verhindert und die Modulzusammensetzung erschwert.

Abgrenzung

Die Eigenschaft ist empfindlich gegenüber der gewählten Logik und den erlaubten Sprachfragmenten: Einige modale und propositionale Systeme besitzen uniforme Interpolation, viele erste-Ordnung-Fragmenten nicht, und zusätzliche Operatoren oder Quantormuster können die Uniformität zerstören.

Semantische Spannung

Es besteht Spannung zwischen uniformer Interpolation und Ausdrucksstärke: Reichere Logiken können mehr Unterscheidungen treffen, verlieren dabei aber möglicherweise uniforme Interpolanten; uniforme Interpolation handelt vom Austausch von Ausdrucksstärke gegen modulare Komprimierbarkeit von Informationen.

Synthese

Uniforme Interpolation formalisiert eine uniforme Form des Symbolvergessens: Sie garantiert, dass man zu jeder Formel eine kanonische Darstellung ihrer Konsequenzen in einem eingeschränkten Vokabular extrahieren kann, was bei Bestehen der Eigenschaft ein mächtiges Werkzeug für Modularität, Definierbarkeit und automatische Abstraktion ist.