Famous Theorems of Mathematics/Logic

Gödel's completeness theorem

In the following, we state two equivalent forms of the theorem, and show their equivalence.

Later, we prove the theorem. This is done in the following steps:

1. Reducing the theorem to sentences (formulas with no free variables) in prenex form, i.e. with all quantifiers ($\forall$ and $\exists$) at the beginning. Furthermore, we reduce it to formulas whose first quantifier is $\forall$. This is possible because for every sentence, there is an equivalent one in prenex form whose first quantifier is $\forall$.
2. Reducing the theorem to sentences of the form $\forall x_{1}\forall x_{2}...\forall x_{k}\exists y_{1}\exists y_{2}...\exists y_{m}\phi (x_{1}...x_{k},y_{1}...y_{m})$. While we cannot do this by simply rearranging the quantifiers, we show that it is yet enough to prove the theorem for sentences of that form.
3. Finally we prove the theorem for sentences of that form.
   • This is done by first noting that a sentence such as $B=\exists x_{1}\exists x_{2}...\exists x_{k}\exists y_{1}\exists y_{2}...\exists y_{m}\phi (x_{1}...x_{k},y_{1}...y_{m})$ is either refutable or has some model in which it holds; this model is simply assigning truth values to the subpropositions from which B is built of. The reason for that is the completeness of propositional logic, with the existential quantifiers playing no role.
   • We extend this result to more and more complex and lengthy sentences, D_n (n=1,2...), built out from B, so that either any of them is refutable and therefore so is φ, or all of them are not refutable and therefore each holds in some model.
   • We finally use the models in which the D_n hold (in case all are not refutable) in order to build a model in which φ holds.

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.

"φ is refutable" means by definition "¬φ is provable".

Equivalence of both theorems

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.

Proof of theorem 2: first step

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 satisfiable" → "φ is either refutable or satisfiable". Then, once this claim (expressed in the previous sentence) is proved, it will suffice to prove "φ is either refutable or satisfiable" 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).

There are standard techniques for rewriting an arbitrary formula into one which does not use function or constant symbols, at the cost of introducing additional quantifiers; we will therefore assume that all formulas are free of such symbols. In Gödel's paper, 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 prenex 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 ψ). It follows now that we need only prove Theorem 2 for formulas φ in normal form.

Next, we eliminate all free variables from φ by quantifying them existentially: if, say, x₁...x_n are free in φ, we form $\psi =\exists x_{1}...\exists x_{n}\phi$. If ψ is satisfiable in a structure M, then certainly so is φ and if ψ is refutable, then $\neg \psi =\forall x_{1}...\forall x_{n}\neg \phi$ 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 $\psi =\forall y(P)\exists z(\Phi \wedge [F(y)\vee \neg F(z)])$. Since $\forall y\exists z(F(y)\vee \neg F(z))$ is clearly provable, it is easy to see that $\phi =\psi$ 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:

$\phi =(\forall x_{1}...\forall x_{k_{1}})(\exists x_{k_{1}+1}...\exists x_{k_{2}}).......(\forall x_{k_{n-2}+1}...\forall x_{k_{n-1}})(\exists x_{k_{n-1}+1}...\exists x_{k_{n}})(\Phi )$

We define the degree of $\phi$ to be the number of universal quantifier blocks, separated by existential quantifier blocks as shown above, in the matrix of $\phi$. The following lemma, which Gödel adapted from Skolem's proof of the Löwenheim-Skolem theorem, lets us sharply reduce the complexity of the generic formula $\phi$ 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.

