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 -> aOn 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.
Perhaps this automagical type insertion is the source of the barrier to understanding? If we wrote out the full natural deduction proof with all the intermediate steps explicit, would this be clearer? Well, here’s a sample natural deduction proof in tree format, from this lecture:
OK, that’s slightly easier to read, but good luck writing that. And the format would be completely unmanageable for a larger proof. How about tableau proofs? Not to be confused with analytic tableaux, which are a different concept, this is the classic multi-column format dreaded by many sufferers of introductory geometry and logic classes. Here’s a (slightly abridged!) sample from ProofWiki in this format:
| Line | Pool | Formula | Rule | Depends upon |
|---|---|---|---|---|
| 1 | 1 | \(p \wedge q\) | Assumption | (None) |
| 2 | 1 | \(\neg(\neg p \vee \neg q)\) | Sequent Introduction | De Morgan’s Laws: Conjunction: Formulation 1: Forward, 1 |
| 3 | \((p \wedge q) \Longrightarrow (\neg(\neg p \vee \neg q))\) | Rule of Implication | 1 - 2 | |
| 4 | 4 | \(\neg(\neg p \vee \neg q)\) | Assumption | (None) |
| 5 | 4 | \(p \wedge q\) | Sequent Introduction | De Morgan’s Laws: Conjunction: Formulation 1: Reverse, 4 |
| 6 | \((\neg(\neg p \vee \neg q)) \Longrightarrow (p \wedge q)\) | Rule of Implication | 4 - 5 | |
| 7 | \((\neg(\neg p \vee \neg q)) \Longleftrightarrow (p \wedge q)\) | Biconditional Introduction | 3, 6 |
… yeah. All that entire table did was prove that, if we have \(p \wedge q \vdash \neg(\neg p \vee \neg q)\) and \(\neg(\neg p \vee \neg q) \vdash p \wedge q\), then we have \(\vdash p \wedge q \Longleftrightarrow \neg(\neg p \vee \neg q)\). I’m not sure we’re really making progress here.
So, to sum up, existing formalized systems of propositional logic are almost always either horrendously unwieldy or unreadably compact. In a future post, I’ll cover existing formal proof systems for more sophisticated mathematics as well as discussing possible improvements, but I figured a survey of some of the available systems for simple logic and their flaws was a good place to start.
