[Prev][Next][Index][Thread]

Function construction principle in calculus of constructions

Date: Wed, 23 Oct 91 22:32:41 -0400

 ON THE FUNCTION CONSTRUCTION PRINCIPLE IN COQUAND'S CALCULUS OF
			  CONSTRUCTIONS

				
		       Jonathan P. Seldin
		    Department of Mathematics
		      Concordia University
			Montreal, Quebec
		    seldin@alcor.concordia.ca


	By the function construction principle, I mean

(all x : A)(exists ! y : B)(F x y)  -> 
			(exists g : A -> B)(all x : A)(F x (g x))

Pottinger (private communication) proves that in the presence of
excluded middle, adding this assumption to Coquand's calculus of
constructions leads to ``proof degeneracy'', which says that,
using the equality defined by the Leibniz property, any two terms
in a small type can be proved equal.  The proof is based on a
proof by Coquand [1] that adding both the strong existential type
and excluded middle to the calculus of constructions leads to
proof degeneracy.  Since the type of the natural numbers is a
small type, proof degeneracy implies that all natural numbers are
provably equal, and is thus undesirable.  Pottinger has expressed
(private communication) some surprise at this incompatibility of
the function construction principle and excluded middle in the
calculus of constructions.  However, the result of Coquand on the
strong existential type is not surprising at all, since the
strong existential type, which has pairs as members and also a
right projection, guarantees a term as a witness for anything
proved to exist, and this implies the existential property, which
is known to be a property of constructive logic incompatible with
classical logic.  Similarly, I believe that if we look at the
function construction principle in the right way, its
incompatibility with excluded middle in the calculus of
constructions is not really such a surprise.

	The antecedent of the principle,

	       (all x : A)(exists ! y : B)(F x y),

is a formula of pure logic that asserts nothing about the term
structure on which the calculus of constructions is based.  On
the other hand, the consequent,

	    (exists g : A -> B)(all x : A)(F x (g x)),

uses the application operation of this term structure in an
essential way to denote the value of the function it asserts to
exist, and it thus ties itself to what is true this term
structure.  (It also ties itself to the term structure by
asserting that the function in question is in an arrow type.)
Now the term structure is fixed and independent of any logical
assumptions that may be made.  In the presence of excluded
middle, the true instances of the antecedent will be uncountable
for certain types A and B (types which have countably many
terms); the term structure, however, remains countable.  For this
reason alone, we should expect the function construction
principle to be incompatible with excluded middle.

	If anything is surprising, it should be that there is some
evidence that if excluded middle is not assumed, and if the other
assumptions are suitably limited, then the function construction
principle is consistent.  That evidence is a consequence of the
strong normalization theorem for deductions.  That theorem is
proved in [2] for a formulation of the calculus of constructions
in which deductions assigning types follow the constructions of
the terms to which types are assigned.  In a normalized
deduction, if the last rule is the rule of universal elimination
[also called the rule of appliclation], then the only inferences
in the main branch of the deduction are by this rule or the rule
of conversion.  It follows that the formula at the top of that
branch cannot be discharged in the deduction.

	This fact is related to the consistency of assumptions as
follows:  since void is defined to be (all x : Prop)x, given a
deduction of Gamma |- N : void, by taking a new variable x and
adding x : Prop as a new assumption and using the rule of
universal elimination, one obtains a deduction of Gamma, x : Prop
|- Nx : x.  Thus, proving that there is no deduction of Gamma |-
N : void for a set of assumptions Gamma is equivalent to proving
that for a variable x not in Gamma there is no deduction of
Gamma, x : Prop |- M : x, and from the normalization theorem that
there is no normalized deduction of this.  Now in a normalized
deduction ending in M : x for a variable x, the last rule must be
the rule for universal elimination, and the formula at the top of
the left branch must be in Gamma.  If Gamma can be restricted to
formulas that cannot occur in this position, then one can
conclude that Gamma is a consistent set of assumptions.

	In [3] and [4], I define a strongly consistent
environment to be an environment whose assumptions satisfy
conditions which make it impossible for any of them to occur at
the top of the main branch of a deduction ending in M : x.
Strongly consistent environments are very restricted, and cannot
include types of the form A and B, A or B, not A, void, or M
eq(A) N [given their standard definitions].  If all the
assumptions of a deduction form a strongly consistent
environment, then the logic used is constructive.

	The evidence mentioned above is the following result:

	Theorem.  Suppose Gamma, x : A is a strongly consistent
environment.  If

	    Gamma |- (all x : A)(exists y : B)(F x y)

then there is a term G such that

		       Gamma |- G : A -> B

and

		Gamma |- (all x : A)(F x (G x)).

	The proof depends on the constructive existence property.

	To use the function construction principle with classical
logic probably requires a new notion of function to be defined
(say, for example, a property of ordered pairs) with an
application operation defined by the logic rather than the
underlying term structure.


			      REFERENCES

[1] T. Coquand, Metamathematical investigations of a calculus of
constructions, in Logic and Computer Scence (ed. P. Odifreddi),
Academic Press (Apic Series 31), 1990.

[2] J. P. Seldin, MATHESIS: the Mathematical Foundation for
ULYSSES, Technical report RADC-TR-87-223 (November 1987, actually
published in 1988, prepared for Odyssey Research Associates),
Chapter 4.

[3]  J. P. Seldin, Coquand's calculus of constructions:  a
mathematical foundation for a proof development system, Formal
Aspects of Computing, to appear.

[4]  J. P. Seldin, Excluded middle without definite descriptions
in the theory of constructions (extended abstract), Proceedings
of the Montreal Workshop on Programming Languages, Concordia
University, Montreal, April 29-30, 1991, to appear.