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$.

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

$\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)$ 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.

$\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.

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

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.

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

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}$

$\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.

Proof:

$\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}$

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

Proof:

$\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}$

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

Proof:

$\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.