Comment: Take a formula φ of degree k+1 of the form $\phi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi$, where $(P)\psi$ is the remainder of $\phi$ (it is thus of degree k-1). φ states that for every x there is a y such that... (something). It would have been nice to have a predicate Q' so that for every x, Q'(x,y) would be true if and only if y is the required one to make (something) true. Then we could have written a formula of degree k which is equivalent to φ, namely $(\forall x')(\forall x)(\forall y)(\forall u)(\exists v)(\exists y')(P)Q'(x',y')\wedge (Q'(x,y)\rightarrow \psi )$. This formula is indeed equivalent to φ because it states that for every x, if there is a y which satisfies Q'(x,y), then (something) holds, and furthermore, we know that there is such a y, because for every x', there is a y' which satisfies Q'(x',y'). Therefore φ follows from this formula. It is also easy to show that if the formula is false, then so is φ. Unfortunately, in general there is no such predicate Q'. However, this idea can be understood as a basis for the following proof of the Lemma.

Proof. Let φ be a formula of degree k+1; then we can write it as

$\phi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi$

where (P) is the remainder of the prefix of $\phi$ (it is thus of degree k-1) and $\psi$ is the quantifier-free matrix of $\phi$. x, y, u and v denote here tuples of variables rather than single variables; e.g. $(\forall x)$ really stands for $\forall x_{1}\forall x_{2}...\forall x_{n}$ where $x_{1}...x_{n}$ 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

$\Phi =(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )$

Clearly, $\Phi \rightarrow \phi$ is provable.

Now since the string of quantifiers $(\forall u)(\exists 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)\rightarrow (\forall u)(\exists v)(P)\psi )\equiv (\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )$

And since these two formulas are equivalent, if we replace the first with the second inside Φ, we obtain the formula Φ' such that Φ≡Φ':

$\Phi '=(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )$

Now Φ' has the form $(S)\rho \wedge (S')\rho '$, 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)(\rho \wedge \rho ')$, 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:

$\Psi =(\forall x')(\forall x)(\forall y)(\forall u)(\exists y')(\exists v)(P)Q(x',y')\wedge (Q(x,y)\rightarrow \psi )$

and we have $\Phi '\equiv \Psi$.

Now $\Psi$ is a formula of degree k and therefore by assumption either refutable or satisfiable. If $\Psi$ is satisfiable in a structure M, then, considering $\Psi \equiv \Phi '\equiv \Phi \wedge \Phi \rightarrow \phi$, we see that $\phi$ is satisfiable as well. If $\Psi$ is refutable, then so is $\Phi$ which is equivalent to it; thus $\neg \Phi$ is provable. Now we can replace all occurrences of Q inside the provable formula $\neg \Phi$ 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 $\neg \Phi$, 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(x',y') in $\neg \Phi$ with the formula $(\forall u)(\exists v)(P)\psi (x,y|x',y')$. Here (x,y|x',y') means that instead of ψ we are writing a different formula, in which x and y are replaced with x' and y'. Note that Q(x,y) is simply replaced by $(\forall u)(\exists v)(P)\psi$.

$\neg \Phi$ then becomes

$\neg ((\forall x')(\exists y')(\forall u)(\exists v)(P)\psi (x,y|x',y')\wedge (\forall x)(\forall y)((\forall u)(\exists v)(P)\psi \rightarrow (\forall u)(\exists v)(P)\psi ))$

and this formula is provable; since the part under negation and after the $\wedge$ sign is obviously provable, and the part under negation and before the $\wedge$ sign is obviously φ, just with x and y replaced by x' and y', we see that $\neg \phi$ is provable, and φ is refutable. We have proved that φ is either satisfiable or refutable, and this concludes the proof of the Lemma.

Notice that we could not have used $(\forall u)(\exists v)(P)\psi (x,y|x',y')$ instead of Q(x',y') from the beginning, because $\Psi$ would not have been a well-formed formula in that case. This is why we cannot naively use the argument appearing at the comment which precedes the proof.

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. φ cannot be of degree 0, since formulas in R have no free variables and don't use constant symbols. So the formula φ has the general form:

$(\forall x_{1}...x_{k})(\exists y_{1}...y_{m})\phi (x_{1}...x_{k},y_{1}...y_{m})$

