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

[Kalani Thielen]

I've seen negation interpreted as continuations (not A = A -> bottom).  Maybe this paper will be helpful:

http://www.cs.rutgers.edu/~ccshan/polar/paper.pdf

With your example, I believe that x:A and y:not A, A&(not A) = A&(A -> bottom) can be "reduced" in the way that you suggest by applying y to x (yielding bottom -- i.e.: giving the continuation what it wants).

Hope this helps (and/or more qualified people can explain in more detail).



-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Xuhui Li
Sent: Thursday, May 20, 2010 10:57 PM
To: types-list at lists.seas.upenn.edu
Subject: [TYPES] what does a negative proposition represent in type theory?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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