An Interactive Tutorial of the Sequent Calculus
May 22, 2012You can view it here: An Interactive Tutorial of the Sequent Calculus. This is the “system in three languages” that I was referring to in this blog post. You can also use the system in a more open ended fashion from this page. Here’s the blurb:
This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic.
Developing this system has been quite a fascinating foray into user interface and game design. While similar systems have been built in the past, my goal was a little different: I wanted something simple enough and accessible enough that anyone with a vague interest in the topic could pick it up, work through it in an hour, and learn something interesting about formal logic. I don’t think this demo will be particularly successful among the math-phobic, but perhaps it will be more successful with people who have an intrinsic interest in this sort of thing. I must have incorporated dozens of comments from my many friends at MIT who put up with my repeated badgering about the system. The first version looked very different. I give my superlative thanks to my beta testers.
There is a lot of hubbub about the next generation of online teaching systems (edX), and this demo (because, really, that’s what it is) is intended to explore how to blur the line between textbooks and video games. It doesn’t really go far enough: it is still too much like a textbook, there is not enough creative latitude in the early exercises. I don’t feel like I have gotten the right feel that a video game which progressively layers concepts (e.g. Portal). On the other hand, I do feel I have done a good job of making the text skimmable, and there are a lot of little touches which I think do enhance the experience. I am embarrassed to admit that there are some features which are not included because they were technically too annoying to implement.
If there is one important design principle behind this demo, it is that there is a difference between giving a person a map and letting a person wander around in a city for a few hours. But, fair reader, you probably don’t have a few hours, and I am probably demanding too much of your attention. Nevertheless, forgive my impoliteness and please, take it out for a spin.
Looks really slick (if I overlook use of classical logic ;-D). It survived a little bit of gratuitous abuse by me, though responsiveness was getting noticeably bad by the end; I’m glad I didn’t try to add four to something!
I like the choice of forcing contraction on implication left, where you would otherwise have to explain how to split the whole context, but allowing contraction to be user-specified at the quantifiers; it seems like the obviously right choice UI-wise. The other choice would probably be to always force contraction on non-invertible rules, I suppose, but what you did probably leads to better-looking final sequent proofs (my proof was wide enough as it was).
That is pretty gratuitous :-) One reason for the slowdown is that there’s a bit of code which is written with the assumption that proof trees are pretty small; so they get traversed and re-traversed quite a bit. I don’t think there is any fundamental reason for this limitation, but you’re example is clearly not what I had in mind :-)
I think it’s the case that some treatments of sequent calculus have auto-contraction in implication left, so it’s not entirely my invention. I think there exists a good interface for moving the context between the two goals (click and drag a hypothesis to the other goal), but I was too lazy to code it up, and it’s nice not having to tell people what contraction is until later.
Fantastic! I love it.
Several comments:
An alternative to the modal quantifier box is to replace the quantified term with input fields, thus still allowing interactivity with other parts of the derivation.
OK, quantifier boxes work a /lot/ better now.
Slava: I’m not sure; the examples are supposed too look like real math, and I worked hard to make the illusion that it is an article :-)