Computer Aided Formal Reasoning Fall, 1995 Lecture notes 3 Rod Burstall and Judith Underwood

1 Propositional Logic

We now turn to logic, initially propositional logic, and apply the same techniques as for functional programming, but using propositions instead of types and proofs instead of terms. Instead of saying “A term has a type,” we say “A proof proves a proposition.”

We shall see that we can use the same kinds of rules to develop proofs as we used to derive programs. This is because of the Curry-Howard Correspondence (sometimes called “Curry-Howard Isomorphism” – the names of Tait and de Bruijn are sometimes also added). The slogan for this correspondence is

Propositions as types

and, as a consequence, we will have

Proofs as programs.

A proposition is provable when it has a proof; a type is inhabited when there is a term of that type. Types that arise in programming languages are virtually all inhabited, but here we are taking a more abstract view.

There will be a correspondence between the type constructors and the propositional connectives, so that implies corresponds to ->, and and corresponds to # (pairing). The logical connective or corresponds to +, the (disjoint) sum of two types, where by s+t we mean the type of elements which are either of type s or of type t and are marked as such. We did not consider this type in our programming language. You should be able to deduce how elements of this type work when you see the rules for manipulating the proofs of disjunctions (and hence, correspondingly, terms of disjoint union type).

Notation: We write L, M, N for proofs and p,q,r for propositions.

Introduction and elimination operators for propositions

Proposition Introduction rules Elimination rules

                  p ->q       [x:p] M          M N
                  and p q     pair M N         fst M , snd M
                  or p q      inl M, inr N     or elim M N L
                  absurd                       absurd elim M p

A proposition p is provable if there is a proof M such that M:p. In Lego, you may write p /\ q for and p q and p \/ q for or p q, but these are just abbreviations.

absurd is Lego’s name for the false proposition (false being of type bool); it corresponds to the empty type. If we assume M : absurd, then we can prove any proposition p with the proof absurd elim M p – this is the representation of the fact that false implies anything.

This gives us intuitionist, or constructive, logic, not classical logic. Some classical theorems are not provable in intuitionist logic, for instance not(not P) ->P, which means that proof by contradiction is not allowed. However, constructive logic is useful for reasoning about computation because of the Curry-Howard correspondence. If you assume the above proposition (or any of a number of equivalents to it), you regain classical reasoning.

Proof rules for propositions (without proof terms)

Let’s first look at rules from a purely logical standpoint. The most basic rule is

                                 \overline{G, p |-p}

We consider everything to the left of the turnstile (|-) to be our assumptions; if our assumptions include p, then we can conclude p.

Proposition Introduction rules  Elimination rules

     p->q         \frac{G, p |-q}{G|-p->q}           \frac{G|-p->q   G|-p}{G|-q}

   and p q      \frac{G|-p    G|-q}{G|-and p q}        \frac{G|-and p q}{G|-p}
                                            \frac{G|-and p q}{G|-q}
    or p q       \frac{G|-p}{G|-or p q}

                 \frac{G|-q}{G|-or p q}       \frac{G |-or p q   G |-p->r   G |-q->r}{G |-r}
    absurd                                  \frac{G |-absurd}{G |-p}

We define not p as p ->absurd.

Example: a proof that and is commutative in this logic is:

                  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)

Proof rules for propositions (with proof terms)

The basic rule is

                                  \overline{G, x:p |-x:p}

The x here stands for a proof of proposition p, so we can read this as saying “if we have, as an assumption, that x proves p, then x proves p.” We now extend G to stand for a set of such propositions paired with proofs.

Proposition  Introduction rules  Elimination rules

        p->q        \frac{G, x:p |-M:q}{G|-[x:p]M : p->q}                    \frac{G|-M:p->q   G|-N:p}{G|-M N : q}

      and p q      \frac{G|-M:p    G|-N:q}{G|-pair M N:and p q}                    \frac{G|-M: and p q}{G|-fst M:p}
                                                          \frac{G|-M: and p q}{G|-snd M:q}
       or p q       \frac{G|-M:p}{G|-inl M:or p q}

                     \frac{G|-N:q}{G|-inr N:or p q}       \frac{G |-L: or p q   G |-M : p->r   G |-N : q->r}{G |-or elim L M N:r}
       absurd                                       \frac{G |-M: absurd}{G |-absurd elim M p :  p}

Again, we define not p as p ->absurd.

If we ignore the proof terms, we get the purely logical proof system above. The proof terms are essentially a flat notation which describes the rule which has been applied.

For example, including the proof terms in the proof that and is commutative gives:

               L: and p q |-L: and p q
                 L:and p q |-snd L:q

                                         L:and p q |-L: and p q
                                          L:and p q |-fst L:p
                    L:and p q |-pair (snd L)(fst L): and q p
           | − [L:and p q]pair (snd L)(fst L): (and p q) ->(and q p)

