# Propositional Logic Theorems as Types in Idris

Suppose you have a function from `Int`

to `Char`

and an `Int`

and you need a `Char`

. How can you get one? In other words, how would you implement the function

Easy, just apply the function to the argument:

Okay, now suppose you have a function from `Int`

to `Char`

and a function from `Char`

to `String`

and an `Int`

. How can you get a `String`

? In other words, how can you implement

Easy again, just compose the calls to the functions:

Finally, suppose you have a function from `Int`

to `Char`

to `String`

and a function from `Int`

to `Char`

and an `Int`

. Again, how can you get a `String`

? In other words, how can you implement

This one is left for the reader.

You might notice that these functions seem to have an **algebraic** character, and don’t have anything to do with `Int`

, `Char`

, or `String`

in particular. That’s true, and so the signatures can be rewritten **generically** (the implementations can be left alone):

At this point you might look at these signatures and notice that they bear a striking similarity to certain theorems of **propositional logic**, namely modus ponens, hypothetical syllogism, and Frege’s theorem, respectively. If you thought this, then congratulations, you’ve just discovered the first part of the **Curry-Howard correspondence**. The “correspondence” is the **deep isomorphism** between **types and programs**, on the one hand, and **propositions and proofs** on the other. The first part of the correspondence has to do with **propositional logic** and was discovered by Curry in the 1930s. The second part has to do with **quantificational logic**, and was discovered by Howard several decades later. (We’ll ignore the second part for now.)

Here’s a theorem for joining inferences:

We can also prove **double negation introduction** (where `p -> Void`

^{1} stands in for *p → ⊥*, which is equivalent to *¬p*)^{2}:

What about **double negation elimination** (DNE)?

Not so fast! It turns out that the type systems used by languages like **Idris** and **Haskell** don’t correspond to **classical logic**, but rather to **intuitionistic logic**^{3}. Intuitionistic logic is like classical logic except that it doesn’t validate the **principle of the excluded middle** (PEM): *p ∨ ¬p*. That is, it’s not the case that for any proposition, either that proposition or its negation holds, and a double negative is *not* proof positive.

To see why someone might reject PEM, consider the following classic argument.

There are irrational numbersClaimaandbsuch thatais rational.^{b}

The number √2Proof^{(√2)}is either rational or it isn’t. If it is, leta = b = √2and we’re done. Otherwise, leta = √2and let^{(√2)}b = √2. Thena. Tada!^{b}= (√2^{(√2)})^{(√2)}= √2^{(√2 * √2)}= √2^{2}= √2 * √2 = 2

There’s something *off* about this proof. It says that numbers with some property exist, but it doesn’t give **witnesses**; without witnesses, the knowledge feels hollow. The critical point in the proof is this line: *The number √2 ^{(√2)} is either rational or it isn’t.* But this is an instance of PEM! So you might forbid reasoning with PEM in order to preclude proofs like this one.

^{4}

Anyway, our type system can’t prove PEM, or DNE, or any of a variety of other equivalent statements, like **Peirce’s law** or the or the **consensus theorem**:

On the other hand, it *is* possible to prove the double negation of any of them, or indeed of any classically valid proposition.^{5} Here, for instance, is the proof of the double negation of Peirce’s law:

It’s also possible to prove any of those statements given (an instance of) another. For instance, here’s a proof DNE implies PEM (taking PEM itself for *p* in DNE):

# Exercises

- Prove the double negations of PEM, DNE, and the consensus theorem.
- Prove that PEM, DNE, Peirce’s law, and the consensus theorem are equivalent. DNE -> PEM is already done, so there are eleven more implications to prove. Or you could prove them in a circle if that’s too much work.
- Prove contraposition (
`contraposition : (p -> q) -> (q -> Void) -> p -> Void`

). Can you prove its converse? - Prove the double negation of
`(a -> c) -> (b -> c) -> ((a -> b) -> b) -> c`

.

# Discussion Questions

- To what extent should nonconstructive reasoning be accepted?
- Does any of this types-as-propositions stuff have any bearing on writing real programs in the real world? Does it have any bearing on proving new theorems?

# Further Reading

# Footnotes

^{1} In Idris, `Void`

is a type with no constructors. It therefore has no instances, and is said to “uninhabited”.

^{2} Some sources make it sound like use *p → ⊥* for *¬ p* was an innovation of intuitionism, but *p → ⊥ .↔ ¬ p* is classically valid.

^{3} The name comes from *intuitionism*, a philosophy that has something to do with mathematics stemming from mental activity. Personally I could do without that historical baggage. *Constructive logic* would be a less loaded name, but I think it might already be used for something else.

^{4} Specifically, this means stipulating that a proof of a disjunction requires a proof of one of its disjuncts.

^{5} Classical logic proves all the theorems of intuitionistic logic and then some, so in one sense classical is the stronger logic. But since any classical theorem can be proved intuitionistically by adding a double negation, we might say that intuitionistic is the stronger logic. After all, if a theorem can’t be proved intuitionistically except with a double negation, then we know it doesn’t have a constructive proof.