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

[![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 $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 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