Computer Aided Formal Reasoning 1996/7 Lecture notes 3 Judith Underwood

Room change announcement: Starting next week, the Tuesday lectures will be in room 3218. Thursday lectures will still be in 3317.

Today we will look at a proof system for propositional logic which extends the system we saw last time to include formulas with and and or, and also a constant absurd. As last time, we’ll have both proof rules and terms representing proofs. We’ll also see a bit more about using Lego to help with proofs in this system.

1 Propositional Logic

The formulas in this logic are defined by the following grammar:

A = P  (P a variable)
| A->A

                              | and A A

| or A A

                              | absurd

This is a less wordy way of saying that variables are formulas, absurd is a formula, and if A and B are formulas then and A B, or A B, and A->B are formulas. The prefix notation (and A B instead of A and B) is for reasons to do with Lego which we’ll get to later. In fact, in Lego you could write A /\ B for and A B and A \/ B for or A B, but these are just abbreviations.

Below we have the introduction and elimination rules for this system. Introduction rules say how to build a proof of a formula with a given connective; elimination rules say what you can conclude, given a proof of formula with that connective. As before, we also have the axiom rule

                                    \overline{G, A ⊢ A}

which says that if A is in our set of assumptions, we may conclude A. Here, G denotes a (possibly empty) set of formulas.

Proposition Introduction rules  Elimination rules

       A->B          \frac{G,A ⊢ B}{G ⊢ A->B}                 \frac{G ⊢ A->B   G ⊢ A}{G ⊢ B}

      and A B      \frac{G ⊢ A    G ⊢ B}{G ⊢ and A B}      \frac{G ⊢ and A B}{G ⊢ A}
                                                 \frac{G ⊢ and A B}{G ⊢ B}
      or A B        \frac{G ⊢ A}{G ⊢ or A B}
                     \frac{G ⊢ B}{G ⊢ or A B}       \frac{G ⊢ or A B   G ⊢ A->C   G ⊢ B->C}{G ⊢ C}

      absurd                                    \frac{G ⊢ absurd}{G ⊢ A}

We define not A as A ->absurd. (We use the name absurd rather than false because next week we will add a type of boolean values to the logic, and the natural names for them are true and false.)

The introduction and elimination rules for -> are just as we had them last time. Notice that we have two introduction rules for or, depending on which side of the disjunct we have proved, and two elimination rules for and, depending on which side of the conjunct we wish to use. There are no introduction rules for absurd. This means that if absurd is ever proven, it must be as a consequence of some set of contradictory assumptions which mention absurd, for example, A and not A, that is, A and A->absurd. The elimination rule for absurd represents the fact that if we have a contradiction, we may conclude anything.

Example:

                    and P Q ⊢ and P Q
                       and P Q ⊢ Q

                                         and P Q ⊢ and P Q
                                            and P Q ⊢ P
                               and P Q ⊢ and Q P
                             ⊢ (and P Q) ->(and Q P)

1.1 Adding proof terms

Remember that the proof terms are really just a flat notation for proofs, where variables are essentially labels for assumptions.

The axiom rule is the same as last time:

                           x1:A1, ..., xn:An ⊢ xi:Ai

In general something of the form x:A means that x represents a proof of A. So, the axiom rule can be read as “if we have, as an assumption, that xi proves Ai, then xi proves Ai.”

Here are the rest of the rules. We now use G to abbreviate the list of assumptions with their labels. Lower case letters will stand for proof terms in hypotheses.

Proposition  Introduction rules  Elimination rules

       A->B         \frac{G, x:A ⊢ b:B}{G ⊢ [x:A]b :  A->B}                 \frac{G ⊢ f:A->B   G ⊢ a:A}{G ⊢ fa :  B}

      and A B      \frac{G ⊢ a:A    G ⊢ b:B}{G ⊢ pair a b:  and A B}                \frac{G ⊢ t:  and A B}{G ⊢ fst t:A}
                                                         \frac{G ⊢ t:  and A B}{G ⊢ snd t:B}
      or A B         \frac{G ⊢ t:A}{G ⊢ inl t:or A B}
                      \frac{G ⊢ t:B}{G ⊢ inr t:or A B}        \frac{G ⊢ d:or A B   G ⊢ f:A->C   G ⊢ g:B->C}{G ⊢ or elim d f g:  C}

      absurd                                         \frac{G ⊢ t:  absurd}{G ⊢ absurd elim t A : A}

