[TYPES] what does a negative proposition represent in type theory?
xhli06 at 163.com
Thu May 20 22:56:55 EDT 2010
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