Gödel's original proof of completeness shows that a formula of the form $\forall \exists A$ is either satisfiable or refutable. The quantifier-free formula $A$ is composed of individual variables $v_i$, functional variables $F_i$, and propositional variables $X_i$, conjoined by propositional connectives according to the standard rules.
The proof constructs a sequence of quantifier-free formulas $A_i$ that can be regarded as approximations to $\forall \exists A$ in a finite domain.
$A_i$ is constructed by dropping the quantifiers of $\forall \exists A$, replacing the $r$-many universal variables of $\forall \exists A$ by the $i^\mathrm{th}$ $r$-tuple of variables $x_1, x_2, ...$ in some pre-given ordering, and adding $n$-many indexed variables (distinct from variables introduced for $A_j, j<i$) to replace the existential variables of $\forall \exists A$. The levels are cumulative so at each level $i$, $A_i$ has $i$-many conjuncts.
The idea is to show that each $A_i$ is satisfiable by the completeness of propositional logic. For this, Godel introduces the notions of a propositional counterpart $B_n$ of $A_n$, and a "satisfying system of level $n$":
Here, "functional variables"are what we would call uninterpreted function symbols, and "propositional variables" are the basic building blocks of propositional logic (e.g. the sentential letters "$P$" and "$Q$" in the formula "$P \lor Q$") whose values vary over the truth values 0 and 1. The integer $ns$ refers to the largest index on an individual variable $x_i$ introduced at the $n^\mathrm{th}$ level, where $s$ is the number of existentially quantified variables in the original formula $\forall \exists A$.
Question: I don't understand the right to left direction in the case where $A$ contains functional variables. Why couldn't $B_n$ be satisfied by a system of level greater than $n$, that is, by replacing the functional variables by a system of functions defined on a domain bounded by some $m > ns$?
To elaborate,
If we assume that $A$ does not contain functional variables, then $A_n$ would consist entirely of propositional variables $X_i$ and atomic formulas of the form $G(v_1,...v_n,...v_{ns})$. If we replace individual variables by their indices, then the formulas $G(1, ...,n,...ns)$ may also be treated as propositional variables. The idea is to consider all truth-assignments to these variables representing atomic propositions (We allow the interpretation of the predicate letters $G$, $H$, etc. to be determined by the truth-assignment). A satisfying system would (on the above assumption) simply be an assignment of truth-values such that the resulting propositional counterpart of $A_n$ comes out true. In this case, it makes sense why every satisfying system of level $n+1$ is an extension of a system of level $n$.
However, $A$ may contain functional variables, so that some of the atomic components have forms such as $G(F_1(v_i), F_2(v_j))$. The functional terms $F_i(v)$ need to be assigned denotations in order for $G(F_1(v_i), F_2(v_j))$ to be treated as a propositional variable and assigned a truth-value. This explains the need for a system of functions to replace the variables $F_i$. But it does not explain (a) why the functions must be defined on the domain $\{1,2,...ns\}$, nor (b) why every satisfying system of level $n+1$ extends one of level $n$. Again, (b) is true before the addition of function symbols. But considering all possible denotations for the function symbols, only some of the functions of level $n+1$ coincide with functions of level $n$ when restricted to the same domains.
Reference
Kurt Godel, [1986] Collected Works. I: Publications 1929–1936. S. Feferman, S. Kleene, G. Moore, R. Solovay, and J. van Heijenoort (eds.), Oxford: Oxford University Press. (p. 115-116)
