Extensions to Theory of Constructions (734 lines)

Date:     Wed, 27 Sep 89 11:22:41 EDT


                              Jonathan P. Seldin
                          Department of Mathematics
                             Concordia University
                         7141 Sherbrooke Street West
                          Montreal, Quebec, H4B 1R6

     Acknowledgement of Sponsorship:  The research which produced the 
     information contained in this document was sponsored in part by the 
     U.S. Air Force Systems Command, Rome Air Development Center, Grif-
     fiss AFB, New York 13441-5700 under Contract No. F30602-85-C-0098, 
     in part by grant EQ41840 from the program Fonds pour la Formation de 
     Chercheurs et l'aide a la Recherche (F.C.A.R.) of the Quebec 
     Ministry of Education, and in part by grant OGP0023391 from the 
     Natural Sciences and Engineering Research Council of Canada.

1.  Introduction

     In his posting to the TYPES network [1989], Pottinger shows that if 
excluded middle and definite descriptions are added to Coquand's calculus of 
constructions, then any two terms in a small type (i.e., a type in Prop) are 
equal (in the sense of Leibniz equality).  This conclusion is called "proof 
degeneracy".  Although in general proof degeneracy does not imply inconsisten-
cy, it is still undesirable because it means that all terms in small types are 
identified by the logic, and hence there is no representation of a data type 
with more than one element.

     Coquand [forthcoming] showed by a model theoretic proof that excluded 
middle in the calculus of constructions is consistent.  Here I show a stronger 
result, that excluded middle without definite descriptions does not imply 
proof degeneracy.  My method  is proof theoretic, a variant of the - - 
interpretation, and part of it provides an alternative proof of Coquand's 
consistency result.  My main result will follow from a proof that an 
environment which implies classical arithmetic is consistent.  Since one of 
the Peano axioms asserts that zero is not a successor, proof degeneracy would 
imply the inconsistency of this environment.

     Coquand [forthcoming] also proved that excluded middle and strong sums 
imply proof degeneracy.  Garrel Pottinger has pointed out to me (private 
communication) that the strong sums, when interpreted under the Curry-Howard 
isomorphism, have the disjunction property.  Since this property is known to 
be characteristic of constructive logic and incompatible with classical logic, 
this result of Coquand is really a confirmation of what we should expect of 
classical logic.  The result of Pottinger [1989], on the other hand, is 
unwelcome, since both excluded middle and definite descriptions are desirable 
in some circumstances.  The result proved here shows that we are more likely 
to have to give up definite descriptions than excluded middle.

     I realize that this version will be hard to read because it is written 
entirely in ASCII characters.  I am writing it this way for circulation on the 
TYPES network.  I intend to incorporate this work in more readable form in 
Seldin [in preparation 2].

     I would like to thank Garrel Pottinger for his helpful comments and 

2.  TOC

     I will follow Pottinger [1989] in referring to the theory of construc-
tions as TOC.  The version of the theory of constructions used here will be 
the one of Seldin [1987], which is more general (in its equality rules) than 
the versions used by Coquand and Pottinger.  More specifically, I will use the 
formulation of TOC which is called TAC in Seldin [1987, Chapter 4].
     I will adopt most of the conventions of Pottinger [1989].  However, I 
