 The next pieces of \(D\) are the clauses for the quantifiers. Let \(\theta\) be a formula, \(v\) a variable, and \(t\) a term (i.e., a variable or a constant). Then define \(\theta(v|t)\) to be the result of substituting \(t\) for each free occurrence of \(v\) in \(\theta\). So, if \(\theta\) is \((Qx \amp \exists\)xPxy), then \(\theta(x|c)\) is \((Qc \amp \exists\)xPxy). The last occurrence of \(x\) is not free.