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 .