[TYPES] what does a negative proposition represent in type theory?

[Uday S Reddy]

Xuhui Li writes:

> In type theory there is a proper correspondance between compound propositions
> and types, such as A & B, A -> B. However, what does a negative proposition
> like "ØA" mean? What is an element of the type "ØA"? Further, suppose x:A and
> y:ØA, is there certain rules to reduce x and y just like reduce A&ØA
> in  logic system?

If you are talking about intuitionistic type theory, then not(A) is
just a short hand notation for A -> false.  Everything else follows
from that.

Cheers,
Uday Reddy