(This post is overdue; I’ve been more than usually busy at work on a new project, and have not had the energy to do anything interesting when I get home. Well, I saw this a while ago and today out of the blue remembered something interesting in relation to it. So I’ll start by posting about Logitext since it’s a pretty nicely made tool, and because the sequent calculus always deserves a bit of publicity.)
On Reddit some time ago, I saw Logitext. It’s a web-based sequent calculus explorer. It’s like a short text-book on the sequent calculus, with one special feature: the examples in it will change in response to input.
Like (I suppose) many computer scientists, I used to wonder: proving stuff is so hard and seems to require either miraculous leaps of intuition, or hopelessly intractable brute force searches over the set of proof derivations. How then am I supposed to write a program to do it?
The sequent calculus provides one answer: represent the proof as a tree, and define a few rules for growing branches until the tree is complete — in other words, until all the leaves of that tree are axioms. Start with the proposition to be proved as the unadorned root of a tree. Then, at each step, there are a finite number of rules that can be applied to grow the tree. (Wikipedia and the Logitext tutorial explain it better.)
A program that proves even simple theorems like
p -> (q -> p) can be a hard thing to implement naively. Having parsed the proposition into a term, where do you start proving it? In the sequent calculus, you parse it into the sequent
|= p -> (q -> p), and have a finite number of options on what to do next. One of which is the introduction rule for
->: move the
p into the antecedent, creating a branch
p |= q -> p. Performing it again grows to
p, q |= p. And finally, a structural rule lets us remove
q to finally grow a leaf: the axiom
p |= p.
This is represented as a tree (a trivial one with no branching, in this case):
One of the great properties of the LK system in sequent calculus is that it has the subformula property: all the terms needed to complete a proof are subterms of the initial proposition. So a program only needs to apply rules using those terms, and can be sure that it will find a proof if one exists.
I’ve forgotten a lot since I last studied it in… 2006, but some memories are coming back. We had an assignment to implement a theorem prover in Prolog, using the LJ and LK systems. It was remarkably easy, except for the feature for converting a proof, easily found with the sequent calculus, into a natural deduction proof. I have to confess I’ve not figured that part out yet…
- A tool for learning the lambda calculus
(a short presentation about my honours project on Simplifying Beta-reductions).
Few outside my supervisor and circle of reviewers must have known of the Lambda Calculus Explorer. I thought it was moderately original at the time, but I can only wonder how many other web-based formal system explorers there are out there.