What have we built so far? (part 2 of 2)
This post follows on part 1, which described various elements of the Lurch user experience. That post introduced the “bubbles” paradigm, which enables users to structure their documents however they like while retaining the ability to write mathematical statements and arguments with unambiguous meaning and structure.
Every Lurch user benefits from bubbles; you can’t use Lurch without them. But this post covers a part of Lurch generally seen only by instructors, not students.
There are no rules!
After installing Lurch, the blank document you see on first launch of the app is not really blank at all. It “depends on” a whole host of mathematical definitions, theorems, and rules of logic that are available for your use in that document. You can see this list if you go to the Meaning menu and choose “List all defined rules.” Lurch shows you a long list, the beginning of which is shown here.
These are just five of the over 100 rules Lurch knows. So why did I say, “There are no rules!?”
Because you don’t have to accept our rules! You can throw them all away and start from scratch if you like, or keep some and throw away others. Our team included many common rules of mathematics in Lurch our way, but you can rewrite them your way, or even invent a system of reasoning that has nothing to do with these rules.
We’ve had this design goal from the beginning. If you’re teaching a course on nonstandard logical systems, or the surreal numbers, or non-Euclidean geometries, you should be able to cast aside the normal rules and replace them with new ones. Let’s see how.
I make the rules!
In part 1, we saw how bubbles communicate meaning to Lurch. Each has a certain role, and you can click its tag to change that role–including specifying that the role is to define a new kind of rule. This blog post won’t go into great in detail, but eager rule-makers can dive into the Advanced Users’ Guide (which is also in Lurch‘s built-in help).
I give one example, from a document that ships with Lurch, that defines rules for propositional logic.
Here the user creates an outer bubble of type “if-then rule,” and uses an inner bubble to specify that a portion of the inside represents an assumption. Similar inner bubbles will mark “contradiction” as a required premise and “W” as a conclusion. A property bubble (also mentioned in part 1) can give the rule a name, and that’s it! Just having the rule in your document lets Lurch knows it. You can cite it later in your document and Lurch will use it to check the corresponding step of work.
All the rules built into Lurch were created this way! Instructors can even put their rules into a separate document so that students can cite them without having to explicitly rewrite each rule in their assignments. There’s more to it than in this simple example, but that’s the essence.
I hope this works!
It does! In fact, I’ll give you three good reasons to trust that it works.
First, Lurch has been tested in two semester-long courses, one in 2008 and one in 2013, and in both cases, only a few bugs were found, and they were fixed.
Second, the Lurch developers have an extensive test suite that they use to verify that the Lurch validation engine does what it’s supposed to do.
Third, the declaration and validation system is based partially on established mathematical research (thanks, Dan!), and comes with a theorem of its own that the design of our system accomplishes correct validation of users’ documents.