Part Of: Computational Trinitarianism sequence
Content Summary: 1400 words, 14 min read

Ephemeral Proofs

You will be hard pressed to find a mathematician who affirms a theorem without proof. Indeed, mathematical texts are conscientious in pairing mathematical theorem with their proofs.

The tree-like nature of mathematics contributes to its beauty: theorems build on prior results. Theorems are permanent fixtures, solemnly passed from generation to generation.

But what of the proofs? After they convince their audience, they sort of… disappear. Bookmark this sense of confusion; we will return to it in a little while.

What Does Logic Mean?

Consider some proposition A. Most mathematicians would evaluate claims about A as follows:

• [A true] means “A is objectively true”
• [¬A true] means “A is objectively false”

This ontological interpretation of logic holds that logic encodes facts out there in the world.

But there is also an epistemic interpretation of logic. Consider what it means to interpret propositions as a reflection of our knowledge:

• [A true] means “I have a proof of A”
• [¬A true] means “I have a refutation of A”

This alternative interpretation of logic is also known as the BHK Interpretation.

Motivating Realizability

The above two interpretations of logic usually coexist fairly peacefully. But in one particular procedure, their differences make themselves known: proof by contradiction. The game goes like this:

• Conjecture: A is true.
• Proof: Suppose A is false. After exploring this possibility, an absurdity appears. Therefore, A is true.

Let’s get concrete. Here’s an example:

Conjecture: There exists some non-rational numbers a and b such that a^b is rational.

Proof: Suppose there are not two non-rational numbers such that a^b is rational. Consider two examples:

• Case A. { a = √2 , b = √2 }.
• Case B: { a = √2^√2 , b = √2 }.

It is a fact that √2 is irrational. So Case A contains two non-rational numbers. From our hypothesis we thus know that the output of case A, √2^√2 cannot be rational.

But if √2^√2 is non-rational, then Case B contains two non-rational numbers, and its output must also be non-rational.  But:

a^b = (√2^√2)^√2 = √2^(√2*√2) = √2^2 = 2

To say that 2 is non-rational is a contradiction. Therefore, the conjecture is proven.

Classical mathematics is perfectly content with this inference, that ¬¬A = A. But constructive mathematicians would complain that refuting ¬A is not the same as producing a proof of A. It takes considerable effort to show that prove A directly: to prove the non-rationality of some number, you must demonstrate bounds between it and every rational number at some margin.

This is why constructive mathematicians reject the principle of excluded middle, ¬¬A = A as incompatible with their epistemic view of logic. They argue that proof by contradiction desecrates the meaning of the existential quantifier. As Weyl put it in 1946, you have merely “informed the world that a treasure exists without disclosing its location”.

With the BHK Interpretation then, existence is constructive: whenever we claim an object exists, we must provide a way to construct it. This notion is known as realizability, and rejection of excluded middle is known as intuitionism.

The Birth Of Computer Science

It was later found that most of mathematics could be recovered using constructive principles. For example, there does exist a constructive proof that √2^√2 is non-rational.  For decades, there was little real progress (or even interaction) between these competing schools. We need to turn to a different field to understand what happens next.

In 1928, David Hilbert challenged the world to provide a procedure that could answer any statement  of first-order logic and answer “Yes” or “No”. This “decision problem” (in German, “Entscheidungsproblem“), in many ways prompted the invention of computer science. Hilbert’s problem was solved not once, but three times:

• In 1933, Kurt Godel wrote about General Recursive Functions.
• In 1936, Alonzo Church introduced his Simply Typed Lambda Calculus
• In 1936, Alan Turing invented his eponymous Machine

Perhaps dissatisfied with his late submission, Turing went on to show that these wildly divergent systems are, at some deep level, equivalent (“Turing complete”). This is a surprising result.

Computer science did not leverage the above three systems equally, despite their equivalence. Possibly due to its hardware-like aesthetic, the Turing Machine was the conceptual fuel that spawned computer architectures, on which programming languages were designed. But lately lambda calculus, with its “software-first” aesthetic, experienced a major revival.  Functional programming languages are based on Church’s system.

While General Recursive Functions are not viewed as particularly implementation-friendly, it is fair to say that the remaining two systems comprise the core of what is computer science:

bi-CCCs and the Curry-Howard Correspondence

So far, I have been weaving two separate stories: logical interpretation and history of computer science. Haskell Curry is the person who binds my narrative together. In 1958, he began noticing odd similarities between intuitionistic propositional logic (IPL) and the simply typed lambda calculus (STLC). Let me motivate one such similarity here. Both formal systems have operations that do work:

• In IPL it is useful to talk about implication (A → B). Implication is useful for encoding sentences like “If Socrates is a man, then he is mortal”.
• In STLC, it is useful to talk about “moving inside” a function; the moment when you inject the value of an argument into the content of a function. This operation is known as beta reduction.

These two operations were designed by specialists in different fields, with different motivations, notations, and style of exposition. Nevertheless, if you abstract away all of these all-too-human factors, and stare directly at the underlying formal systems, they begin to smell alike.

The “similar smell” was detected by Haskell Curry in the 1950s and William Howard in the 1960s. As the number of these correspondences increased, the ties between STLC and APL became known as the Curry-Howard Correspondence.

In the 1970s, Joachim Lambek used category theory to provide a fully formal account of this correspondence. It turns out that implication and beta reduction both share the same mathematical structure, and the shape of its construction is named the exponential.

The exponential is not the only shape shared between IPL and STLC. Other equivalences are now understood:

• Terminal object & Product
• Initial object & Coproduct
• Exponential

Formal systems that contain all five of these “shapes” are known as a bi-Cartesian Closed Category (bi-CCC)

Mathematics Is Computation

Don’t fully understand the above section? Good. Each of these equivalences should not “click” without an exploration of how STLC and IPL are implemented. That will come in due time. For now, I ask that you imagine a world in which the Curry-Howard Correspondence is true.

The Correspondence provides a bridge between mathematics and computation.

This bridge is very powerful. I opened this post complaining about the second-rate status of proofs in classical mathematics. But our bridge facilitates the following identification: Proofs are programs.

Let me repeat that! A mathematical proof is the exact same thing as a program. Every constructive proof ever created by a mathematician can be made into an algorithm. And every algorithm conceived by a software engineer is ultimately a proof of a mathematical fact.

In logic, proofs are employed as witness to the truth of theorems. Theorems are types. Type theory has been called the Grand Unified Theory of programming languages. The Curry-Howard correspondence provides us with a deep insight: just as a theorems motivate the shape of a proof, types specify the shape of its executing function.

Robert Harper coined the term computational trinitarianism to denote this inter-referential characteristic of type theory, proof theory, and category theory.

You don’t know what you’re talking about, until you understand the idea in all three theories. Once you have all three meanings, you have a genuine scientific discovery. It is permanent.

Takeaways

• There are two ways to interpret logic: as a description of the world, or a description of our knowledge
  •  The latter epistemic view of logic is known as the BHK interpretation
• The epistemic view of logic rejects excluded middle and holds that construction precedes existence claims.
  • This view of mathematical existence is known as realizability.
• Two inventions spawned computer science: the Turing Machine and the Simply Typed Lambda Calculus (STLC)
• STLC turns out to be equivalent to intuitionistic propositional logic!
  • This “bridge” is named the Curry-Howard Correspondence.
  • Category Theory crystallized the shape of the bridge as bi-Cartesian Closed Categories.
• The Curry-Howard Correspondence unifies mathematics and computation
  • Proofs are Programs, and Theorems are Types
  • Any mathematical proof can be translated into a program, and vice versa.