Lurch Design and Theory$^*$

How Lurch works its magic

Introduction

You can use Lurch to check proofs without understanding how it is able to do so. For those of you who want to understand Lurch at a deeper level (or are just curious), here is a very brief high-level overview of how it works.$^{**}$

We answer the question "How does it work?" from three different perspectives: for mathematicians, logicians, and computer scientists.

In what follows we assume you have already read and understand the material in the Quick Start Guides and Writing Proofs worksheet.

Lurch Theory for Mathematicians

If you look at the example proofs in Lurch, one striking feature you may notice is that it does not require that you justify your claims with reasons or explain how you came to any particular conclusion. So how does it determine if your proof is valid?

In simple terms, it begins by considering each statement in your document one at a time and asking "What do we know about this statement?". To answer that question it looks at every definition, theorem, axiom, rule, and formula in the context or document content and checks each one to see if it has anything to say about the particular statement. Whenever it does, it adds the relevant fact to the list of known information. Finally, when all such facts have been determined and collected, it checks if your conclusions follow from the list of known facts.

Example

Suppose a Lurch document contains only the following (and no context).

Gina's Coffee Shop Analysis

Declare is, loves to be constants, and suppose the following is true for any $x, y, z$.

Trivia: If $x$ is $y$, and $z$ loves $y$ then $z$ loves $x$

Now let's assume Gina loves chocolate, and mocha is chocolate. It immediately follows that Gina loves mocha and mocha is chocolate.

Lurch will exhaustively determine all of the facts it can obtain from the rule that involve the three statements Gina loves chocolate, mocha is chocolate, and Gina loves mocha, and replaces the rule with the facts it finds to obtain:

Gina's Coffee Shop Analysis

Declare is, loves to be constants.

Trivia Fact 1: If chocolate is chocolate, and Gina loves chocolate then Gina loves chocolate

Trivia Fact 2: If chocolate is mocha, and Gina loves mocha then Gina loves chocolate

Trivia Fact 3: If mocha is chocolate, and Gina loves chocolate then Gina loves mocha

Trivia Fact 4: If mocha is mocha, and Gina loves mocha then Gina loves mocha

Now let's assume Gina loves chocolate, and mocha is chocolate. It immediately follows that Gina loves mocha and mocha is chocolate.

(Admittedly, not all facts it finds are useful!)

Finally, Lurch marks the document and its claims as valid, as all of the claims logically follow from the assumptions and the facts it discovered.

To convince Lurch, a proof must include sufficient detail to validate each claim. In practice, the only way to convince Lurch that a non-trivial proof correct is if you already know why you are entering each statement. If students only consider one rule at a time to motivate each claim in their proof, then Lurch will find the relevant facts and judge the proof to be valid. But if they skip steps (or have an incorrect proof) Lurch will not be convinced by their argument until they provide more detail and/or correct their mistakes. In this way, students are trained by Lurch to have a justification for every step without explicitly requiring them to do so (just like most proofs in textbooks).

Lurch Theory for Logicians

The goal of Lurch is to be as natural, easy to use, and customizable as possible. Existing proof verification methods and foundations mathematics in the literature (e.g., Formal Axiom Systems, ZFC, Type Theory, Category Theory) are not particularly well-suited for that purpose. This motivates a different approach that is used by Lurch, which we now briefly explain.

A Magic Trick

Think of a topic. Any topic. Don't tell me what it is. Don't even tell me what you think the word 'topic' means. The only requirement is that your topic must have theorems. In fact, don't tell me what you think a 'theorem' is. Without knowing what your topic is, or what you think a theorem is, I will now tell you a true fact about the theorems of your topic:

Either Gina loves mocha is a theorem of your topic, or Gina loves mocha is not a theorem of your topic.

This is true about your topic because it's a tautology, and thus true by definition. In general, any propositional tautology whose atomic propositions are of the form '$t_0$ is a theorem of your topic', '$t_1$ is a theorem of your topic', '$t_2$ is a theorem of your topic', $\ldots$ '$t_n$ is a theorem of your topic' will be true about the theorems in whatever topic you might be considering.

How does this help?

No Formal Language – Modern Foundations of Mathematics like ZFC, Type Theory, Category Theory, frequently begin by defining a language - the set of syntactically valid statements in the mathematical topic that they are trying to formalize. Lurch's foundation does not make any such restriction. You can define and say whatever you want.
No Context ‐ Lurch does not assume any mathematical or logical rules by default, so instructors and users are free to define their own from scratch. Proofs in undergraduate math textbooks rarely used formal operators like $\Rightarrow$, $\wedge$, $\forall$, or $\exists$. Lurch can validate such proofs because it also does not require them (or any other formal operator).
Propositional Form – Lurch converts your entire document (context, assumptions, theorems and proofs ... all of your meaningful content) to a single proposition, and checks if that proposition is a tautology. You do not have to learn any Lurch-specific rules or reasoning. Yet doing proofs in Lurch 'feels' very natural, as illustrated by the following example.

Example

Suppose we have the following Lurch document with no additional context or content.