Now we define an ordering of the k-tuples of natural numbers as follows: $(x_{1}...x_{k})<(y_{1}...y_{k})$ should hold if either $\Sigma _{k}(x_{1}...x_{k})<\Sigma _{k}(y_{1}...y_{k})$, or $\Sigma _{k}(x_{1}...x_{k})=\Sigma _{k}(y_{1}...y_{k})$, and $(x_{1}...x_{k})$ precedes $(y_{1}...y_{k})$ in lexicographic order. [Here $\Sigma _{k}(x_{1}...x_{k})$ denotes the sum of the terms of the tuple.] Denote the nth tuple in this order by $(a_{1}^{n}...a_{k}^{n})$.

Set the formula $B_{n}$ as $\phi (z_{a_{1}^{n}}...z_{a_{k}^{n}},z_{(n-1)m+2},z_{(n-1)m+3}...z_{nm+1})$. Then put $D_{n}$ as

$(\exists z_{1}...z_{nm+1})(B_{1}\wedge B_{2}...\wedge B_{n})$

Lemma: For every n, $\phi \rightarrow D_{n}$.

Proof: By induction on n; we have $D_{k}\equiv D_{k-1}\wedge (\exists z_{1}...z_{nm+1})B_{n}\equiv D_{k-1}\wedge (\exists z_{a_{1}^{n}}...z_{a_{k}^{n}})(\exists y_{1}...y_{m})\phi (z_{a_{1}^{n}}...z_{a_{k}^{n}},y_{1}...y_{m})$, where the latter equivalence holds by variable substitution, since the ordering of the tuples is such that $(\forall k)({a_{1}^{n}}...{a_{k}^{n}})<(n-1)m+2$. Each conjunct here obviously follows from φ.

For the base case, $D_{1}\equiv (\exists z_{1}...z_{m+1})\phi (z_{a_{1}^{1}}...z_{a_{k}^{1}},z_{2},z_{3}...z_{m+1})\equiv (\exists z_{1}...z_{m+1})\phi (z_{1}...z_{1},z_{2},z_{3}...z_{m+1})$ is obviously a corollary of φ as well. So the Lemma is proven.

Now if $D_{n}$ is refutable for some n, it follows that φ is refutable. On the other hand, suppose that $D_{n}$ is not refutable for any n. Then for each n there is some way of assigning truth values to the distinct subpropositions $E_{h}$ (ordered by their first appearance in $D_{n}$; "distinct" here means either distinct predicates, or distinct bound variables) in $B_{k}$, such that $B_{k}$ will be true when each proposition is evaluated in this fashion. This follows from the completeness of the underlying propositional logic.

We will now show that there is such an assignment of truth values to $E_{h}$, so that all $D_{n}$ will be true: The $E_{h}$ appear in the same order in every $D_{n}$; we will inductively define a general assignment to them by a sort of "majority vote": Since there are infinitely many assignments affecting $E_{1}$, either infinitely many make $E_{1}$ true, or infinitely many make it false and only finitely many make it true. In the former case, we choose $E_{1}$ to be true in general; in the latter we take it to be false in general. Then from the infinitely many n for which $E_{1}throughE_{h-1}$ are assigned the same truth value as in the general assignment, we pick a general assignment to $E_{h}$ in the same fashion.

This general assignment must lead to every one of the $B_{k}$ and $D_{k}$ being true, since if one of the $B_{k}$ were false under the general assignment, $D_{n}$ would also be false for every n > k. But this contradicts the fact that for the finite collection of general $E_{h}$ assignments appearing in $D_{k}$, there are infinitely many n where the assignment making $D_{n}$ true matches the general assignment.

Now from this general assignment which makes all of the $D_{k}$ true, we construct an interpretation of the language's predicates which makes φ true. The universe of the model will be the natural numbers. Each i-ary predicate $\Psi$ should be true of the naturals $(u_{1}...u_{i})$ precisely when the proposition $\Psi (z_{u_{1}}...z_{u_{i}})$ is either true in the general assignment, or not assigned by it (because it never appears in any of the $D_{k}$).

