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

Xuhui Li xhli06 at 163.com
Thu May 20 22:56:55 EDT 2010

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?

More information about the Types-list mailing list