Real mathematics, part 1
Well, okay, propositional logic, but real proofs!
One of the early topics in some introduction to proof courses is logic, often starting with propositional logic. You may have noticed the example proof below (in propositional logic) on the documentation home page.
The rules are in the header
As discussed in the previous tutorial page, the mathematical system being used is hidden in the document header, so that it does not clutter up the document. But you can view it with the Document menu, and the first item, "Edit document header in new window."
Exercise: Read the logical rules
Take a look at how the rules for propositional logic are defined in Lurch, by viewing the document header as described above. You may notice:
- It begins by declaring some symbols. If this is unexpected, refer back to a page for instructors from earlier in this tutorial.
- Each rule of logic is an environment of type "Rule." That has several implications, including that Lurch will not check the reasoning inside of it, but just accept that all substitution instances of it are valid types of inference.
- Recall that only the content inside blue expression bubbles is used for checking reasoning, so a lot of the text in the header is just for expository purposes only, including the name of each rule, and the explanatory text connecting its premises to its conclusion.
- For rules that expect one to build a subproof before using them (e.g., the rule for conditional introduction), the rule contains an environment called a "Premise," which means that the user of the rule must build a subproof shaped like that environment in order to use the rule.
Theorems and proofs
Just as LaTeX contains theorem environments and proof environments, so does Lurch. And just as LaTeX theorem environments are where you place the statement of your theorem, and LaTeX proof environments are where you place the proof of your theorem, they function the same way in Lurch as well. If you examine the document above, which contains one theorem and its proof, you will see this pattern holds there.
Let's try constructing a new theorem-proof pair in the same document, below the one that's already there, and proving a new fact. Yes, let's prove your first theorem in Lurch!
Exercise: Create a theorem-proof pair
- Place your cursor at the very bottom of the document in the editor above. It will be inside the proof, just before its end.
- Press enter. Uh-oh! Lurch assumed you wanted to add new content inside the proof. That's not what we want.
- Use the Insert menu to add an "Empty paragraph below" the proof (or use the keyboard shortcut you find there).
- Now that we have space to insert a new theorem, use the Insert menu, choose Environment, and pick "theorem" from the list of options. Click OK.
- You should see a new, empty Theorem in your document. Leave it empty for now.
- Repeat the same steps as above to create an empty proof after your theorem. (You'll need to Insert > Empty paragraph below again.)
Tip: Use shortcuts
Just like in LaTeX, Lurch knows about some shortcuts, triggered by the
backslash (\
) key. For example, instead of using the Insert menu to add a
proof, you could type \proof
, and it would offer to insert one for you.
In fact, as soon as you type \p
, it's already offering to insert a proof,
and you can just press Enter to accept.
Stating a basic theorem
Exercise: A theorem without a proof
Try entering the following theorem into your empty Theorem environment: If \(X\text{ and }Y\) then \(Y\text{ or }Z\).
Warning
It is essential for you to mark the first expression as an assumption and the second as a statement! For a reminder on how to distinguish those two things, refer back to an earlier page in this tutorial.
What happens if you ask Lurch to check your work at this point? The theorem does not yet have a proof, but it gets a green check mark anyway! The reason is that this theorem is so obvious that Lurch can tell it's true just from trivial applications of the rules of logic, without the user's help.
This is actually a downside if you're teaching propositional logic! But don't worry. Future versions of Lurch will have customizable levels of helpfulness, so that the software doesn't do "too much" on the student's behalf. Right now, however, we have just one setting, and that's Lurch at maximal helpfulness.
What did we learn?
We learned how to state theorems and build empty proofs!
Let's move on to a theorem that's tricky enough we actually have to prove it..