Definitions and assumptions
We work with first-order predicate calculus. Our languages allow constant, function and relation symbols. Structures consist of (non-empty) domains and interpretations of the relevant symbols as constant members, functions or relations over that domain.
We fix some axiomatization of the predicate calculus: logical axioms and rules of inference. Any of the several well-known axiomatisations will do; we assume without proof all the basic well-known results about our formalism (such as the normal form theorem or the soundness theorem) that we need.
We axiomatize predicate calculus without equality, i.e. there are no special axioms expressing the properties of equality as a special relation symbol. After the basic form of the theorem is proved, it will be easy to extend it to the case of predicate calculus with equality.
Statement of the theorem and some reductions
Theorem 1. Every formula valid in all structures is provable.
This is the most basic form of the completeness theorem. We immediately restate it in a form more convenient for our purposes:
Theorem 2. Every formula φ is either refutable, or satisfiable in some structure.
Note that "φ is refutable" means by definition "¬φ is provable".
To see the equivalence, note first that if Theorem 1 holds, and φ is not satisfiable in any structure, then ¬φ is valid in all structures and therefore provable, thus φ is refutable and Theorem 2 holds. If on the other hand Theorem 2 holds and φ is valid in all structures, then ¬φ is not satisfiable in any structure and therefore refutable; then ¬¬φ is provable and then so is φ, thus Theorem 1 holds.
We approach the proof of Theorem 2 by successively restricting the class of all formulas φ for which we need to prove "φ is either refutable or satisfiable". At the beginning we need to prove this for all possible formulas φ in our language. However, suppose that for every formula φ there is some formula ψ taken from a more restricted class of formulas C, such that "ψ is either refutable or falsifiable" → "φ is either refutable or falsifiable". Then, once this claim (expressed in the previous sentence) is proved, it will suffice to prove "φ is either refutable or falisifiable" only for φ's belonging to the class C. Note also that if φ is provably equivalent to ψ (i.e., (φ≡ψ) is provable), then it is indeed the case that "ψ is either refutable or satisfiable" → "φ is either refutable or satisfiable" (the soundness theorem is needed to show this).
We start restricting the class of formulas φ to prove our theorem for by eliminating function and constant symbols. (to be rewritten...) According to the considerations in the previous paragraph, we see now that we need only to prove Theorem 2 for φ's which do not use function or constant symbols.
Note: the reduction of the preceding paragraph is absent from Gödel's paper because he uses a version of first-order predicate calculus which has no function or constant symbols to begin with.
Next we consider a generic formula φ (which no longer uses function or constant symbols) and apply the normal form theorem to find a formula ψ in normal form such that φ≡ψ (ψ being in normal form means that all the quantifiers in ψ, if there are any, are found at the very beginning of ψ). The normal form theorem proves that such a ψ exists for every φ, and the construction of ψ from φ adds no new function or constant symbols. It follows now that we need only prove Theorem 2 for formulas φ in normal form without function or constant symbols.
Next, we eliminate all free variables from φ by quantifying them existentially: if, say, x1...xn are free in φ, we form ψ = ∃x1...∃xnφ . If ψ is satisfiable in a structure M, then certainly so is φ; and if ψ is refutable, then ¬ψ = ∀x1...∀xn¬φ is provable, and then so is ¬φ, thus φ is refutable. We see that we can restrict φ to be a sentence, that is, a formula with no free variables.
Finally, we would like, for reasons of technical convenience, that the prefix of φ (that is, the string of quantifiers at the beginning of φ, which is in normal form) begin with a universal quantifier and end with an existential quantifier. To achieve this for a generic φ (subject to restrictions we have already proved), we take some one-place relation symbol F unused in φ, and two new variables y and z.. If φ = (P)Φ, where (P) stands for the prefix of φ and Φ for the matrix (the remaining, quantifier-free part of φ) we form ψ = ∀y (P) ∃∀z ( Φ ∨ [ F(y) ∨ ¬F(z) ] ). Since ∀y∃z ( F(y) ∨ ¬F(z) ) is clearly provable, it is easy to see that φ≡ψ is provable.
Reducing the theorem to formulas of degree 1
Our generic formula φ now is a sentence, in normal form, and its prefix starts with a universal quantifier and ends with an existential quantifier. Let us call the class of all such formulas R. We are faced with proving that every formula in R is either refutable or satisfiable. Given our formula φ, we group strings of quantifiers of one kind together in blocks:
φ = (∀x1...∀xk_1)(∃xk_1+1...∃xk_2).......(∀xk_n-2+1...∀xk_n-1)(∃xk_n-1+1...∃xk_n) (Φ)
We define the degree of φ to be the number of universal quantifier blocks, separated by existential quantifier blocks as shown above, in the matrix of &phi. The following lemma lets us sharply reduce the complexity of the generic formula φ for which we need to prove the theorem:
Lemma. Let k>=1. If every formula in R of degree k is either refutable or satisfiable, then so is every formula in R of degree k+1.
Proof. Let φ be a formula of degree k+1; then we can write it as
φ = (∀x)(∃y)(∀u)(∃v) (P) ψ
where (P) is the remainder of the prefix of φ (it is thus of degree k-1) and ψ is the quantifier-free matrix of φ. Note that x, y, u and v denote here tuples of variables rather than single variables; e.g. (∀x) really stands for ∀x1∀x2...∀xn where x1...xn are some distinct variables.
Let now x' and y' be tuples of previously unused variables of the same length as x and y respectively, and let Q be a previously unused relation symbol which takes as many arguments as the sum of lengths of x and y; we consider the formula
Φ = (∀x')(∃y') Q(x',y') ∧ (∀x)(∀y) ( Q(x,y) → (∀u)(∃v)(P)ψ )
We note that clearly Φ→φ is provable.
Now since the string of quantifiers (∀u)(∃v)(P) does not contain variables from x or y, the following equivalence is easily provable with the help of whatever formalism we're using:
( Q(x,y) → (∀u)(∃v)(P)ψ ) ≡ (∀u)(∃v)(P) ( Q(x,y) → ψ )
And since these two formulas are equivalent, if we replace the first with the second inside Φ, we obtain the formula Φ' such that Φ≡Φ':
Φ' = (∀x')(∃y') Q(x',y') ∧ (∀x)(∀y) (∀u)(∃v)(P) ( Q(x,y) → ψ )
Now Φ' has the form (S)ρ ∧ (S')ρ' , where (S) and (S') are some quantifier strings, ρ and ρ' are quantifier-free, and, furthermore, no variable of (S) occurs in ρ' and no variable of (S') occurs in ρ. Under such conditions every formula of the form (T)(ρ ∧ ρ'), where (T) is a string of quantifiers containing all quantifiers in (S) and (S') interleaved among themselves in any fashion, but maintaining the relative order inside (S) and (S'), will be equivalent to the original formula Φ'(this is yet another basic result in first-order predicate calculus that we rely on). To wit, we form Ψ as follows:
Ψ = (∀x')(∀x)(∀y) (∀u)(∃y')(∃v)(P)Q(x',y') ∧ ( Q(x,y) → ψ )
and we have Φ' ≡ Ψ .
Now Ψ is a formula of degree k and therefore by assumption either refutable or satisfiable. If Ψ is satisfiable in a structure M, then, considering Ψ≡Φ'≡Φ and Φ→φ, we see that φ is satisfiable as well. If Ψ is refutable, then so is Φ which is equivalent to it; thus ¬Φ is provable. Now we can replace all occurrences of Q inside the provable formula ¬Φ by some other formula dependent on the same variables, and we will still get a provable formula. (This is yet another basic result of first-order predicate calculus. Depending on the particular formalism adopted for the calculus, it may be seen as a simple application of a "functional substitution" rule of inference, as in Gödel's paper, or it may be proved by considering the formal proof of ¬Φ, replacing in it all occurrences of Q by some other formula with the same free variables, and noting that all logical axioms in the formal proof remain logical axioms after the substitution, and all rules of inference still apply in the same way.)
In this particular case, we replace Q in ¬Φ with the formula (∀u)(∃v)(P)ψ(x,y|x',y') . ¬Φ then becomes
¬ ( (∀x')(∃y') (∀u)(∃v)(P)ψ(x,y|x',y'); ∧ (∀x)(∀y) ( (∀u)(∃v)(P)ψ → (∀u)(∃v)(P)ψ ) )
and this formula is provable; since the part under negation and after the ∧ sign is obviously provable, and the under negation and part before the ∧ sign is obviously φ, just with x and y replaced by x' and y', we see that ¬φ is provable, and φ is refutable. We have proved that φ is either satisfiable or refutable, and this concludes the proof of the Lemma.
Proving the theorem for formulas of degree 1
As shown by the Lemma above, we only need to prove our theorem for formulas φ in R of degree 1 (note that φ cannot be of degree 0, since formulas in R have no free variables and don't use constant symbols).
Extension to first-order predicate calculus with equality
Extension to countable sets of formulas