My Journey to Build a Paradox: Implementing Gödel's Incompleteness in Swift

Some ideas in science and mathematics are so profound they change the way you see the world. For me, Kurt Gödel's First Incompleteness Theorem is one of those ideas. It's a statement about the absolute limits of logic and reason, a beautiful, paradoxical truth that says any powerful system of logic will inevitably contain statements that are true but can never be proven within that system.

For years, this concept fascinated and eluded me. This is the story of that project—a journey to translate one of the most abstract theorems in history into working Swift code.

---

The Winding Path to a Locked Room

My journey didn't start with Gödel. In fact, it started with a very practical interest in functional programming. Writing cleaner, more predictable code led me down the rabbit hole of Type Theory, the mathematical foundation for languages like Haskell and Swift. I was captivated by the idea that a program's type could be a proof of its correctness.

This led me to Gentzen's Proof Theory, where I started to see proofs not as static walls of text but as dynamic, structured objects that could be manipulated and reasoned about. With every step, I was unknowingly gathering the tools I needed to tackle the big one.

Every path seemed to lead back to Gödel.

I was reminded of a book on his proof I had bought over a decade ago. On my first attempt to read it, I admit I understood almost nothing. It was a dense, impenetrable wall of symbols. But this time, after my detour through types and proofs, something clicked. The symbols weren't just abstract logic anymore; they were components of a system. And systems can be built.

This project is the result of that "aha!" moment—an attempt to demystify the theorem by building its machinery from the ground up.

---

The Blueprint: How Do You "Build" a Theorem?

Before diving into code, we need to understand the core concepts we're trying to model.

1. Formal Systems: A Game of Logic

Imagine a simple board game. You have:

• Axioms: The starting positions of your pieces. These are statements you accept as true without proof (e.g., "0 = 0").

• Rules of Inference: The legal moves you can make (e.g., if you have statements A and "A implies B", you can derive B).

• Theorems: All the possible board states you can reach from your starting position using only legal moves.

A formal system is just this game of logic. The goal of the system is to generate all possible true theorems. Gödel's theorem asks: is it possible for a system to generate all true statements about numbers? His answer was a resounding no.

2. Gödel Numbering: Turning Logic into Math

Gödel's central genius was to find a way to make a formal system talk about itself. He did this by assigning a unique number (a Gödel Number) to every symbol, formula, and proof.

For this project, I assigned a number to each symbol in our simple logical language: ~ is 1, ∨ is 2, ( is 8, x is 11, and so on. A formula is a sequence of these numbers. To get a single unique number for a whole formula, we use prime factorization:

The formula s1, s2, s3, ... becomes 2^{g(s1)} x 3^{g(s2)} x 5^{g(s3)} x ...

Suddenly, statements about logic become statements about numbers. "This formula is a theorem" becomes "This specific, massive number has a certain mathematical property."

---

The Technical Challenge: An Impossible Number

A central challenge in implementing Gödel's proof is representing the "Gödel numbers" themselves. Let's take a simple 10-symbol formula from the project: (∃x)(x=sy). While it looks small, its Gödel number is anything but. Through logarithmic calculation, we can determine that its value requires approximately 287 bits (or 36 bytes) of storage.

For perspective, a standard 64-bit integer (UInt64), the largest in many languages, offers only 64 bits (8 bytes). Our number isn't just a little bigger; it's more than four times the size and represents a value so vast it's in a completely different universe of magnitude. And this is for a trivial formula. A real proof would require thousands or millions of bits, making it computationally impossible to store these numbers directly.

So, how do you work with a number you can't compute? You work on it symbolically. For this, I used a library I had previously built called ExpressionTree. Instead of calculating the final number, ExpressionTree represents it as a tree of its prime factors. For example, $2^8 x 3^4$ is stored like this:

* (^ 2 8) (^ 3 4)

This allows the program to reason about these immense numbers, compare them, and—most importantly—perform substitutions on them without ever needing to compute their final value.

---

A Walk Through the Code

The project's structure directly mirrors the concepts above.

• Proposition.swift: This is the alphabet of our formal language. It defines each logical symbol and assigns it a Gödel number.

• GodelNumbering.swift: This is our universal translator. It takes a formula string, converts it into a sequence of Gödel numbers, and then encodes that sequence into an ExpressionTree.

• GStatement.swift: The protagonist of our story. This struct represents the famous self-referential Gödel sentence, "G." Its one job is to enact the self-reference that creates the paradox.

---

The Climax: A Paradox in a Unit Test

The entire logical argument of the theorem comes to life in a single unit test: test_provable_leads_to_contradiction(). Let's walk through it.

Step 1: The Template (G)

First, we define our Gödel sentence, G. At this stage, it's just a template. It contains a placeholder variable, y, and it informally says:

"The formula you get by substituting y in the formula with Gödel number y is not provable."

Step 2: The Self-Reference (G(g))

This is the moment of magic. We perform a substitution on G, but we substitute the placeholder y with the Gödel number of G itself.

The formula is no longer a template. It's a concrete statement that now says:

"This very statement is not provable."

Step 3: The "What If" Scenario

Now we test the limits of our system. We ask, "What if our formal system was powerful enough to prove this statement?" We simulate this by creating a Proof object where our self-referential statement is manually added to the list of official theorems.

Step 4: The Contradiction

The final line of the test asserts that GStatement.isProvable() should be true. And it is—because we put the proof in ourselves. But think about what we've just done.

Our system has successfully proven a statement that is explicitly defined as being "not provable." It has proven a falsehood. This is a fundamental contradiction, meaning any system capable of this feat is logically inconsistent.

And what if the test had failed? That would mean our system is consistent... but it would also mean it failed to prove a statement that we know to be true (the Gödel sentence itself). That would make the system incomplete.

This is the dilemma. Consistent or Complete. You can't have both.

---

Conclusion: The Beauty of Limits

Gödel's theorem is often seen as a pessimistic result—a statement about what we can never know. But I see it differently. It's a beautiful map of the boundaries of formal reason. It shows that truth is a larger concept than provability.

For me, this project was the ultimate confirmation of a simple idea: the best way to understand a complex system is to build it. Going from an impenetrable book to a passing unit test transformed an abstract piece of mathematics into a tangible, working machine.