Notice that the absurd_elim proof term, which represents the fact that anything follows from a contradiction, includes the formula being proved.

Example: including the proof terms in the previous example gives:

            x:  and P Q ⊢ x:  and P Q
             x:  and P Q ⊢ snd x:  Q

                                         x:  and P Q ⊢ x:  and P Q
                                          x:  and P Q ⊢ fst x:  P
                  x:  and P Q ⊢ pair (snd x) (fst x):  and Q P
            ⊢ [x:and P Q]pair (snd x) (fst x):  (and P Q) ->(and Q P)

Reduction rules

In addition to β-reduction for lambda calculus, we have the following rules for the new kinds of proof term:

                          fst (pair m n)  ⟶ m
                          snd (pair m n)  ⟶ n
                          or elim (inl x) f g ⟶ f x
                          or elim (inr x) f g ⟶ g x

There is no reduction rule for absurd elim.

   We can look at these new proof terms (pair, fst, snd, inl, inr, or elim, and absurd elim)

in two ways. We can interpret them as a representation for the proof rules above, or we can consider them as special functions which take proofs as arguments and return proofs of a different formula. (After all, that is just what a proof rule is – a way of using existing proofs to make a new proof.) Thought of as functions, the types of these functions describe the proofs required as input and output.

When interpreted this way, the functions and their types are:

pair : P -> Q -> and P Q
fst : and P Q -> P
snd : and P Q -> Q
inl : P -> or P Q
inr : Q -> or P Q
or_elim : (or P Q) -> (P->R) -> (Q->R) -> R
absurd_elim : absurd -> P

Interpreted as propositions, these types represent axioms in the sense of a statement which is given as fundamental. The terms can be though of as names for the axioms when they are used in a proof. The types of these axioms are really what are called type schemas – we may substitute other types for P, Q and R as desired. To represent this formally, the types are universally quantified. The Lego notation for this is

pair: {P,Q:Prop}P -> Q -> and P Q

and so forth. The formula {P:Prop}A is read “for all propositions P, A”. We’ll look at quantification more next time.

More about Lego

Last time we saw how to get started in Lego, and how to build and evaluate proofs in implicational logic. Extending the proof system to include and, or, and absurd gives us more scope for interesting proofs.

Let’s look at a detailed example – a proof of (and P Q) ->(and Q P). Recall that we must declare P and Q to be propositions:

Lego> [P,Q:Prop];
decl  P Q: Prop

Then, we start the proof:

Lego> Goal (and P Q) -> (and Q P);
Goal
  ?0 : (and P Q)->and Q P
Lego> intros x;
intros (1) x
  x : and P Q
  ?1 : and Q P

Remember that “intros” corresponds to the ->introduction rule, applied backwards. Now we want to apply the and elimination rule. The way we have to do this is by noting that we build a proof of and Q P from its components by using pair:

Lego> Refine pair;
Refine by  pair
  ?4 : Q
  ?5 : P

Think of using Refine here as providing a proof term or part of a proof term for the current goal. Given the goal ?1 : and Q P, issuing the command Refine pair is something like telling Lego that the proof term which will fill in for ?1 will start with pair. Lego then calculates what will be required as arguments to pair, and presents those as subgoals.

Recall that we work with the lowest-numbered (first-listed) current subgoal, in this case ?4 : Q. Also recall although it is not listed here, we still have the assumption x : and P Q. So, given this x, we can provide a proof of Q by taking snd x:

Lego> Refine snd x;
Refine by  snd x
  ?5 : P

This eliminated goal ?4 completely, leaving us with only goal ?5 : P, which we can deal with by using the assumption x again:

Lego> Refine fst x;
Refine by  fst x
Discharge..  x
*** QED ***

And now we’re done. We save this proof:

Lego> Save and_comm;
"and_comm"  saved as global

and look at the proof term created:

