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.  

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$":   

[![enter image description here][1]][1]

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 $nth$ 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)
    


  [1]: https://i.sstatic.net/j63tV.png