Logik/Vollständigkeitssatz/Modellkonstruktion/Konsistente Terminterpretation/Fakt

Es sei eine Menge an -Ausdrücken (über einem Symbolalphabet ), die abgeschlossen unter Ableitungen ist.

Dann gilt für die Interpretation , wobei die in Fakt beschriebene Menge aus Termklassen (mit der natürlichen Interpretation von Konstanten, Funktionssymbolen und Relationssymbolen) und die natürliche Belegung für Variablen ist, die Beziehung

für alle Terme .