Exercise: Look at this long enough so that you see how the term [L:and p q]pair (snd L)(fst L) actually describes the whole proof of (and p q) ->(and q p).

Using this logic

Eventually, we would like to introduce propositions about booleans, natural numbers and lists, so that we may prove properties of programs. The usual way to do this would be to introduce predicates, including a special predicate called equality which enables us to formulate equations. Then we would introduce the quantifiers ∀ and ∃ , to get “predicate logic”.

This is a big step. The simple type theory which we introduced for functional programming has operators ->, #, and + which correspond to implies , and and or , but it has no type constructors corresponding to the quantifiers. This discrepancy is precisely the seed which gave rise to the flourishing development of “Type Theory” initiated by Howard and Scott in the late seventies; they built on Curry’s earlier insight into the correspondence between simple type theory and propositional logic. (Hence the name “Curry-Howard correspondence”.) It turns out there are several ways of introducing quantifiers as types; we will look at this more in the next few lectures.

But first let us see how to develop proofs by refinement in just the same way that we developed functional programs. Here are two examples:

The proof above that and is commutative can be written:

Goal and comm:

(and p q) ->(and q p)

[L: and p q] (and q p) pair

q snd L p fst L

All we have done is rewrite the proof, beginning with the conclusion, and indenting for each rule applied (we stopped just before we got to the axioms). The bold entries are the propositions on the right side of the turnstile; beneath them are the proof terms supplied as evidence for that proposition. The assumptions are introduced in square brackets.

Goal or imp:

(or (p->q) (p->r) ) ->(p ->(or q r) )

[L: or (p->q) (p->r) ] p ->(or q r) or elim L

(p->q) ->(p ->(or q r) )

[M: p->q ][N: p ]

or q r inl q M N

(p->r) ->(p ->(or q r) )

[M: p->r ] [N: p ]

or q r inr r M N

Exercise: Rewrite this proof as a purely logical proof, using the system without proof terms. Here is the term which constitutes the proof:

        [L: or (p->q) (p->r) ]
                or_elim L
                        ([M: p->q ] [N: p ] inl (M N))
                        ([M: p->r ] [N: p ] inr (M N))

Whilst we may be able to write functional programs using the top-down method it seems hard to write proofs directly just by inspection.

Exercise: Prove the transitivity of ->.

Exercise: Prove the commutativity of or.

Exercise: Prove that and distributes over or.

Exercise*: Prove that p:Prop((not (not p))->p) ->p:Prop(or p (not p)) .

A good feature of such proofs, as opposed to the traditional tree-like displays, is that they are easy to store in the computer, and it is easy to check what a proof really proves - you just run a straightforward type checking algorithm on it. This algorithm can be obtained by inspecting the typing rules which we gave earlier in these notes. So you can deliver a proof to someone and they don’t have to know how you found it in order to satisfy themselves that it really is a proof. If we want to develop a big theory, we can store such proofs and typecheck them each time as we extend the theory, rather than rerunning the refinement developments. (This is how Lego ”Make” works.)

Lego hints for propositional logic

Since we are now dealing with abstract propositions rather than concrete types like nat and bool, it will be convenient to be able to introduce propositional variables into the Lego state. We can do this with declarations at the top level, for example:

Lego> [p:Prop];
decl  p : Prop
Lego> [q:Prop];
decl  q : Prop
Lego> Goal or_comm: (or p q)->(or q p);
Goal
  ?0 : (or p q)->or q p

and so forth. Until these declarations are removed with Discharge, we can use p and q as propositional variables. Discharge p removes all the declarations since p and reformulates theorems which used them to be universally quantified, e.g. the type of or comm becomes {p,q:Prop}(or

p q)->or q p.

When dealing with logical connectives in Lego, you may be surprised by the results of some commands. In particular, new propositional variables may appear when you have done something as innocent as “Intros;”. This is because and, or, and absurd are actually defined in terms of − >, using quantification over types. For the curious, these definitions are:

or = [A,B:Prop]{C|Prop}(A->C)->(B->C)->C
and = [A,B:Prop]{C|Prop}(A->B->C)->C
absurd = {A:Prop}A

Note that {A:Prop}A means essentially “for all propositions A, A is true” – a manifestly false statement, and one which clearly implies the truth of all propositions. This explains why absurd is both the definition of false, and why if we assume we have t of type absurd, we can produce a term of any type A by applying t to A. This is all that absurd elim does. We’ll talk about this more in class over the next few lectures.

Using intros instead of Intros will help you avoid getting the expansions of these defined connectives when you don’t want them.