Elimination von Variablen

Um im Sequenzenkalkül Probleme mit freien Variablen zu vermeiden, werden diese durch Konstantensymbole ersetzt.
Lemma: Sei $\phi (x_1,\dots ,x_k)$ eine Formel. Seien $c_1,\dots ,c_k$ neue Konstantensymbole (nicht in der Signatur).
$\phi$ ist erfüllbar gdw. $\phi [x_1/c_1,\dots ,x_k/c_k]$ erfüllbar ist.
Dies erlaubt uns, im Kalkül ausschließlich mit Sätzen zu arbeiten.