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^{1}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

^{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!

## No comments:

Post a Comment