Do Angels Dream of Recursive Symbol Systems?

(Evangelion Week, Day 5)

Let’s say you wanted to formalize Evangelion. Not the plot. The metaphysics. The pain, the self-loss, the divine recursion, the way the whole system collapses under the weight of trying to express meaning through structure.

You’d need something expressive.
You’d need something typed.
You’d need… dependent type theory.

Modeling Instrumentality in Type Theory

In Martin-Löf Type Theory, we don’t just have sets and elements—we have types that depend on terms, and terms that construct types. It’s recursive. Structured. Intimate.
You know what else is like that?
The Human Instrumentality Project.
Let’s define a type Human : Type
Now, define a function ATField : Human → Shield, where Shield is what separates self from Other.
It's the metaphysical membrane. The boundary that says, this is me, and that is not.

Instrumentality would then be modeled as:
                ∀ h : Human, ATField h = ⊥
In other words: for every human h, the shield collapses.
The boundary dissolves.
But then what?
Once the AT Field is gone—once individuality is erased—what do you return?
What’s the type of a merged consciousness?

• A dependent product over all selves?
• A Σ-type of every person we used to be, now bundled into one?
• A broken function?
• Or just ⊥—logical bottom? The place where meaning stops.

Gödel Shows Up!

Gödel’s incompleteness theorems say no system of logic can contain its own consistency proof. But in Evangelion, the system tries anyway. It tries to contain itself—Shinji’s grief, Rei’s multiplicity, Kaworu’s godhood. The system wants to close.

But it can’t. Because the axioms are haunted.

The moment Rei becomes all things and no thing, the moment Shinji tries to name a wish for humanity—he collapses the system. He introduces an unresolvable contradiction between self and unity, freedom and fusion.

There is no total function from Human → Meaning.
Only partial applications. Only errors.
Only proof trees that don’t terminate.

Recursive Collapse as Revelation

Type theory tries to keep things clean.
So does Evangelion.

But both fall apart—beautifully—when confronted with emotion, failure, and the impossibility of encoding grief.

What’s left is a trace.
A term.
A partially evaluated expression: Shinji : Person
Still trying to return something.
Still waiting for the next input.

Proof Assistants for When Your Soul Is a Functor

[1] Per Martin-Löf, Intuitionistic Type Theory
The origin point. Where types are proofs, terms are programs, and somewhere in between, you accidentally formalize your feelings.
[2] Philip Wadler, Propositions as Types
Short, beautiful, and suspiciously emotional for a CS paper. Explains how logic and computation mirror each other—like Rei and Lilith and also your deepest fears.
[3] Douglas Hofstadter, Gödel, Escher, Bach
Recursive selfhood, tangled loops, and formal systems that dream about themselves. Evangelion’s spiritual cousin in a tuxedo made of symbolic logic.
[4] Gian-Carlo Rota, Indiscrete Thoughts
Not formal, but brilliant. A meditation on math, failure, and the parts of proof that don’t show up in the final PDF. Like End of Evangelion, but in lecture form.
[5] Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics
For when your notion of identity breaks down and you realize equality is a path, not a fact. Warning: may induce existential recursion.