Proof Maneuvers

On the last page, we discussed two key components of the structural backbone of a proof: a collection of assumptions, called hypotheses, from which we prove goals. We saw that, over the course of a proof, we update our context and goals by taking certain logical steps.

But if we want to be certain that the proofs we're producing are valid—and, of particular relevance to Lean, if we want a computer to be able to mechanically check that our proofs are valid—we'll need to specify precisely what such a "logical step" looks like and which ones we can use to create a logically admissible proof.

Connectives and Quantifiers

In order to specify our proof rules, we're going to need to be a bit more precise about the kinds of expressions that we allow in our context and goals. Previously, we used English sentences like "n is divisible by 2" or "there exists some integer c such that n = 2c." But Lean uses a more restricted, symbolic language amenable to checking by a computer. This language consists of the quantifiers and connectives that have been (and/or will be) discussed in lecture and in the course text. We provide a recap of them here:

• Conjunction ("and", ∧): P ∧ Q asserts that both P and Q are true
• Disjunction ("or", ∨): P ∨ Q asserts that at least one of P or Q is true
• Negation ("not", ¬): ¬P asserts that P is false
• Implication ("if…then…", →): P → Q asserts that if P is true, then Q must also be true
• Bi-implication ("if and only if", ↔): P ↔ Q asserts that P and Q are always true or false at the same time, and is equivalently the conjunction of P → Q and Q → P
• Existential quantification ("there exists"/"some", ∃): ∃ x, P x asserts that there exists some value x that makes P x true
• Universal quantification ("for all"/"every", ∀): ∀ x, P x asserts that every value x makes P x true

Introduction and Elimination Rules

We now define our proof rules by considering the intuitive behavior that each of the connectives and quantifiers we've listed ought to have.¹

We'll split our proof rules into two groups: introduction rules and elimination rules. Introduction rules tell us what we must do in order to prove a proposition involving a given connective or quantifier. For example, intuitively, in order to prove P ∧ Q, we need to prove P and we need to prove Q, since conjunction requires that both conjuncts be true. In contrast, in order to prove P ∨ Q, we only need to show one of the two sides to be true, since disjunction only requires that one disjunct be true. Since introduction rules tell us how to prove a proposition of a certain form, they're useful for reducing our goal to simpler propositions: for instance, on the last page, we implicitly appealed to the introduction rule for conjunction to split a goal with an "and" in it into two separate goals, following the same pattern we just laid out in our formal language above!

Elimination rules, on the other hand, are useful for "extracting information from" our hypotheses. Elimination rules tell us, given that we know a proposition involving a certain connective or quantifier to be true, what information we're allowed to directly conclude from that knowledge. For instance, if we know that P ∧ Q is true, then we can conclude that P is true and that Q is true, since conjunctions require both conjuncts to be true. Moreover, if we know that P → Q is true and also that P is true, then we must be able to conclude that Q is true, since the implication tells us that whenever P is true (which it is!), Q must be true as well.

We said earlier that the job of proof rules is to update our goals and contexts. Therefore, to state these proof rules precisely, we should spell out exactly what modifications each of these rules makes to our list of hypotheses and our goals.

Let's use conjunction as an example. The introduction rule deals with constructing a desired proof (namely, a proof of P ∧ Q, where P and Q can be arbitrary propositions); since the goal represents what we're trying to prove, our introduction rule will deal with the goal rather than our hypotheses. (This isn't always the case, though: we'll see later that some rules can act on both!) We know that the introduction rule for conjunction should split our goal in two: we need to prove P and prove Q separately in order to conclude that P ∧ Q is true. So our introduction rule should transform a proof state that looks like this:

… hypotheses …
⊢ P ∧ Q

Into one that looks like this:

… hypotheses …
⊢ P

… hypotheses …
⊢ Q

Notice that we've kept the hypotheses the same: since we're proving P ∧ Q under the assumption that all those hypotheses are true, we should still be able to assume them when we're proving P and Q individually. (If I am proving "n is odd and n > 3" with the hypothesis "n = 5," clearly it would be a mistake to drop that hypothesis when trying to prove the two conjuncts—if we don't have that hypothesis, then neither is necessarily true of an arbitrary number n!)

There's an issue with the notation above, though: it's clumsy. If we were to write out every introduction and elimination rule for every connective and quantifier mentioned above in that format, this page would be very long indeed. Instead, we use a more concise (and more precise) notation.

First, rather than writing "hypotheses," we'll represent our collection of existing hypotheses with a capital C (for "context"). Then, we'll write our rule in the following form:

C ⊢ P     C ⊢ Q
⎯⎯⎯⎯⎯⎯⎯
C ⊢ P ∧ Q

We read this from the bottom up: "in order to prove P ∧ Q (with context C), it suffices to prove P (with context C) and then prove Q (with context C)." Alternatively, using the same language as above: our rule transforms a proof state that looks like the bottom into a proof state that looks like the top.

Introduction rules