In this model, each of the formulas $(\exists y_{1}...y_{m})\phi (a_{1}^{n}...a_{k}^{n},y_{1}...y_{m})$, is true by construction. But this implies that φ itself is true in the model, since the $a^{n}$ range over all possible k-tuples of natural numbers. So φ is satisfiable, and we are done.

Intuitive explanation

We may write each B_i as Φ(x₁...x_k,y₁...y_m) for some x-s which we may call "first arguments" and y-s which we may call "last arguments".

Take B₁ for example. Its "last arguments" are z₂,z₃...z_m+1, and for every possible combination of k of these variables there is some j so that they appear as "first arguments" in B_j. Thus for large enough n₁, D_n1 has the property that the "last arguments" of B₁ appear, in every possible combinations of k of them, as "first arguments" in other B_j-s within D_n. For every B_i there is a D_ni with the corresponding property.

Therefore in a model which satisfies all the D_n-s, there are objects corresponding to z₁, z₂... and each combination of k of these appear as "first arguments" in some B_j, meaning that for every k of these objects z_p1...z_pk there are z_q1...z_qm which makes Φ(z_p1...z_pk,z_q1...z_qm) satisfied. By taking a submodel which contains only these z₁, z₂... objects, we have a model satisfying φ.

Gödel's incompleteness theorems

First Theorem: For any consistent formal, computably enumerable theory that proves basic arithmetical truths, an arithmetical statement that is true, but not provable in the theory, can be constructed. That is, any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete.

Second Theorem: For any formal recursively enumerable (i.e. effectively generated) theory T including basic arithmetical truths and also certain truths about formal provability, T includes a statement of its own consistency if and only if T is inconsistent.

Modern Proof

Assuming that a computer exists, and that formal logic can be represented as a computer program, it is easy to prove Gödel's incompleteness theorem from basic lemmas in computer science.

1. The Quine lemma—any computer program can include a subroutine that prints out the entire program's code. This allows any program to write itself into a string variable, or a large enough bigint.

proof: Let the printing subroutine be a standard quine, with additional data that contains all the rest of the code.

2. The Halting lemma: There does not exist a computer program PREDICT(P) which takes the code to program P and predicts whether P eventually halts.

proof: Write program SPITE, which prints itself into variable R, then calculates PREDICT(R). If the answer is R halts, Spite goes into an infinite loop. If the answer is R does not halt, SPITE halts. Since R is really SPITE in disguise, no matter what PREDICT says, the answer is wrong.

The incompleteness theorem: Suppose that an axiom system describes integers (or any other discrete structure), and that it has enough operations (addition and multiplication are sufficient) to describe the working of a computer. Then this system is either inconsistent or incomplete.

proof: Write DEDUCE to deduce all consequences of the axiom system. Let DEDUCE print its own code into the variable R, and search for the theorem R never halts, in the embedding of a computer inside the system. Only if DEDUCE finds this theorem does it halt.

If the axiom system proves that DEDUCE doesn't halt, it is inconsistent. If the system is consistent, DEDUCE doesn't halt and the axioms cannot prove it.

This argument doesn't explicitly demonstrate the incompleteness, because a consistent axiom system could still prove the $\omega$-inconsistent theorem that DEDUCE halts (even though it doesn't) without contradiction.

So write ROSSER: ROSSER prints its code into R, and searches deductions for either 1. R prints something out or 2. R never prints anything out. If it finds 1, it halts without printing anything. If it finds 2, It prints "Hello World!" to the screen and halts.

If the axiom system is consistent, it cannot prove either ROSSER eventually prints something nor the negation ROSSER does not print anything. So whatever its conclusions about DEDUCE, the axiom system is incomplete.

To prove the second incompleteness theorem, note that the consistency of the axioms proves that DEDUCE does not halt, so the axiom system cannot prove its own consistency.