Computer Aided Formal Reasoning Fall, 1995 Lecture notes 5 Judith Underwood

Adding quantification

Last time I talked about using axiom schemes to represent a family of axioms following some pattern. For example, recall that we had

    pair:  A → B → and A B
    fst:  and A B → A
    snd:  and A B → B

We can look at these in two ways: as a (logical) list of axiom schemes together with names for them, or as programming language constructs which can be given types of a particular pattern.

Looking first at the programming language interpretation, we would really like a more formal way of saying that there is a family of pair operations, one for every type following the pattern A → B → and A B. A function like pair is called polymorphic; it can be applied to arguments of many types. To describe this, we introduce type variables, variables which range over types (as opposed to variables which range over terms of a given type.) We will generally use capital letters (A, B, C) to denote type variables. These will now be part of our term language.

We can fit the idea of a family of pairing functions into our functional framework if we think of pair as a function which takes two types as arguments, and returns a pairing function of the appropriate type, so that

                          pair A B: A → B → and A B

i.e. the first two arguments determine the type of the resulting function.

To express the type of this version of pair, we can say

                       pair : ∀A ∀B. A → B → and A B.

In other words, for all types A and B, we have a pairing function of type A → B → and A B. The Lego notation for this is

                         {A:Prop}{B:Prop}A->B->and A B

(usually simplified to {A,B:Prop}A->B->and A B.) This is just another way of describing a function type – the type A->B is the same as {x:A}B if B does not contain x. In the case of pair, the type of the result depends on the arguments A and B, so we must preserve their names.

An element of this type (i.e. a pairing function) would look like:

             [A:Prop][B:Prop][x:A][y:B] (something which pairs x and y)

We will look at this in greater detail soon, but first shall present the rules for dealing with quantification over Prop more formally.

Rules

First, recall the rules we had last time:

                                   \overline{G, x:A ⊢x:A}

                                \frac{G, x:A ⊢M:B}{G ⊢[x:A]M :A ->B}

                             \frac{G ⊢M: A ->B    G ⊢N: A}{G ⊢M N:B}

We extend the set of assumptions G to include assumptions of the form A: Prop for propositional variables. Now we add rules for introducing and eliminating propositions quantified by propositions:

                            \frac{G, x:Prop ⊢M:B}{G ⊢[x:Prop]M :\{x:Prop\}B}

                         \frac{G ⊢M: \{x:Prop\}B    G ⊢N: Prop}{G ⊢M N:B[N/x]}

Finally, we have a rule which just describes the fact that a quantified proposition is still a proposition:

                              \frac{G, A:Prop ⊢B:Prop}{G ⊢\{A:Prop\}B : Prop}

There are still more rules than these for dealing with Prop, but these should be enough for now.

These rules describe how we can construct universally quantified propositions as well as when we can prove them. Notice that when we apply a term to an element of Prop, we do the substitution in the type as well as the term. Thus we have types parameterized by Prop, and the terms of these types are also parameterized by Prop.

Using quantification to define and and or

In Lego, the connectives and and or are defined using quantification over types and the function type ->. (We could not have defined them just using ->.) Let us consider first and. We want that and should be a function of type Prop ->Prop ->Prop, i.e. it should take two propositions (say A and B) as arguments and return a proposition, and A B. The proposition returned must package up A and B in some way which describes the meaning of and A B. This meaning is determined by the properties of proofs of and A B (or the properties of elements of the type and A B. How might we use a proof of and A B? In general, we will want to be able to use both parts of the conjunction in a proof of some other proposition C. If we can prove C assuming A and B, then having and A B should mean that C is provable. In other words, if and A B is provable, then A ->B ->C implies there is a proof of C, for all propositions C. On the other hand, if it is the case that for all C, knowing that A ->B ->C is sufficient to prove C, then and A B should be provable. More formally, and A B = {C:Prop}(A ->B->C)->C. We can check that this is Lego’s definition:

Lego> and;
value of and = [A,B:Prop]{C|Prop}(A->B->C)->C
type  of and = Prop->Prop->Prop

Recall that {C|Prop} is the same as {C:Prop} except that the argument need not be supplied explicitly, as it can be deduced from the other arguments. To see how this works, let us look at fst and snd, the functions which create and eliminate elements of type and A B. These are also defined:

Lego> pair;
value of pair = [A,B|Prop][a:A][b:B][C|Prop][h:A->B->C]h a b
type  of pair = {A,B|Prop}A->B->and A B

Given a:A and b:B, the element of and A B produced is [C|Prop][h:A->B->C]h a b. Notice that this packages up the a and b given as arguments and “hides” them inside a function. To get them out, we need to apply the function. This is how fst and snd work.

Lego> fst;
value of fst = [A,B|Prop][h:and A B]h ([g:A][_:B]g)

type  of fst = {A,B|Prop}(and A B)->A
Lego> snd;
value of snd = [A,B|Prop][h:and A B]h ([_:A][g:B]g)
type  of snd = {A,B|Prop}(and A B)->B

Notice how fst and snd use the argument h of type and A B – they use the fact that it is really a function from A ->B ->C to C, and they apply it to an argument of type A ->B ->C to produce their results. In the case of fst, the argument is ([g:A][ :B]g): A ->B ->A (hence Lego infers that C is A), and the result is of type A, as desired.

Similarly, or is defined as a function from Prop to Prop to Prop:

Lego> or;
value of or = [A,B:Prop]{C|Prop}(A->C)->(B->C)->C
type  of or = Prop->Prop->Prop

The constructors again “hide” the argument in a function term, and the elimination rule applies that function:

Lego> inl;
value of inl = [A,B|Prop][a:A][C|Prop][h:A->C][_:B->C]h a
type  of inl = {A,B|Prop}A->or A B
Lego> inr;
value of inr = [A,B|Prop][b:B][C|Prop][_:A->C][h:B->C]h b
type  of inr = {A,B|Prop}B->or A B
Lego> or_elim;
value of or_elim = [A,B,C|Prop][M:or A B][N1:A->C][N2:B->C]M N1 N2
type  of or_elim = {A,B,C|Prop}(or A B)->(A->C)->(B->C)->C

Notice that all or elim does is apply the argument of type or A B to the other arguments – the definitions of inl and inr ensure that this works out. So, or elim is just syntactic sugar, and Refine or elim d; in Lego is really equivalent to just Refine d;

Exercise Show that or elim (inl a) f g = f a by expanding the definitions and normalizing the resulting lambda terms.

Exercise Think about what applied a term of type and A B to an argument would do. (This could be packaged as an and elim analogous to or elim. What kind of argument would it take? How might you use this?

Finally, let us look at the definition of absurd:

Lego> absurd;
value of absurd = {A:Prop}A
type  of absurd = Prop
Lego> absurd_elim;
value of absurd_elim = [M:absurd][N:Prop]M N
type  of absurd_elim = absurd->{N:Prop}N

Again, absurd elim is just an application of the term of type absurd to a proposition. It produces a proof from nothing since absurd is the same as the assertion, “For all propositions A, A is provable.”

Prop versus Type

Until now I have been emphasizing the similarities between propositions and types. In Lego, however, there is a distinction – propositions are types, but not all types are propositions. (I have been somewhat sloppy about the distinction in these notes, but we will fix that soon.) The reason is that there are really two kinds of quantification in Lego, one which defines propositions and one which defines types. So far, we have been working with propositions only, and we will continue to concentrate on propositions for a while. However, we will use both ideas when we talk about existential quantification next time.