(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…
Footnote. I played with Logitext earlier this year. But today — due to, perhaps, a cosmic ray — it suddenly occurred to me that it should look eerily familiar. After all, my own Lambda Calculus Explorer was the same thing: terms are presented as part of a web page, and clicking on parts of them will result in the creation of new terms. Tragically (or perhaps as a serendipitous reprieve for blog readers) I no longer have PHP and JavaScript code for it. But I did salvage these slides out of Gmail:
- 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.
EJRH 
Extracting an NJ proof from an LJ proof is pretty straightforward: NJ intro rules correspond clearly to LJ intro-right rules, NJ elimination rules to LJ intro-left rules.
LK is a bit different though. Consider the following LK derivation:
A => A
——-
=> A, -A
———
=> A v -A
It is not clear how to get a natural deduction proof out of this: you (probably) need to make use of a rule that deals with some instances of connectives to overcome the use of the multiple conclusions. But it is not nearly so clean as the LJ/NJ relationship.
You can easily construct a sequent calculus for classical proposition logic with (at most) one formula on the right. You will loose the subformula property, but you’ll get somethng just as good (probably sub-formulas of the formulas to the left of the sequent arrow, and sub-formulas of the double-negation of the formula to the right of the sequent arrow). And you will be able to read the NK proof off of the sequent derivation.
As you can imagine I’ve forgotten at least some of what I did in one paper in 2006, not to mention lost all my notes and all my work. I don’t recall whether NJ proofs were only required for LJ proofs, though it seems likely. I know I was having one of those tricky programming problems where behaviour X — something about how (un)discharged assumptions are generated as the LJ tree is grown — doesn’t occur as often as it should, and a hacky code change will fix that but make behaviour X happen when it shouldn’t. Of course, as a functional programmer you may be mystified by my use of the word “behaviour”, and even my occasional descriptions of a program using temporal concepts like “occur”, “happen”, “generated”, “often”, “to grow” or, in fact, almost any verb, since most verbs involve some kind of mutation.
All that notwithstanding, I think there was a cunning plan to use the antecedent as a place to store the un(discharged) assumptions on the way up the tree.
Anyway, thanks for the response. I’ll need to re-research a bit more before I can play with it though. You should take a look at Logitext in the meantime.
I cheerfully remind you that you still have my halfremembered ramblings on Epigram to look foward to.