We'll run through the introduction rules for all of our connectives here.

And (conjunction) intro

As we just described, the rule for ∧ intro looks like this:

C ⊢ P     C ⊢ Q
⎯⎯⎯⎯⎯⎯⎯
C ⊢ P ∧ Q

Or (disjunction) intro

To prove a statement like P ∨ Q, we have two choices: we can either prove P, or prove Q. We don't need to do both! This means that there are two introduction fules for ∨, a "left" rule:

C ⊢ P
⎯⎯⎯⎯⎯
C ⊢ P ∨ Q

and a "right" rule:

C ⊢ Q
⎯⎯⎯⎯⎯
C ⊢ P ∨ Q

Again, read from the bottom up. This rule transforms an "or" goal into a simpler one.

Implication intro

Reasoning with an if-then statement is a form of hypothetical reasoning. This is the first rule that will change the context, that is, add hypotheses to our proof state:

C, P ⊢ Q
⎯⎯⎯⎯⎯
C ⊢ P → Q

In English: "in order to prove P → Q, it suffices to prove Q with the extra assumption that P."

We usually write this in natural language proofs with the word "assume" or "suppose."

Bi-implication intro

An "if and only if" statement is, essentially, the "and" of two "implies" statements.

C ⊢ P → Q     C ⊢ Q → P
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
C ⊢ P ↔ Q

Not (negation) intro

This can be a tricky one! To show that a statement does not hold, we have to show that if it does hold, then nonsense follows. This is another example of hypothetical reasoning: notice the similarity with implication.

C, P ⊢ False
⎯⎯⎯⎯⎯⎯
C ⊢ ¬ P

We represent "nonsense" as False here.

Atom intro

The simplest rule of all says that if we know P, then we can prove P.

⎯⎯⎯⎯
C, P ⊢ P

Notice there are no conditions above the horizontal bar. This is a "terminal" rule: it closes a goal! If we need to prove P and P is in our context, there's nothing left to do.

Existential and universal intro

We'll wait to add these until we've reached them in class!

Elimination rules

Remember that intro rules are goal directed. Given a goal of a certain shape, we can pick an appropriate intro rule to prove it. Elimination rules, in contrast, are hypothesis directed. They tell us how to use a hypothesis of a certain shape.

And (conjunction) elim

To use an "and" statement in our context, we can split it into its two components.

C, P, Q ⊢ G
⎯⎯⎯⎯⎯⎯
C, P ∧ Q ⊢ G

Once again, we can read this from the bottom up: "to prove a goal G using a hypothesis P ∧ Q, it suffices to prove G using two hypotheses P and Q."

Or (disjunction) elim

Using an "or" statement involves reasoning by cases. If we know that either P or Q holds, and we want to show G, we can suppose that P holds and show G, then suppose that Q holds and show G. Since the hypothesis in at least one branch must be true, we've covered all possibilities.

C, P ⊢ G     C, Q ⊢ G
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
C, P ∨ Q ⊢ G

Implication elim

Using an implication is a very classic move that sometimes goes by the Latin name modus ponens. We'll represent this two ways.

First: if we know an implication P → Q, and we know the left hand side P, we must also know the right hand side Q. This form of modus ponens adds a new hypothesis to our context.

C, P → Q, P, Q ⊢ G
⎯⎯⎯⎯⎯⎯⎯⎯⎯
C, P → Q, P ⊢ G

The other way to think about this is more goal-oriented. If we know P → Q and our goal is to show Q, it suffices for us to show P. (Intuitively: if we can show that P, we could then apply the previous version of modus ponens to get a new hypothesis Q, which would then close the goal of Q.)

C, P → Q ⊢ P
⎯⎯⎯⎯⎯⎯⎯
C, P → Q ⊢ Q

Bi-implication elim

Once again, bi-implication is treated like a conjunction of two implications. We can use an iff statement by splitting it into two "implies."

C, P → Q, Q → P ⊢ G
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
C, P ↔ Q ⊢ G

Not (negation) elim

What can we do with the fact that P is false? Not much, on its own. But if we also know that P is true, then something very absurd is going on. Negation elimination captures exactly this idea: if we know both a proposition P and its negation ¬ P, we can conclude False. This terrible proposition holds only if we're in a world that doesn't make sense! In natural language, we say that we've found a contradiction.

⎯⎯⎯⎯⎯⎯⎯⎯
C, P, ¬ P ⊢ False

In fact, we can generalize this even more. If False holds, and the world doesn't make sense, then every proposition is provable. So from a contradiction, we can conclude any statement.

⎯⎯⎯⎯⎯⎯
C, P, ¬ P ⊢ G

Other Kinds of Maneuvers

info

This section will be introduced soon.

Footnotes

1. Perhaps you're a bit suspicious of this appeal to "intuition." But fear not: there are ways of verifying that the system of proof rules we've set up is indeed "reasonable" (and ways of defining "reasonable" more precisely)! But those techniques are the content of a course in logic, not 22. ↩