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

[Xuhui Li]

Hi, All
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?
 
Thanks.
 
Xuhui