Suppose mocha is chocolate. Additionally, assume the following Fun Fact:

Trivia: If mocha is chocolate then Gina loves mocha.

Then we can conclude that Gina loves mocha and also that mocha is chocolate.

Let $P=$ 'mocha is chocolate' and $Q=$ 'Gina loves mocha'. Then this document has propositional form $(\neg P \vee (\neg( \neg P \vee Q ) \vee (Q \wedge P)) )^*$ which is a tautology. So Lurch indicates that the document is valid.

$^*$Equivalently $(P\text{ and } (P \Rightarrow Q )) \Rightarrow (Q \text{ and } P)$

(Meta-)True about Everything – As the magic trick above illustrates, the proposition that Lurch actually evaluates is true about whatever topic or model you might be considering. This has some nice implications for context design and development.

Recall that any theorem in Neutral Geometry is true about both the Euclidean plane and the hyperbolic plane. Neither Euclid's parallel postulate $E$ nor its negation $\neg E$ can be proven in Neutral geometry, and either one can be added as an additional axiom without introducing a contradiction. Goedel's Theorem generalizes this situation by showing that for any sufficiently complicated consistent formal system there will always be a statement, $G$, such that neither $G$ nor $\neg G$ can be proven using that system, and either can be added to the system without introducing a contradiction.

From the perspective of the foundation used by Lurch, these results simply say that we can always extend our context to prove results about things that are independent of the context (unless the context allows you to prove everything - the Lurch flavor of 'inconsistent'). This is due to the fact that Lurch does not restrict to a particular formal language or assume any context by default. It allows you to start with any context, spotting whatever high level facts you like, as an alternative to requiring that every proof be built up from very low-level axioms.

To illustrate this, consider the following example.

Example

Suppose we have a Lurch document with only these three rules (and the definition of $=$ via the Equations Rule), and we declare $+,\cdot,=,0,\text{is},$ and $\text{linear}$ to be constants.

Additive Identity (one sided): $x+0=x$

Multiplication by Zero (one sided): $0\cdot x=0$

Definition of Linear: If $f$ is linear then $f(a\cdot x+b\cdot y)=a\cdot f(x)+b\cdot f(y)$.

Whatever topic you might be considering, in this context the following proof and theorem will be valid.

Theorem (linear maps preserve zero): If $g$ is linear then $g(0)=0$.

Proof:

Assume $g$ is linear. Then

$$ \begin{aligned} g(0) &= g(0+0) \\ &= g(0\cdot 0+0) \\ &= g(0\cdot 0+0\cdot 0) \\ &= 0\cdot g(0)+0\cdot g(0) \\ &= 0\cdot g(0)+0 \\ &= 0\cdot g(0) \\ &= 0 \end{aligned} $$

So g(0)=0 as desired.

$\square$

Notice that this context does not define addition, multiplication, zero, the natural numbers, what a function is, or specify anything about whether $a,b,x,y$ are scalars, vectors, matrices, elements of a field, or a ring, or whether addition or multiplication are commutative. We have not specified any additional axioms about the natural numbers, set theory, rings, groups, or rules of logic.

This illustrates how Lurch allows us to create assignments that ask students to prove theorems with short proofs that focus on the main ideas by spotting them high-level definitions and theorems in the context, rather than forcing them to prove everything from the ground up from first principles in an axiomatic system. But there is nothing to prevent you from doing that as well!

Lurch Theory for Computer Scientists

Validation

Under the hood, Lurch validates your proof using what we call the Global $n$-compact algorithm. A brief overview of the algorithm is given in the talk slides in the first link. A more detailed description, the API documentation, and source code links are after that.

Validation in Lurch an introduction to the Global $n$-compact validation algorithm used in this version of Lurch (talk slides).
Validation Algorithm API docs the source code documentation for the Global $n$-compact algorithm and supporting infrastructure.
Core API docs the LC data structure, putdown notation, matching package, and other core utilties.
Official Lurch Source Code on GitHub the source code and content of this repository on GitHub.

Parsing

The Lurch web interface uses two parsers written using Peggy. One converts the user's input for meaningful expressions into the internal data structure used by the validation algorithm. The other converts it to the $\LaTeX$ source needed to render mathematics in the document.

Lurch Syntax a quick reference showing how to type various math expressions in Lurch.
Peggy LaTeX Parser Grammar this is the full Peggy source code for the tex parser.
Peggy Putdown Parser Grammar this is corresponding Peggy source code for the putdown parser.

$^*$Most of the original ideas and designs discussed on this page were motivated by the desire to make Lurch as natural and user friendly as possible. Existing proof verification methods and foundations mathematics in the literature (e.g., Formal Logic Systems, ZFC, Type Theory, Category Theory) are not well-suited for that purpose. Some aspects of the design are still a work in progress and subject to modification. I intend to write up the details once the dust settles. In the meantime, if you have questions or would like to discuss these ideas further, feel free to contact me.

$^{**}$It is not necessary to understand anything on this page in order to use Lurch. It is just how I think about it. I find that having some deeper way of thinking about it can be helpful when creating your own contexts and assignments.