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.
Proving theorems is not for the mathematicians anymore: with theorem provers, it's now a job for the hacker. — Martin Rinard
I want to tell you about a neat system called the sequent calculus. It's a way of deducing whether or not a statement is true, but unlike proofs where the prover makes wild leaps of deduction from one statement to another, the sequent calculus always has a simple set of rules that is easy to check the validity of.
An ordinary software engineer rarely has any need for proof, even though he deals with the issues of truth and falsehood on a daily basis. His tool is boolean logic, where there are propositions, and they are either true or false, and even in the most complicated cases, the truth of a statement like "A or not A" can be checked by checking all of the possible cases using a truth table.
However, as a tool for describing the world, Boolean logic is inflexible. Suppose I claim "all men are mortal" and "Socrates is a man". I should then be able to deduce "Socrates is mortal"; however, in Boolean logic, these three propositions have no relationship with each other. Instead, I would like a way to say the word "all", a quantifier, is special in some sense. It deserves to be an operator like AND/OR/NOT, and have some meaning assigned to it.
However, now there's a problem: we can't figure out if a logical statement is true anymore by writing out the truth table. We can't check that a statement about "all" individuals is true by checking each individual one-by-one: there may be too many. We need another way of reasoning about these statements, which are called statements in first-order logic.
There are a lot of ways to think about first-order logic. In this tutorial, we'll focus on one fundamental way of dealing with statements. It will be a little unintuitive at times, but it will have the benefit of being precise, unambiguous and simple. It is so precise and simple we can program it into a computer. But it is also powerful enough to let us derive any true statement in first-order logic. You should come out of this tutorial with an appreciation of how to do the symbolic manipulation of the sequent calculus.
The sequent calculus operates by a set of rules, not all of which are intuitively obvious. Our goal is to learn the rules of the game, while at the same time becoming familiar with the notation and terminology which is conventionally used by mathematicians on pen and paper.
All of the examples in this document are interactive. Technical terms are underlined; you can mouse over them for a definition. You can reset your changes to an example by clicking the turnstile symbol (⊢).
Sequents and axioms. The turnstile is always included in a sequent, an example of which is displayed below. You can interact with it by clicking on the A, which are clauses. You can read the sequent as "A implies A": the turnstile can be thought of as a sort of implication. In this example, when you click on the A, a bar appears on top, which indicates the sequent is axiomatically true. The only axioms in this system are when some atomic clause appears on both sides of the turnstile. We're done when all sequents have bars over them.
Hypotheses on the left. Read the following sequent as "Γ and A imply A." If you click on A, you will successfully complete the proof, but if you click on Γ, you will fail (because it is not a conclusion you are proving.) Γ (a capital Greek gamma) conventionally indicates hypotheses which are not relevant.
Conclusions on the right. Read the following sequent as "A implies A or Δ". Δ (a capital Greek delta) conventionally indicates conclusions which are not relevant. Notice that the comma means conjunction on the left but disjunction on the right. One reason for this is that it makes it very easy to identify axiomatically true statements: if an atomic clause is on the left and on the right, then you're done.)
Backwards deduction. Up until now, clicking on a clause has either told us "this sequent is axiomatically true" (completing the proof) or given us an error. These make for very boring proofs: what about logical operators? When you click on a clause that contains a logical operator, the system generates one or more further goals, which you need to prove. It's its way of saying, "In order to show A ∨ B ⊢ A, B is true, you need to show A ⊢ A, B is true and B ⊢ A, B is true." Notice that in both of the subgoals, there no longer is a disjunction; in sequent calculus, we use backwards deduction to get rid of logical operators until we have atomic clauses.
Inference rules. Now, it is great that the computer has told you what new goals you need to prove, but what if you wanted to write out the proof by hand? You need to know what to write down. Fortunately, for each logical operator, there are exactly two inference rules which say what new goals are generated: one for when it's on the left side of the turnstile (hypothesis), and one when it's on the right (conclusion). You applied the rule for left-disjunction in the previous example: here is the rule written out in general.
The Γ and Δ are placeholders for other hypotheses and conclusions: in the previous example Γ was empty, and Δ was "A, B" (two clauses). The text on the right of the bar indicates what rule was applied: the first letter indicates the logical operator involved, and the second letter indicates left or right. Together, axioms and inference rules make up the entirety of our deductive system: they are all you need. We'll now go on a tour of all the inference rules in first-order logic.
Trivial rules. Recall that all of the hypotheses on the left side of the turnstile can be thought of as ANDed together, and the conclusions on the right side ORed together. Thus, if I have a hypothesis which is an AND, or a conclusion which is an OR, we can very easily get rid of the logical operator.
Meta-implication rule. The turnstile itself can be thought of as implication, so to prove A → B, I can assume A as a hypothesis and prove B instead ("moving" the clause to the left side of the turnstile.)
It's worth noting that, because this is classical logic, you can use any hypothesis generated this way for any other conclusion (a sort of "bait and switch"). It's worth taking some time to convince yourself why this is allowed, since it shows up in other inference rules too. Here is a simple example of this:
Branching rules. What about conjunction, disjunction and implication on the other side of the turnstile? All of these generate two new goals, both of which need to be proved.
Negation rules. Negation is a strange operator: applying its inference rule moves the un-negated clause to the other side of the turnstile.
Quantifier rules. The rules for the quantifiers are quite interesting. Which of these four statements is true?
You should only be able to prove two of the four: forall left (∀l) and exists right (∃r). In both cases, the system asks you for an individual to instantiate the variable with. This variable can be anything, including variables which already exist in the expression. Intuitively, it should make sense why these are the two true statements: in the case of forall, if I know something about all individuals, I know something about a particular individual too; in the case of exists, in order to show the existence of something, all you need to do is produce it. The "particular individual" and "the individual which exists" are precisely what the system asks you for.
In the case of the forall right (∀r) rule and the exists left (∃l), the system picks a variable for you. But it doesn't pick any old variable: the variable it picks is required to be distinct from anything pre-existing in the sequent: this is often referred to as the "no free occurrence" rule. One intuition for why the system is constrained in this way is to consider this: it is generally harder to prove something is true for all individuals than it is to show it is true for only one.
In practice, this means is that the order you apply tactics is important:
If you start off with the left-forall, when you apply the right-forall, the system will always give you something that doesn't match what you originally picked, and then you are stuck! But it is easy to complete in the other direction.
One last note: the "contraction" button duplicates a hypothesis or goal, so you can reuse it later (say, you want to say that because all people are mortal, then Bob is mortal, AND Sally is mortal). Use of this structural rule may be critical to certain proofs; you will get stuck otherwise. (This rule is somewhat paradoxically called contraction because when you read the rule in the normal top-down direction, it "contracts" two identical hypotheses into a single one.)
Summary. Here are all the inference rules for first order logic:
With these inference rules, you have the capability to prove everything in first-order logic.
Hint: these two require contraction.
I want to leave you with some parting words about why I find this topic interesting.
First-order logic is well worth studying, because it is a simple yet powerful tool for modelling the world and writing specifications and constraints. These constraints can be given to tools called SMT solvers, which can then automatically determine how to satisfy these constraints. You can't do that with plain English!
A common complaint with a formal systems like the sequent calculus is the "I clicked around and managed to prove this, but I'm not really sure what happened!" This is what Martin means by the hacker mentality: it is now possible for people to prove things, even when they don't know what they're doing. The computer will ensure that, in the end, they will have gotten it right. (You don't even have to test it, and there are no bugs! Of course, it does help to know what you are doing.) Writ large, working with this demo is like working with a proof assistant. If you're interested in tackling more complicated problems than presented here, I suggest checking out a textbook like Software Foundations.
One primary motivation for this tutorial, which constrained the user interface design considerably, was to demonstrate the notation and concepts relied upon heavily in the academic type theory literature. As an undergraduate, I always found inference rules to be some of the most intimidating parts of academic papers in programming languages. Studying how these conventions work in a simpler setting is a key step on the way to being able to "read the Greek." While some of the notational choices may seem hair-brained to a modern viewer, overall the system is very well optimized. Inference rules are a remarkably compact and efficient way to describe many types of systems: the space savings are analogous to using BNFs to specify grammars.
Overall, my hope is that this tutorial has helped you take your first step into the fascinating world of formal systems, type theory and theorem proving. Return to the main page, and try coming up with some theorems of your own!
Colophon. This tutorial is powered by Coq, Haskell and Ur/Web.