[Prev][Next][Index][Thread]
Extensions to Theory of Constructions (734 lines)
Date: Wed, 27 Sep 89 11:22:41 EDT
EXCLUDED MIDDLE WITHOUT DEFINITE DESCRIPTIONS IN THE THEORY OF CONSTRUCTIONS
Jonathan P. Seldin
Department of Mathematics
Concordia University
7141 Sherbrooke Street West
Montreal, Quebec, H4B 1R6
Canada
seldin@antares.concordia.ca
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
suggestions.
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,
namely
(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,
(Eq")
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-
TENT.
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
D_1
u : - B M" : B
-------------------------- (all e)
uM" : void
D_2
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'
D_3
u' : - B' M''' : B'
------------------------------ (all e)
u'M''' : void
D_4
M' : w,
where B' is simple or the negation of a simple type. But then
w : P, u : - B, u' : - B'
D_3
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
D_1
u : - - B M" : - B
----------------------------- (all e)
uM" : void
D_2
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
1
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:
D_1
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
D_1
cl : CL A : P
------------------- (all e)
cl A : - - A -> A,
where the conclusion is not a major premise for (all e), by
D_1
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
n
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
D_v
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
"eta"-convertible.)
Now consider in a prepared deduction a sample subdeduction of the form
D_1
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
D_3
and D_4(y)
B : kappa
C : P.
Then we can transform
D_1
cl : CL A : P D_2
------------------- (all e)
cl A : - - A -> A M : - - A
-------------------------------------------- (all e)
cl A M : A
into the following:
1
[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
2
[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
D_v
cl : CL void : P D_1
---------------------------- (all e)
cl void : - - void -> void M : - - void
-------------------------------------------------------- (all e)
cl void M : void
by
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
D_1
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
ARGUMENTS.
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-
structions.
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
follows:
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.
References
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
Press.
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".