Godel'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 $ith$ 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.  
   

A *satisfying system of level n* is a system of functions $\mathfrak{F} = \{f_1^{n},f_2^n,... f_k^n,...\}$ defined on the domain $\{1,2,...,ns\}$ (where $ns$ is the largest index on an individual variable introduced at the $nth$ level), and an assignment $w$ of truth values such that when the functional variables $F_i$ of $A_n$ are replaced by the $f_i^n$, the propositional variables by their truth values under $w$, and the individual variables $v_i$ by their integer indexes, a true proposition results.


**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\}$.** 

 

Godel writes:

> Satisfying systems of level $n$
obviously exist if and only if $B_n$ is satisfiable. 

$B_n$ is the propositional counterpart of $A_n$ resulting from the replacements described above 

**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$?