In my last post, I gave an implementation for a program that searches through every proof in a particular proof notation for propositional logic, and collects all the theorems that it finds. The proof formalism used was Hindley–Milner, with types being the formulas of the theory and well-typed lambda terms the valid proofs (per the Curry–Howard correspondence).

The program’s output looked like this:

`\a. DoubleNegElim (\b. a) : forall a. False -> a`

On the right side of the colon, we have our type/theorem: for every proposition \(a\), \(\bot \rightarrow a\). The notation there is about as good as you’re going to get in ASCII text. But then we have the proof, on the left side of the colon. It’s an inscrutable lambda term encoding a natural deduction proof. The type inference engine is filling in the steps in the proof based only on which deductive rules were used, with the result that, even if you know how to read the notation, you really have to stare at it for a while to figure out why the proof *works*. While this admittedly lends an aura of elegance and mystery to the proceedings, I think I’d prefer a proof that is comprehensible by a human without significant head-scratching.

→ continue reading...