[Prev][Next][Index][Thread]
Descriptions, Excluded Middle, and Constructions
Date: Mon, 6 Nov 89 18:18:58 EST
Definite Descriptions and Excluded Middle in the Theory of Constructions
Garrel Pottinger
Odyssey Research Associates , Inc.
301A Harris B. Dates Drive
Ithaca, New York 14850-1313
oravax!garrel@cu-arpa.cs.cornell.edu
Personal thanks: Thierry Coquand and Jonathan Seldin were
kind enough to read the first draft of this document and
comment on it. It is a pleasure to acknowledge their help,
while, of course, absolving them of responsibility for
errors or infelicities which may be found below.
Acknowledgement of Sponsorship: The research which produced
the information contained in this document was sponsored, in
whole or in part, by the U. S. Air Force Systems Command, Rome
Air Development Center, Griffis AFB, New York 13441-5700 under
Contract No. F30602-85-C-0098.
1. Introduction
A definite description is a phrase such as "the present Queen of England",
"the present Queen of France", "the President of the United States during
the twentieth century", "the President of the United states during September
1989", "the even prime", "the even prime greater than 2", "the odd prime
greater than 2" [Russell 1905]. Definite descriptions are used freely in
the language of ordinary mathematics, including constructive mathematics.
For example, if we have proved that there is a unique, smallest prime between
n + 1 and n! + 1, inclusive, we may legitimately define a function f by
specifying that f n = the smallest prime between n+1 and n! + 1, inclusive.
Although we use definite descriptions in ordinary mathematics without
making many mistakes, describing their logical behavior is a tricky business.
A definite description purports to refer to a unique object, and when, in
fact, exactly one object has the property involved in the description,
we know what to say --- if there is a unique object which F's, then
the thing that F's F's. But we must also figure out what (if anything) to
assert when either no object is described or more than one is.
Various reactions to this problem (and others which descriptions may raise,
depending on the expressive power of the language in which they are embedded)
are possible, and a host of formal theories of descriptions have resulted.
(The literature on this subject is vast. See [Pottinger 1988b] for a cursory
look at some of the theories and entry points to the literature.)
If we are only interested in formalizing mathematical arguments and our
logic is first order (classical or intuitionist), we can avoid the
complications descriptions bring with them by using the well-known
techniques for eliminating descriptions from first order languages
[Kleene 1950, section 74] to handle informal function definitions
like the one considered in the first paragraph of this document.
But these techniques are sensitive to certain features of the
syntax of first order languages and may fail for a language with
a richer syntax. Indeed, they do fail for the theory of constructions.
Consequently, if we are to use the theory of constructions as a logic for
formalizing ordinary mathematics, we must introduce definite descriptions.
Moreover, we may also want to avail ourselves of classical logic. The sequel
shows that there is a serious conflict involved in combining these two
extensions of the theory of constructions, if descriptions are introduced in
what seems to be the most natural manner. We show that, in the presence of
unrestricted descriptions and excluded middle, it follows that every
proposition has at most one proof (where "proposition" and "proof" are
understood in the technical senses explained below). Since the set of
natural numbers, the set of lists built over a given set of objects, etc.
are usually represented as propositions in the theory of constructions and
a proposition is, essentially, the set of its proofs, we cannot formalize
mathematics on such a basis.
Analysis of the argument which leads from unrestricted descriptions and
excluded middle to the conclusion that every proposition has at most
one proof shows that it depends on the fact that descriptions allow us
to define certain functions from the type of all propositions to a given
proposition. We also present a restricted formalism for descriptions
in the theory of constructions which blocks this argument, while retaining
much of the expressive power which motivated their introduction.
The research reported here was stimulated by [Coquand forthcoming].
The fact that classical logic is used in the security theory of
Romulus [ORA staff 1988a, ORA staff 1988b] and Romulus is based on
the theory of constructions lent piquancy to the work. (Romulus
was formerly called "Ulysses".)
2. TOC
Since a number of different formal systems have been used in developing
the theory of constructions and since the results presented here depend
on the exact details of the system considered, we begin by defining the
formal system called "TOC" in this document. This system seems to be a
way of writing down the stable core of the various calculi of constructions
discussed by Coquand, Huet, and others.
Terms are built up from the logical constants P, T, iota, iota_in,
a denumerable stock of non-logical constants (also called "parameters"),
and a denumerable stock of variables by means of application, type-labelled
lambda-abstraction, and type-labelled universal quantification. The
constant P represents the type of propositions and T is the type of
large types, of which P is an element. The constants iota and iota_in
will be used when descriptions are introduced, below.
In what follows pi, rho, sigma, pi_1, ... are to be parameters, a, b, c, f,
g, h, l, m, n, p, q, r, w, x, y, z, a_1, ... are to be variables, and A, B, C,
F, G, H, L, M, N, X, Y, Z, A_1, ... are to be terms. Also, kappa, kappa_1, ...
are to be either P or T.
In terms of the forms \ x : Y . X and all x : Y . X, the variable binder
binds the free occurrences of x in X but binds nothing in Y. Terms which
would ordinarily be said to be the same up to alphabetic change of bound
variables will be identified. (Our official view is that they are literally
the same term [Pottinger 1988a].)
A term of the form (\ x : Y . X) Z is a redex, and it contracts to
Sub[ Z / x / X ] (i.e., the result of substituting Z for x in X). Given
this, conversion is defined as usual.
Formulas have the form X : Y. In what follows, E, F, G, E_1, ... are to
be formulas and Gamma, Delta, Theta, Xi, Gamma_1, ... are to be finite
sequences of formulas. Sequents have the form Gamma |- E. (We note that,
although in principle Gamma can contain arbitrary formulas, the rules
of the system insure that if Gamma |- E is derivable, then, in fact,
Gamma has the form pi_1 : X_1 , ... , pi_n : X_n.)
Axioms:
|- P : T
Structural rules:
Gamma |- A : kappa
------------------------ Hyp
Gamma , pi : A |- pi : A
provided no item of Gamma has the form pi : B.
Gamma |- E Gamma , F |- G
----------------------------- Reit
Gamma , F |- E
Remark: Hyp and Reit differ from Coquand's rules for extending Gamma and
using formulas in Gamma, but it is easy to show that the present system
is equivalent to one where Hyp and Reit are replaced by Coquand's rules
[Pottinger 1988a]. Apart from the fact that it is written down using
sequents, rather than subderivations, the system defined here is presented
in the style of [Fitch 1952].
Operational rules:
Gamma , pi : A |- B : kappa
---------------------------------------------- allF
Gamma |- all x : A . Sub[ x / pi / B ] : kappa
Remark: "F" is short for "Formation".
Gamma , pi : A |- M : B
-------------------------------------------------------------------- allI
Gamma |- \ x : A . Sub[ pi / x / M ] : all x : A . Sub[ x / pi / B ]
provided B is not T.
Remark: Note that this is the comprehension rule in TOC --- i.e., the
rule that enables us to prove that functions exist. When we add descriptions
and excluded middle, it is the interplay between allI and descriptions which
we will have to be careful about.
Gamma |- M : all x : A . B Gamma |- N : A
--------------------------------------------- allE
Gamma |- M N : Sub[ N / x / B]
Gamma |- M : A A conv B Gamma |- B : kappa
-------------------------------------------------- :conv
Gamma |- M : B
Having completed the definition of TOC, we classify the term A as a
Gamma-proposition if, and only if, Gamma |- A : P is derivable, and
we call X a Gamma-proof if, and only if, for some Gamma-proposition
A, Gamma |- X : A is derivable.
Next we introduce the abbreviations needed for convenient statement of
axioms and rules for descriptions. Let FV X be the set of free variables
of X.
A -> B = all x : A . B, where x not in FV B.
A & B = all p : P . (A -> B -> p) -> p
Sigma A = \ f : A -> P . all p : P . (all x : A . f x -> p) -> p, where
p not in FV A.
exists x : A . B = Sigma A (\ x : A . B)
Q A = \ x : A . \ y : a . all f : A -> P . f x -> f y, where x,y not in
FV A.
exists! x : A . B = exists x : A . B & all y : A . Sub[ y / x / B] -> Q A y x,
where x not in FV A and y not in (FV A) Union (FV B).
3. TOC with descriptions
TOCD arises from TOC by adding the following axioms.
|- iota : all p : P . all f : p -> P . (exists! x : p . f x) -> p
|- iota_in :
all p : P . all f : p -> P . all m : (exists! x : p . f x). f (iota p f m)
The axiom for iota is harmless. The one for iota_in is the thing we must
keep our eye on, because it tells when the thing that f's f's.
That's ALWAYS the main thing to know about a theory of descriptions.
Note that if we say that for every f, the thing that f's f's, we will wind
up asserting things like "The natural number which is both odd and not odd
is both odd and not odd".
It is necessary to make the value of iota depend on m because TOC is
constructive. We can't expect, in general, to have a function which returns
the unique thing of type p which has f, given simply p and an f which just
happens to hold for exactly one object of type p.
Note that we can easily interpret TOCD in TOC by mapping a sequent
Gamma |- E to Theta , Gamma' |- E', where Theta simply assigns appropriate
types to parameters representing iota and iota_in and the primes indicate
that we have fussed around with Gamma and E to reflect this way of
representing iota and iota_in.
4. Proof degeneracy
We turn now to the demonstration that in TOCD excluded middle yields
the conclusion that every proposition has at most one proof. In addition
to the abbreviations given above, we require the following.
absurd = all p : P . p
- A = A -> absurd
A + B = all c : P . (A -> c) -> (B -> c) -> c
A <-> B = (A -> B) & (B -> A)
Also, we use Gamma ||- E to indicate that the sequent Gamma |- E is derivable,
and Gamma >> A means that for some M, Gamma ||- M : A.
Lemma 4.1 [Coquand]: In TOC, if Gamma ||- A : P, Gamma ||- F : A -> P,
Gamma ||- G : P -> A, and Gamma >> all p : P . p <-> F (G p), then
Gamma >> absurd.
The proof of lemma 4.1 involves showing how to interpret the inconsistent
system U of [Girard 1972] in such a Gamma [Coquand forthcoming, p. 19].
Coquand uses the lemma to show that in the theory of constructions
excluded middle and the assumption that every proof of a direct sum
arises by injection from a proof of one of the summands or the other
imply that every proposition has at most one proof. (Coquand presents
this result by introducing a primitive direct sum with the property
just mentioned. The statement of his theorem given here provides
a way of expressing it via the internally definable direct sum.)
We adapt Coquand's argument to show that in TOCD excluded middle leads
to the conclusion that every proposition has at most one proof. Note that,
although there is no particular reason to assume that every proof of a direct
sum arises via injection when we are dealing with a classical version of
the theory of constructions, there are good reasons for wanting to have
definite descriptions whenever we are using the theory of constructions as a
logic for formalizing mathematics. Consequently, the following theorem
shows exactly where the shoe pinches when the mathematics being
formalized is classical.
Theorem 4.2: In TOCD, if Gamma ||- X : all p : P . p + - p, then
Gamma >> all q : P . all x : q . all y : q . Q q x y.
Proof: We consider Gamma' = Gamma , pi_q : P , pi_x : pi_q , pi_y : pi_q and
show Gamma' >> Q pi_q pi_x pi_y. Given the lemma, it suffices to let A be
pi_q, show how to define F and G in Gamma', and prove
Gamma' , pi_w : - Q pi_q pi_x pi_y >> all p : P . p <-> F (G p).
We let F = \ z : pi_q . Q pi_q z pi_x.
As for G, note first that in Gamma', we can use X to construct
an M s.t.
M : all p : P . exists! z : pi_q .
(p & (Q pi_q z pi_x)) + (- p & (Q pi_q z pi_y))
Let H = \ z : pi_q .
(p & (Q pi_q z pi_x)) + (- p & (Q pi_q z pi_y)),
and note that, in Gamma', conversion gives us
M : all p : P . exists! z : pi_q . H z
We define G = \ p : P . iota pi_q H (M p).
With F and G in hand, we proceed to the proof that
Gamma' , pi_w : - Q pi_q pi_x pi_y >> all p : P . p <-> F (G p). Let
Gamma'' be Gamma , pi_w : - Q pi_q pi_x pi_y , pi_p : P.
Note that by what has already been done, in Gamma'' we have
iota_in pi_q H (M pi_p) : H (iota pi_q H (M pi_p))
and conversion gives
(*) Gamma'' >>
(pi_p & (Q pi_q (G pi_p) pi_x)) + (- pi_p & (Q pi_q (G pi_p) pi_y))
First, arguing in Gamma''' = Gamma'' , pi_v : pi_p, we show F (G pi_p).
Given pi_v and (*), we have Q pi_q (G pi_p) pi_x. This converts to F (G pi_p),
so Gamma''' >> F (G pi_p).
Now we let Gamma''' = Gamma'' , pi_v : - pi_p and show - F (G pi_p), which,
since we have excluded middle, will complete the argument.
In this Gamma''', pi_v and (*) give us Q pi_q (G pi_p) pi_y, from which
we can deduce Q P (F (G pi_p)) (F pi_y). The right hand side of the
latter equality converts to Q pi_q pi_y pi_x. Since pi_w gives us
- Q pi_q pi_y pi_x, it follows that Gamma''' >> - F (G pi_p).
5. TOC with weak descriptions
The crux of the proof of theorem 4.2 is the definition of G, which involves
an abstraction over P where the variable of abstraction occurs free in a
term which is the third argument of iota_in. Abstraction of this sort also
leads to the following theorem, which we state without proof.
Theorem 5.1: In TOCD, if Gamma ||- all x : A . exists! y : B . F x y : P
and Gamma ||- B : P, then
Gamma >> (all x : A . exists! y : B . F x y)
-> exists g : A -> B . all x : A . F x (g x).
Now, although apparently weaker than iota and iota_in together,
it turns out that adding the rule corresponding to theorem 5.1 to TOC
is enough, in the presence of excluded middle, to make the demonstration
that every proposition has at most one proof work. The CRUCIAL
point is that, although B must be a Gamma-proposition, A need not
be. In particular, A may be P, which is what happens in the proof
degeneracy argument. We construct TOC with weak descriptions so as
to block the sort of abstraction involved in proving theorem 4.2 and
the unrestricted form of theorem 5.1.
TOCWD is obtained from TOC by proceeding as follows.
Add the axiom for iota to TOC, as in TOCD.
Add the rule:
Gamma |- A : P Gamma |- F : A -> P Gamma |- M : exists! x : A . F x iotaI
-----------------------------------------------------------------------
Gamma |- iota_in A F M : F (iota A F M)
provided x not in FV F.
Remark: Note that we have given iota_in A F M a type, but we have NOT given
iota_in a type. That's inevitable. The only type iota_in could have is
the one shown in the TOCD axiom for this operator, and if iota_in has that
type, then, in view of the representation of TOCD in TOC noted at the
end of section 3, we're cooked.
Split allI into two cases, as follows.
Gamma , pi : A |- M : B Gamma |- A : T
-------------------------------------------------------------------- allI
Gamma |- \ x : A . Sub[ pi / x / M ] : all x : A . Sub[ x / pi / B ]
provided (1) B is not T and (2) there is no subterm iota_in A_1 F M_1
of M s.t. pi occurs in M_1.
Gamma , pi : A |- M : B Gamma |- A : P
-------------------------------------------------------------------- allI
Gamma |- \ x : A . Sub[ pi / x / M ] : all x : A . Sub[ x / pi / B ]
provided B is not T.
6. Concluding remarks
It is certain that the proof degeneracy argument discussed above cannot be
carried out in TOCWD. But, of course, that does not show that no argument
formalizable in TOCWD establishes proof degeneracy. Coquand has suggested
in correspondence that one may be forthcoming via the recently proved
inconsistency of the system U- of [Girard 1972].
If, in fact, there is no such argument, it's very likely that we're going
to need a model to prove it. We conclude by asking whether anybody has
one which will do the job.
7. References
[Coquand forthcoming]
Thierry Coquand, "Metamathematical Investigation of a Calculus of
Constructions", forthcoming.
[Fitch 1952]
Fredric Brenton Fitch, Symbolic Logic, the Ronald Press Company, New
York, 1952.
[Girard 1972]
Jean-Yves Girard, Interpretation Fonctionelle et Elimination des
Coupures de l'Arithmetique d'Order Superieur, thesis, University of
Paris VII, June 1972.
[Kleene 1950]
Stephen Cole Kleene, Introduction to Metamathematics, D. van Nostrand
Company, Princeton, 1950.
[ORA staff 1988a]
ORA staff, "Ulysses: A Computer-security Modeling Environment",
in Proceedings of the 11th National Computer Security Conference,
September 1988.
[ORA staff 1988b]
ORA staff, "Security Modeling in the Ulysses Environment", in Fourth
Aerospace Computer Security Conference, December 1988.
[Pottinger 1988a]
Garrel Pottinger, "Ulysses: Logical and Computational Foundations of
the Primitive Inference Engine", technical report TR 11-8, Odyssey
Research Associates, January 1988.
[Pottinger 1988b]
Garrel Pottinger, "Ulysses: Logical Foundations of the Definition
Facility", technical report TR 11-9, Odyssey Research Associates,
January 1988.
[Russell 1905]
Bertrand Russell, "On Denoting", Mind, 1905. Reprinted in Robert C.
Marsh, Logic and Knowledge, George Allen & Unwin, London, 1956, pp. 41-56.