Lego> and_comm;
value of and_comm = [x:and P Q]pair (snd x) (fst x)
type  of and_comm = (and P Q)->and Q P

Some questions you might have:

If I can do ->introduction with “intros”, why can’t I do and-introduction with some kind of intros as well? This is a very good question. The answer lies in the fact that and and or are actually defined connectives, rather than built in to the system. We’ll see how this works in a few lectures, but for now you can think of “Refine pair” as acting like and-introduction, and “Refine inl” and “Refine inr” as or-introduction.

What’s really going on with Refine? We’ll talk about this in some detail later, since Refine is the real workhorse of the prover. The idea is that Refine replaces a goal G by either a proof of G or some goals which, when proven, will imply G. The type of the term given as an argument to Refine determines what Refine does. If we have the goal G, and we Refine by something of type G (that is, a proof of G) then Refine does not generate any new subgoals. If, however, we Refine by some formula which ends with ->G, as A1->A2->...->G, Refine will eliminate the goal G and replace it with the formulas before the final arrow (in this instance A1, A2, ... ) as new goals.

Why did we jump from goal 1 to goal 4? Lego actually had to do some work when we did that Refine pair step, and it generated some intermediate goals which it was able to discharge by itself. We’ll go into what happened precisely later on, but notice that we use pair to make proofs of any conjunction of two formulas – and A B, and P Q, etc. So, the arguments to pair may be proofs of anything. Lego had to work out that the arguments to this use of pair must be proofs of Q and P to get the desired conclusion and Q P, and, while it computed this, it generated and discharged the two subgoals ?2 and ?3.

Why did you say “Refine snd x” instead of just “Refine snd”? This is related to the answer to the previous question. Let’s see what happens with “Refine snd”. Recall the state was:

  x : and P Q
  ?4 : Q
  ?5 : P
Lego> Refine snd;
Refine snd;
Refine by  snd
  ?6 : Prop
  ?8 : and ?6 Q
  ?5 : P

In order to get a proof of Q using snd, we must have a proof of and (something) Q. We know we’ve got the assumption and P Q, but Lego doesn’t, so it asks us to supply a proposition ?6 and a proof of and ?6 Q We could proceed perfectly well from this point by giving it the proposition P explicitly, via Refine:

Lego> Refine P;
Refine P;
Refine by  P
  ?8 : and P Q
  ?5 : P

and then giving it the proof of and P Q explicitly as well:

Lego> Refine x;
Refine x;
Refine by  x
  ?5 : P

which leaves us where we were after Refine snd x.

Are there any shortcuts? Yes. There are lots of shortcuts which you will discover as the course progresses. Above, I mentioned that you could think of using Refine to provide a proof term or part of a proof term for your current goal. You can carry this as far as doing a whole proof in one step:

Lego> Goal  (and P Q) -> (and Q P);
Goal
  ?0 : (and P Q)->and Q P
Lego> Refine [x:and P Q]pair (snd x) (fst x);
Refine [x:and P Q]pair (snd x) (fst x);
Refine by  [x:and P Q]pair (snd x) (fst x)
*** QED ***

but it is generally easier to break it down into smaller steps.

I made a mistake. What now? You can undo your last n commands with Undo n.

How do I find out what all my assumptions are? The command Prf will show you the whole state of the proof, including all assumptions and subgoals.

I typed “Intros” instead of “intros” and got a mess. What happened? Let’s look at an example of intros:

Lego> Goal (and P Q) -> (and Q P);
Goal (and P Q) -> (and Q P);
Goal
  ?0 : (and P Q)->and Q P
Lego> intros;
intros;
intros (1)
  H : and P Q
  ?1 : and Q P

Note that the assumption has been named H since no name was provided. Now if instead we had typed Intros, we get:

Lego> Goal (and P Q) -> (and Q P);
Goal (and P Q) -> (and Q P);
Goal
  ?0 : (and P Q)->and Q P
Lego> Intros;
Intros;
Intros (3)
  H : and P Q
  C | Prop
  H1 : Q->P->C
  ?1 : C

This is a consequence of the fact that and is really a defined connective rather than a logical primitive operator. We’ll see how this works in a few lectures’ time – for now, just undo and try again.