Now it's evident — totally!

In one of my posts about logics I have shown that a proof of a true proposition consists of constructing a function from ⊤ (truth) to an inhabitant of that proposition (interpreted as a type).

Dually, one would hope, we must construct a function between false propositions and ⊥ (bottom, the empty set).

The big question is: How? There appear to be many functions into the empty set. These surely cannot mean to be proofs!

There is a catch: totality. For every possible input we are obliged to provide a well-defined, deterministic result. A hard job when the target set is empty!

On the other hand it is easy enough for positive proofs: (considering the finite case...) say, we seek a proof of the Bool proposition. Bool has two inhabitants, so the function space from ⊤ (single inhabitant) to Bool must have 2¹ of them. Here is one:

provebool () = True

(Do you find the other one?)

But for negative proofs, it isn't really obvious how to do it. Since refutable propositions (allegedly) have no inhabitants, how do we write a pattern-matching function between them?

But remember, in the finite proof case our arrows had n^m inhabitants, picking any one of these constituted a valid proof.

For the uninhabited case such a way of counting gives us a clue: 0⁰ can be interpreted as 1! And this is the key, we need to do pattern matching with no patterns to get that inhabitant:

refutation = \case of {}

When this function is total, we have our sought-for unique proof. And for actual negative proofs it evidently is!