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\}$ is the set of letters. $x\in S$ reads, $x$ is an element of $S$.

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 $a\equiv b$ ($\equiv$ reads equivalent) and $b\equiv c$ are elements of $\Gamma$, then $\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

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)$ 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, $\varphi=a\equiv c$ is a consequence of $\Gamma=\{a\equiv b, b\equiv c\}$, so $\varphi$ is also a consequence of $\Gamma'=\{a\equiv b, b\equiv c, z\equiv f\}$.

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

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.

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.

Contraposition Rule (Cp)

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.

Proof:

Chain Rule (Ch)

Proof:

Logical And

Proof:

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.