will not use parameters, so lower case Greek letters will be available for 
other uses.  In particular, kappa and kappa' will each be either Prop or Type, 
and Prop and Type will be abbreviated `P' and `T' respectively.  Furthermore, 
`[N/x]M' will denote the result of substituting N for x in M (this was Curry's 
notation, and I am used to it).  The version of TOC used here is a natural 
deduction system in the sense of Gentzen and Prawitz.  It has one axiom, 

(P T)                              P : T.

The rules are as follows:

(kappa kappa' Formulation)

                              [x : A]        Condition:  x does not occur
                                             free in A or in any undis-
          A : kappa           B : kappa'     charged assumption.
              (all x : A)B : kappa',

(Eq' kappa)

               A : kappa      A conv B
                      B : kappa,

(all e)

               M : (all x : A)B       N : A
                       MN : [N/x]B,

(all kappa i)

               [x : A]                       Condition:  x does not occur
                                             free in A or in any undis-
                M : B           A : kappa    charged assumption.
                \x : A . M : (all x : A)B,


                         M : A               A conv B
                                    M : B.

     Seldin [1987, Theorem 4.14] proves the strong normalization theorem for 
deductions in this formulation.  Since this result refers to a Prawitz-style 
reduction (see Prawitz [1965]), it has as a consequence that in any normalized 
deduction whose conclusion is the conclusion of an inference by (all e), the 
main branch (which I am writing as the left branch in tree diagrams) consists 
of inferences by (all e) and (Eq") and no other rules.

3.  Additional assumptions in TOC

     The strong normalization theorem for deductions in TOC implies the 
consistency of the basic system.  However, environments Gamma may still be 
inconsistent in the sense that

                              Gamma |- M : void

for some term M.  To prove an environment Gamma consistent, we need to show 
that this cannot happen.  Note that since void is \x : P . x, from

                              Gamma |- M : void,

it follows for a variable x not free in Gamma that

                           Gamma, x : P |- Mx : x.

Furthermore, the last inference in this latter deduction cannot be by 
(all kappa i).  Hence, the last inference must be by (all e) (or (Eq"), but in 
this case the same conclusion follows).  Furthermore, the formula at the top 
of the main (left) branch cannot be discharged; for the only rule which would 
allow the discharge of an assumption over the left premise is (kappa kappa' 
Formation), and this rule cannot occur in the left branch if the type of the 
conclusion is a variable.  Hence, to show that there is no deduction of

                           Gamma, x : P |- Mx : x,

it is often sufficient to show that no formula of Gamma can occur at the top 
of the left branch.

     One class of environments which satisfies this requirement, and is hence 
consistent, is given by the following definition:

     DEFINITION 1.  Let Gamma  be a valid environment (in the sense of Seldin 
[1987]) of the form

                    x_1 : A_1, x_2 : A_2, ..., x_n : A_n.

For each i = 1, 2, ..., n, let A_i be

      (all y_i1 : B_i1)(all y_i2 : B_i2) ... (all y_i,m_i : B_i,m_i)S_i,

where S_i does not convert to the form (all x : A)B.  This S_i is called the 
TAIL of the type A_i.  (It follows that each S_i converts to the form

                           z_i M_i1 M_i2 ... M_ip,

where z_i is either an atomic constant or a variable.)  Then Gamma is STRONGLY 
CONSISTENT if for each z_i which is a variable (and is hence one of the x_j or 
y_j,k), if the number of universal prefixes of A_i is greater than 0, then the 
tail of the type of z_i (which is the tail of A_j or B_j,k) does not convert 
to Prop.

     (Since we are dealing with terms with normal forms, convertibility is 
decidable here.)

     It is not difficult to see that it follows from this definition that no 
formula of a strongly consistent environment Gamma can occur at the top of the 
left branch of a deduction of the form

                           Gamma, Gamma' |- M : x.

     This proves the following immediate consequence of Definition 1:

     THEOREM 1.  A strongly consistent environment is consistent.

     Note how weak this result is:  no type in a strongly consistent 
environment can be the universal closure of any type of the form void, A and 
B, A or B, (exists x : A)B, or Q A M N (see Seldin [1987, Chapter 5] for the 
definitions of these types).

     If the proofs of Seldin [1987, Theorem 5.2 and Corollary 5.2.1] are 
properly rewritten, they show the consistency of an environment of the form 
Gamma, Gamma', where Gamma is as in Seldin [1987, Theorem 5.2] and Gamma' is 
strongly consistent.  The same sort of modification can be made in Seldin 
[1987, Theorem 5.3 and Corollary 5.3.1].

     Since - A is A -> void, no formula of the form - A can occur as the type 
of an assumption in a strongly consistent environment.  However, certain 
environments with negations of formulas as types can be proved consistent:

     DEFINITION 2.  Let Gamma_0 be a strongly consistent environment.  Let 
Gamma_1 consist of assumptions of the form u : - B, where, under the 
assumptions of Gamma_0, B is a small simple type but B does not convert to the 
type of an assumption in Gamma_0.  Let Gamma_2 consist of assumptions of the 
form v : - - B, where, under the assumptions of Gamma_0, B is a small simple 
type, and where - B does not convert to the type of an assumption in Gamma_1 
(but B may convert to the type of an assumption in Gamma_0).  If Gamma is 
Gamma_0, Gamma_1, Gamma_2, then Gamma is said to be STRONGLY NEGATION CONSIS-

     THEOREM 2.  A strongly negation consistent environment is consistent.

     REMARK.  Clearly, if B converts to C, u : - B, v : C |- void.  What this 
theorem says is that if B is a small simple type, this is essentially the only 
way to get a contradiction.

     Proof.  Suppose Gamma is strongly negation consistent and suppose that 
for some term M

                              Gamma |- M : void.

Then for a variable w which is not free in Gamma, we have for some term M'

                           Gamma, w : P |- M' : w.

Normalize this deduction and let it be D.  Suppose also that there is no 
proper subdeduction of D which proves either Gamma' |- M" : void or else 
Gamma', w : P |- M" : w for any other strongly negation consistent Gamma'; 
otherwise we can begin with this proper subdeduction.  (Here proper subdeduc-
tion means that there is more difference than the one inference necessary to 
go back and forth between a conclusion whose type is void and one whose type 
is w.)  Now the last inference in D which differs from (Eq") cannot be 
(all kappa i); thus it must be (all e).  It follows that the left branch of D 
consists of inferences by (all e) and (Eq"), and hence the top of the left 
branch is not discharged.  This assumption at the top of the left branch must 
be in Gamma_1 or in Gamma_2.

     Case 1.  It is in Gamma_1.  Then it is u : - B for a small simple type B 
not convertible to a type in Gamma_0 or Gamma_2, and D is

                              w : P, u : - B


               u : - B           M" : B
              -------------------------- (all e)
                       uM" : void


                         M' : w.

Now clearly no assumption of D_1 is discharged in D_2.  Hence, since B is a 
simple type, the top of the left branch of D_1 must be in Gamma_1 or Gamma_2.  
Hence, D_1 is

                           w : P, u : - B, u' : - B'


               u' : - B'          M''' : B'
              ------------------------------ (all e)
                       u'M''' : void


                          M' : w,

where B' is simple or the negation of a simple type.  But then

                           w : P, u : - B, u' : - B'


               u' : - B'          M''' : B'
              ------------------------------ (all e)
                       u'M''' : void

is a proper subdeduction of D contradicting the assumption about D.  Hence, 
the top of the left branch of D is not in Gamma_1.

     Case 2.  It is in Gamma_2.  Then it is u : - - B, where B is a small 
simple type, and D is

                              w : P, u : - - B


               u : - - B          M" : - B
              ----------------------------- (all e)
                        uM" : void


                          M' : w.

The argument of Case 1 shows that the last inference in D_1 which differs from 
(Eq") is not (all e), so it must be by (all P i), and D_1 is


          w : P, u : - - B, [v : B]

                    D_3                      D_4

                M''' : void                 B : P
               ----------------------------------- (all P i - 1)
                      \v : B . M''' : - B,

where M" converts to \v : B . M''' : - B.  But then D_3 is a proper 
subdeduction of D contradicting our assumption.  Hence, the assumption at the 
top of the left branch of D is not in Gamma_2.

     This shows that Gamma is consistent.

4.  Classical logic

     Any environment with the assumption

                         cl : (all u : P)(- - u -> u)

will imply classical logic.  On the other hand, this assumption cannot occur 
in a strongly consistent environment.

     To simplify the notation below, let CL be an abbreviation for

                           (all u : P)(- - u -> u).

     We want each occurrence of cl : CL as an assumption to occur in a 
subdeduction of the form:


               cl : CL     A : P                   D_2
              ------------------- (all e)
               cl A : - - A -> A                M : - - A
              -------------------------------------------- (all e)
                               cl A M : A.

This is not a difficult restriction to satisfy, since we can replace


                         cl : CL     A : P                   
                        ------------------- (all e)
                         cl A : - - A -> A,

where the conclusion is not a major premise for (all e), by


  cl : CL     A : P                1                
 ------------------- (all e)
  cl A : - - A -> A           [x : - - A]               D_2
 ----------------------------------------- (all e)
                cl A x : A                           - - A : P
               ------------------------------------------------ (all P i - 1)
                      \x : - - A . cl A x : - - A -> A,

where D_2 is

     D_1            D_v

    A : P         void : P                         D_v
   ------------------------ (PP Formation - v)
           - A : P                               void : P
          ------------------------------------------------ (PP Formation - v)
                            - - A : P,

and where D_v is


                       P : T            [x : P]
                      -------------------------- (T P Formation - n)
                               void : P;

also if cl : CL is not the major premise for an inference by (all e), then we 
can replace it by

                2                                        2

   cl : CL   [x : P]               1                  [x : P]
  ------------------- (all e)
   cl x : - - x -> x          [y : - - x]               D_1
  ---------------------------------------- (all e)
                cl x y : x                           - - x : P
               ------------------------------------------------ (all P i - 1)
                       \y : - - x . cl x y : - - x -> x
                                     /                     Ax
                   \y : - - x . cl x y : - - x -> x       P : T
                  ---------------------------------------------- (all T i - 2)
                       \ x : P . \y : - - x . cl x y : CL,

where D_1 is


  x : P          void : P                          D_v
 ------------------------- (P P Formation - v)
          - x : P                                void : P
         ------------------------------------------------- (P P Formation - v)
                             - - x : P.

A deduction on which both of these replacements have been made systematically 
in all possible places will be called PREPARED.  (Note that in preparing a 
deduction, we replace terms in which cl occurs by terms to which they are 

     Now consider in a prepared deduction a sample subdeduction of the form


               cl : CL     A : P                   D_2
              ------------------- (all e)
               cl A : - - A -> A                M : - - A
              -------------------------------------------- (all e)
                               cl A M : A.

Since there is a subdeduction of A : P, A is a type; hence, it is either 
simple or compound.

     The strategy is to follow the idea of Prawitz [1965] for classical logic, 
and eliminate occurrences of subdeductions like those above in which A is 
compound.  Thus, assume A is (all y : B)C.  We need a lemma:

     LEMMA 3.1.  Let Gamma be a valid environment, and suppose that

                               Gamma |- A : X,

where A conv (all y : B)C and X conv kappa.  Then

        Gamma |- B : kappa'      and       Gamma, y : B |- C : kappa.

     Proof.  A straightfowrard induction on a normalized deduction of 

                               Gamma |- A : X.

     Now by this lemma and D_1 above, it follows that there are deductions

                                                         y : B
                                    and                  D_4(y)
            B : kappa 
                                                         C : P.

Then we can transform 


               cl : CL     A : P                   D_2
              ------------------- (all e)
               cl A : - - A -> A                M : - - A
              -------------------------------------------- (all e)
                               cl A M : A

into the following:


                 [y : B]     D_3             D_5             D_2        1

                   D_4    B : kappa, \y:B.C : (all y:B)P, M : - - A, [y : B]

  cl : CL         C : P                   D_6(B,\y:B.C,M,y)
 ----------------------- (all e)
   cl C : - - C -> C                   T(B,\y:B.C,M,y) : - - C
  ------------------------------------------------------------- (all e)
                      cl C T(B,\x:B.C,M,N) : C
                          /                         D_3
            cl C T(B,\x:B.C,M,N) : C             B : kappa
           ------------------------------------------------ (all kappa i - 1)
              \y:B . cl C T(B,\x:B.C,M,N) : (all x : B)C,

where where D_5 is


                    [y : B]

                     D_4(y)           D_3

                     C : P         B : kappa
                    ------------------------- (all kappa i - 2)
                       \y:B.C : (all y:B)P,

T(u',v',u,v) is

                \w : -v'v . u(\y : (all x : u')(v'x) . w(yv)),

and D_6(u',v',u,v) is the obvious normalized deduction of

     u' : kappa, v' : (all x : u')P, u : - - (all x : u')(v'x), v : u' |-

                        T(u',v',u,v) : - - v'v.

     In the special case in which A is the type void, we have a special 
transformation:  we replace


     cl : CL           void : P                    D_1
    ---------------------------- (all e)
     cl void : - - void -> void                M : - - void
    -------------------------------------------------------- (all e)
                        cl void M : void


                                1                 D_v

          D_1               [x : void]          void : P
                           ------------------------------ (P P Formation - 1)
      M : - - void             \x : void . x : - void
     ------------------------------------------------- (all e)
                  M (\x : void . x) : void.

     If we repeatedly apply these transformations to a deduction, we will 
eventually reach a point at which in all occurrences of a part of a deduction 
of the form


               cl : CL     A : P                   D_2
              ------------------- (all e)
               cl A : - - A -> A                M : - - A
              -------------------------------------------- (all e)
                               cl A M : A,

A is a simple type.  Of course, this will have replaced terms of the form 
cl A M for compound types A of the form (all y : B)C by 
\y:B . cl C T(B,\x:B.C,M,N) and cl void M by M (\u : void . u).  If we repeat 
these replacements, we will eventually eliminate all occurrences of the 
assumption cl : CL.  This will change both the premises and the conclusion; 
>from a deduction of Gamma, cl : CL |- M : A, we will get a deduction of 
Gamma' |- M* : A', where Gamma' and A' are obtained from Gamma and A by 
replacing certain small simple types B by - - B and changing some of the 
terms.  Note that all the terms so changed have occurrences of cl in them; it 
follows from the subject-construction property (see [Hindley & Seldin [1986, 
Notes 14.18 and 15.12 and Remark 16.37] and Seldin [1987, p. 301]; it says 
that a deduction follows the construction of the term) that if a term without 
an occurrence of cl occurs in a type in Gamma or A, then that term is 
unchanged, and so is any type to which it is proved in the deduction to 
belong.  These terms occurring in the types of Gamma or A will be called TYPE 

     Since it is trivial to prove in constructive logic A |- - - A, we can put 
all this in the form of the following theorem:

     THEOREM 3.  If there is a deduction of Gamma, cl : CL |- M : A, and if 
Gamma' and A' are obtained from Gamma and A by 1) replacing every simple small 
type B by - - B provided that B occurs in Gamma or in A but does not occur 
inside an occurrence of the type void or in the type of a type argument in 
which cl does not occur, and 2) by changing type arguments in which cl does 
occur, then for some term M* there is a deduction of Gamma' |- M* : A'.

     Now suppose we have a deduction cl : CL |- M : void (where Gamma is 
empty).  Then by the theorem, there is a deduction D of |- M : void.  Since 
there is no such deduction (by the normalization theorem), this gives us the 
following proof of Coquand's consistency result:

     COROLLARY 3.1.  Classical logic is consistent in the calculus of con-

5.  Classical arithmetic

     In Seldin [1987, Chapter 5], it is shown that intuitionistic arithmetic 
can be obtained by adding the two assumptions

                peano1 : (all n : Nat)(- Q Nat (succ n) zero),

  peano2 : (all n : Nat)(all m : Nat)(Q Nat (succ n) (succ m) -> Q Nat n m).

There is no need for induction because of the the predicate Isnat, which is 
defined to be

\n : Nat . (all A : Nat -> Prop)((all m : Nat)(A m -> A (succ m)) -> A zero -> 
                                    A n).

Then the induction axiom follows for terms of which Isnat is true; in fact, 
this definition is essentially the way Dedekind proved induction.  This is why 
peano1 and peano2 are sufficient for arithmetic.

     In fact peano1 is sufficient.  We can derive a version of peano2 relative 
to Isnat using the predecessor defined in Seldin [1987, Definition 5.7] as 

     LEMMA 4.1.  For some term M,

          |- M : (all n : Nat)(Isnat n -> Q Nat (pred (succ n)) n).

     Proof.  A direct calculation gives that pred (succ (succ n)) converts to 
succ (pred (succ n)).  Hence, there is M_1 such that

  n : Nat, x : Q Nat (pred (succ n)) n |- M_1 : Q Nat (pred (succ (succ n))) 
                                  (succ n).

Hence, by (all P i), there is M_2 such that

|- M_2 : (all n : Nat)(Q Nat (pred (succ n)) n -> Q Nat (pred (succ (succ n))) 
                                  (succ n)).

This is the induction step.  The basis is easy, since pred zero converts to 
zero.  Then induction (which follows from the definition of Isnat) gives us 
the Lemma.

     LEMMA 4.2.  For some term M,

   |- M : (all m : Nat)(all n : Nat)(Isnat m -> Isnat n -> (Q Nat (succ m) 
                          (succ n)) -> (Q Nat m n)).

     Proof.  We can easily formalize in this logic the following argument, 
where m = n represents Q Nat m n:  succ m = succ n, therefore 
pred (succ m) = pred (succ n), and so m = n.

     Hence, to prove classical arithmetic consistent, it is enough to prove 
that cl : CL, peano1 : (all n : Nat)(- Q Nat (succ n) zero) is consistent.

     THEOREM 4.  Let Gamma be a strongly consistent environment in which all 
simple types which have universal prefixes are large.  Then

        Gamma, cl : CL, peano1 : (all n : Nat)(- Q Nat (succ n) zero)

is consistent.

     Proof.  Suppose there is a term M such that

  Gamma, cl : CL, peano1 : (all n : Nat)(- Q Nat (succ n) zero) |- M : void.

Then by Theorem 3, there is a term M' such that

    Gamma', peano1 : (all n : Nat)(- (all z : Nat -> P)(- - z (succ n) -> 
                          - - z zero)) |- M' : void. 

It is not hard to see that Gamma' is strongly negation consistent.  Now in a 
normal deduction of

      Gamma', p1 : (all n : Nat)(- (all z : Nat -> P)(- - z (succ n) ->
                          - - z zero)) |- M' : void,

the top of the left branch must be 

    p1 : (all n : Nat)(-(all z : Nat -> P)(- - z (succ n) -> - - z zero)), 

and the minor premise for an inference by (all e) is

            Q : (all z : Nat -> P)(- - z (succ U) -> - - z zero),

where there is an assumption U : Nat.  This is proved impossible by the 
following lemma.

     LEMMA 4.3.  If Gamma is strongly negation consistent, and if for some 
term M

       Gamma, p1 : (all n : Nat)(- (all z : Nat -> P)(- - z (succ n) ->
          - - z zero)) |- M : (all z : A -> P)(- - z R -> - - z S),

then R converts to S.

     Proof.  Assume that D is a normalized deduction as in the lemma and that 
there is no proper subdeduction of something of this form (where this 
condition is considered to be universally quantified over strongly negation 
consistent environments Gamma).  If the last inference in D is (all e), then 
the top of the left branch must be

   p1 : (all n : Nat)(- (all z : Nat -> P)(- - z (succ n) -> - - z zero)), 

and then the deduction ending in the minor premise violates the assumptions 
about D.  In fact, this shows that

    p1 : (all n : Nat)(- (all z : Nat -> P)(- - z (succ n) -> - - z zero))

cannot occur anywhere in D at the top of the left branch, and, since D is 
normal, this implies that it is not used in the deduction.  It follows (by 
repeating this argument about subdeductions ending in (all e)) that we can 
decompose D until we have a deduction of

            Gamma, z : A -> P, u : - - z R, v : - z S |- Q : void.

By Theorem 2, this is only possible if R converts to S.


Coquand, Thierry [forthcoming], "Metamathematical investigations of a calculus 
of constructions", forthcoming.  (This paper should not be confused with the 
other paper by Coquand of the same name privately circulated by the author 
dated February 9, 1987, and cited in Seldin [in preparation 1]).

Hindley, J. R. & Seldin, J. P. [1986],  "Introduction to Combinators and 
Lambda-Calculus", London Math. Soc. Student Texts 1, Cambridge University 

Pottinger, Garrel [1989]  "Definite descriptions and excluded middle in the 
theory of constructions", TYPES network, 6 November 1989.

Prawitz, Dag [1965]  "Natural Deduction", Almqvist & Wiksell, 1965.

Seldin, J. P. [1987]  "MATHESIS:  the mathematical foundation of ULYSSES", 
Interim Report RADC-TR-87-223 (November 1987), Rome Air Development Center 
(actually published in 1988).

Seldin, J. P. [in preparation 1]  "Coquand's Calculus of Constructions:  a 
mathematical foundation for a proof development system".

Seldin, J. P. [in preparation 2]  "On the proof theory of Coquand's calculus 
of constructions".