Logik/Vollständigkeitssatz/Modellkonstruktion/Fakt

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

Dann liefert die in Fakt beschriebene Konstruktion eine Äquivalenzrelation auf der Menge aller Terme und wohldefinierte Relationen bzw. Funktionen auf der Menge der Termklassen.