Gödel's Completeness Theorem

Given a set of axioms, if φ\varphi is a consequence of those axioms, can this be proven? If so, logic is complete.

In the early 20th century, Gödel proved first-order logic is complete. It's not important to know what first-order logic is. Know this: "First-order logic has the expressive power for the formalization of virtually all of mathematics" (p. 17). And in turn, virtually all true mathematical statements can be shown to be true.

I've spent the past eighty days studying Gödel's completeness theorem. Starting every day with coffee and Mathematical Logic by Ebbinghaus, Flum, and Thomas. I've done most exercises of the first hundred pages and dreamed of S-interpretations, decidability, and other otherworldly terms of the trade.

I thought knowing the minutiae of Gödel's proof would make me wise. But remarkably, Gödel proves every consequence of a set of axioms (in first-order logic) is proveable, without revealing anything about how: given a statement, how to prove it.

To know every truth is provable and be none the wiser about how to prove a particular truth.

Along the way though I was introduced to sequent calculus: A formal way to write proofs. Unlike regular proofs, proofs written in sequent calculus omit no obvious truths, nor require intuition from the reader. These proofs are so simple and procedural they can be checked by a computer.

To prove Gödel's theorem, Mathematical Logic introduces a sequent calculus. Then, shows it is a contradiction for something to be a consequence of some axioms (in first-order logic) and not provable in the sequent calculus. Thus, every consequence of a set of axioms is provable in the sequent calculus.

In this essay I'll introduce sequent calculus, cumulating in a proof that if φ\varphi is a logical consequence of the axioms Γ\Gamma, and ψ\psi is also a logical consequence of Γ\Gamma, then φψ\varphi\land\psi (\land reads and) is a logical consequence of Γ\Gamma.

Sequent Calculus

A set is any aggregation of objects, called elements of the set. For example, {a,b,c,...,z}\{a,b,c,...,z\} is the set of letters. xSx\in S reads, xx is an element of SS.

A formula is either true or untrue. If a formula φ\varphi is a consequence of a set of formulas Γ\Gamma, then Γφ\Gamma\varphi is a sequent. A sequent is a set of assumptions and a logical consequence of those assumptions. For example if aba\equiv b (\equiv reads equivalent) and bcb\equiv c are elements of Γ\Gamma, then Γac\Gamma a\equiv c is a sequent.

A sequent calculus consists of rules which generate sequents from other sequents. For example, provided \lor is the symbol for logical or, the rule

ΓφβΓψβΓ(φψ)β\begin{equation} \begin{array}{l l l} \Gamma &\varphi &\beta \\ \Gamma &\psi &\beta \\[0.3em] \hline\\[-1em] \Gamma &(\varphi\lor\psi) &\beta \\ \end{array} \end{equation}

reads: if β\beta is true whenver Γ\Gamma and φ\varphi are true. And if β\beta is true whenever Γ\Gamma and ψ\psi are true. Then, β\beta is true whenver Γ\Gamma and (φψ)(\varphi\lor\psi) is true. Notably, (1)(1) only admits true sequents.

More rules, justification for those rules, and a proof if φ\varphi and ψ\psi are consequences of Γ\Gamma then (φψ)(\varphi\land\psi) is a consequence of Γ\Gamma follows.

Antecedent Rule (Ant)

ΓΓ\Gamma\subseteq\Gamma' reads, all of the elements of Γ\Gamma are elements of Γ\Gamma'. Assuming φ\varphi is a logical consequence of the elements of Γ\Gamma and all the elements of Γ\Gamma are elements of Γ\Gamma', φ\varphi is a logical consequence of the elements of Γ\Gamma'. For example, φ=ac\varphi=a\equiv c is a consequence of Γ={ab,bc}\Gamma=\{a\equiv b, b\equiv c\}, so φ\varphi is also a consequence of Γ={ab,bc,zf}\Gamma'=\{a\equiv b, b\equiv c, z\equiv f\}.

This fact can be captured in our logical calculus as follows.

ΓφΓφ, if ΓΓ\begin{array}{l l r} \Gamma & &\varphi \\ \hline\\[-1em] \Gamma' & &\varphi \end{array} \quad\text{, if }\Gamma\subseteq\Gamma'

Assumption Rule (Assm)

Say φΓ\varphi\in\Gamma, then Γφ\Gamma\varphi is a valid sequent (it reads, assuming φ\varphi is one of the true formulas, φ\varphi is one of the true formulas). So we can add the following rule to our logical calculus.

Γφ, if φΓ\begin{array}{l l r} \hline\\[-1em] \Gamma & &\varphi \end{array} \quad\text{, if }\varphi\in\Gamma

Contradiction Rule (Ctr)

All formulas must be either true or untrue. ¬φ\neg\varphi reads, φ\varphi is not true. So, for a formula φ\varphi one of φ\varphi or ¬φ\neg\varphi is true.

Say we wanted to prove Melody did not eat the candy (φ\varphi). Here's one way. Suppose Melody ate the candy (¬φ\neg\varphi). If Melody ate the candy, then the seal would be broken (ψ\psi). But I checked, and the seal is not broken (¬ψ\neg\psi). So Melody did not eat the candy (φ\varphi).

Let Γ\Gamma denote the set of all true statements about the world. Because ¬ψ\neg\psi (the seal is not broken) is a true statement, ¬ψΓ\neg\psi\in\Gamma. So by the assumption rule, Γ¬ψ\Gamma\neg\psi is a valid sequent. Supposing ¬φ\neg\varphi (Melody ate the candy) is true, ¬φΓ\neg\varphi\in\Gamma, so by the antecedent rule Γ¬φ¬ψ\Gamma\neg\varphi\neg\psi is a valid sequent. Supposing ¬φ\neg\varphi is true, ψ\psi (the seal is broken) is true, so Γ¬φψ\Gamma\neg\varphi\psi is also valid sequent. However, because all formulas must be either true or false, and when ¬φ\neg\varphi is true ψ\psi and ¬ψ\neg\psi are true, ¬φ\neg\varphi cannot be true, so φ\varphi (Melody did not eat the candy) must be true, so Γφ\Gamma\varphi a valid sequent.

