Questions on proof of Gödel's Completeness Theorem in A Friendly Introduction to Mahematical Logic by Leary and Kristiansen In Proposition 3.2.6, the authors are trying to prove that the structure $\mathfrak{U}$, whose universe is the equivalence classes of the variable free terms, models the set of sentences $\Sigma'$ using induction.
They use the usual trick of completing the proof by doing induction on complexity of the formula like they do here in Theorem 1.4.2. But when it comes to proving the base cases which is showing that statement $\sigma \in \Sigma^\prime \: \text{if and only if} \: \mathfrak{A} \models \sigma$ holds for the relations, they only consider the variable free terms, not all of the terms. How do I justify this? Shouldn't we prove for all terms instead of just the variable free terms?
Also, when proving $\sigma \in \Sigma^\prime \: \text{if and only if} \: \mathfrak{A} \models \sigma$ for statements of the form $\forall x \varphi$, the authors say that $\varphi^x_{t}$ is less complex than $\forall x \varphi$ so the induction hypothesis holds for $\varphi^x_{t}$. How do I make all of these rigorous?
I'm looking for a proper justification of all these arguments. What should I be doing induction on?
 A: The ability to avoid free variables comes from the fact that all the elements of the structure we're looking at are named by closed terms: to check that $\mathfrak{A}\models\forall x\varphi(x)$ we just need to check that $\mathfrak{A}\models\varphi(t)$ for each closed term $t$. This is not true for all structures in general - it's a very special feature of the structure $\mathfrak{A}$ built in the proof.
(On the other hand, every structure $\mathfrak{B}$ has an expansion $\hat{\mathfrak{B}}$ gotten by adding new constant symbols naming all the elements. We then can just work with sentences in the $\hat{\mathfrak{B}}$-context rather than with formulas in the $\mathfrak{B}$-context. This language-expansion trick is really just a repackaging of variable assignments, but it can frequently be convenient; I personally prefer it.)
As to the measure of complexity, this is the same as (in my experience anyways) all the usual arguments by induction on complexity: we count logical operators, that is, Booleans and quantifiers. From "$\forall x\varphi(x)$" to "$\varphi(t)$" is clearly a step down, regardless of how complicated the term $t$ is, since terms cannot use logical operators.
