Formule jsou termy a:
Realizace definuje konstanty, funkční symboly, predikátové symboly. Ne proměnné! Dostáváme tedy něco jako „předpis“ který čeklá na dosazení za proměnné.
Když už dosadíme za proměnné, provádíme ohodnocení proměnných.
Tautologie je formule platná v každé realizaci, kontradikce obdobně.
Formule je splnitelná, pokud existuje nějaká realizace a ohodnocení proměnných ve kterém je platná.
Formule je logicky platná v nějaké realizaci pokud je úplně jedno jak ohodnotím proměnné a vždy to bude pravdivé.
Formule jsou ekvivalentní pokud pro libovolné realizace (ale pro obě formule stejné) a pro libovolné ohodnocení (opět stejné pro obě formule) dávají vždy stejné výsledky.