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. 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. (We allow the interpretation of the predicate letters $G$, $H$, etc. to be determined by the truth-assignment.)

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 why the functions must be defined on the domain $\{1,2,...ns\}$.

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)