This style of proof is called proof-by-contradiction and can be denoted like this in our sequent calculus.

Γ¬φ¬ψΓ¬φ¬ψΓ¬φ\begin{array}{l l l} \Gamma &\neg\varphi &\phantom{\neg}\psi \\ \Gamma &\neg\varphi &\neg\psi \\[0.3em] \hline\\[-1em] \Gamma & &\phantom{\neg}\varphi \end{array}

Contraposition Rule (Cp)

Γ¬φ¬ψΓ¬ψ¬φ\begin{array}{l l l} \Gamma &\phantom{\neg}\varphi &\phantom{\neg}\psi \\[0.3em] \hline\\[-1em] \Gamma &\neg\psi &\neg\varphi \\ \end{array}

Rather than argue for this rule's correctness expositionally, we now have enough rules to write a formal proof. Starting from the premise, we show there is a sequence of rules which when applied produce the target sequent. Because our sequent rules only produce true sequents, we know our target sequent is true.


1.Γφψ(Premise)2.Γ¬ψφψ(Ant applied to 1.)3.Γ¬ψφ¬ψ(Assm)4.Γ¬ψ¬φ(Ctr applied to 2. and 3.)\begin{aligned} 1.\quad\Gamma\quad &\varphi\quad\psi &(\text{Premise}) \\ 2.\quad\Gamma\quad &\neg\psi\quad\varphi\quad\psi &(\text{Ant applied to 1.}) \\ 3.\quad\Gamma\quad &\neg\psi\quad\varphi\quad\neg\psi &(\text{Assm}) \\ 4.\quad\Gamma\quad &\neg\psi\quad\neg\varphi &(\text{Ctr applied to 2. and 3.}) \\ \end{aligned}

Chain Rule (Ch)

ΓφΓφψΓψ\begin{array}{l l l} \Gamma &\varphi & \\ \Gamma &\varphi &\psi \\[0.3em] \hline\\[-1em] \Gamma & &\psi \\ \end{array}


1.Γφ(Premise)2.Γφψ(Premise)3.Γ¬ψ¬φ(Cp applied to 2.)4.Γ¬ψφ(Ant applied to 1.)5.Γψ(Ctr applied to 3. and 4.)\begin{aligned} 1.\quad\Gamma\quad &\varphi \quad &(\text{Premise}) \\ 2.\quad\Gamma\quad &\varphi\quad\psi \quad &(\text{Premise}) \\ 3.\quad\Gamma\quad &\neg\psi\quad\neg\varphi \quad &(\text{Cp applied to 2.}) \\ 4.\quad\Gamma\quad &\neg\psi\quad\varphi \quad &(\text{Ant applied to 1.}) \\ 5.\quad\Gamma\quad &\psi &(\text{Ctr applied to 3. and 4.}) \end{aligned}

Logical And

ΓφΓψΓ(φψ)\begin{array}{l l r} \Gamma & &\varphi \\ \Gamma & &\psi \\[0.3em] \hline\\[-1em] \Gamma & &(\varphi\land\psi) \end{array}


1.Γφ(Premise)2.Γψ(Premise)3.Γφψ(Ant applied to 2.)4.Γ¬ψ¬φ(Cp applied to 3.)5.Γ¬φ¬φ(Assm)6.Γ(¬ψ¬φ)¬φ((1) applied to 4. and 5.)7.Γφ¬(¬ψ¬φ)(Cp applied to 6.)8.Γφ¬(¬ψ¬φ)(Ch applied to 1. and 7.)\begin{aligned} 1.\quad\Gamma\quad &\varphi \quad &(\text{Premise}) \\ 2.\quad\Gamma\quad &\psi \quad &(\text{Premise}) \\ 3.\quad\Gamma\quad &\varphi\quad\psi \quad &(\text{Ant applied to 2.}) \\ 4.\quad\Gamma\quad &\neg\psi\quad\neg\varphi \quad &(\text{Cp applied to 3.}) \\ 5.\quad\Gamma\quad &\neg\varphi\quad\neg\varphi \quad &(\text{Assm}) \\ 6.\quad\Gamma\quad &(\neg\psi\lor\neg\varphi)\quad\neg\varphi \quad &((1)\text{ applied to 4. and 5.}) \\ 7.\quad\Gamma\quad &\varphi\quad\neg(\neg\psi\lor\neg\varphi) \quad &(\text{Cp applied to 6.}) \\ 8.\quad\Gamma\quad &\phantom{\varphi}\quad\neg(\neg\psi\lor\neg\varphi) \quad &(\text{Ch applied to 1. and 7.}) \\ \end{aligned}

This concludes the proof as ψφ\psi\land\varphi is logically equivalent to ¬(¬ψ¬φ)\neg(\neg\psi\lor\neg\varphi).

What Gödel's Completeness Theorem shows, approximately, is all proofs can be done with a sequent calculus like the one introduced here. This blog's previous exposition about division, clock syncronization and distributed consensus could be replaced by a proof in the sequent calculus and a computer could check each step was performed correctly. This is the principle on which automated theorem provers like Lean are based.

If you'd like to explore this topic more, I recommend Mathematical Logic. I've written up solutions to some of my favorite problems in the book here.

Thanks Ally, Janita, Moses, Nick, Noah, Pete, and Tonya for interesting conversation.