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

[Avik Chaudhuri]

Following up on Noam's comments, complementary types indeed seem to be  
quite useful for logical reasoning about programs (e.g., in scripting  
languages with typecase). A subtyping of the form A < ~B can be  
particularly useful. This logically means A \cap B = \emptyset, and is  
equivalent to B < ~A. In "program analysis" terminology, it means that  
values of type A cannot alias values of type B.

-Avik.

On May 21, 2010, at 5:25 PM, Noam Zeilberger wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> Well yes you're right that there are other interpretations of negation
> -- I wasn't sure what you were looking for!  With this clarification,
> I think the question you are asking is really at the "extrinsic" or
> "refinement type" level (related to intersection and union types,
> etc.).
>
> Before we can get there, we need to start at the intrinsic level.
>
> Let's say that a type A denotes some set of values.
> At this level, the standard interpretation of negation is as building
> the set of continuations, i.e., the type ~A denotes the set of
> continuations for A with answer type _|_.
>
> Given a value V : A and a continuation K : ~A, we can combine them to
> produce a "contradiction" K $ V : _|_, in other words just a program
> that computes an answer (of type _|_) by passing V to K.
>
> But you're interested in a different notion of
> negation-as-complementation, so let's continue...
>
> At the extrinsic level, we consider *refinements* S,T of A, which can
> be interpreted as subsets, or properties of A-values.  For example, if
> A = naturals, we can define S = primes, T = evens, etc.  And now, yes,
> it makes sense to consider an additional, very different form of
> negation (which I'll write -) as complementation.  The refinement type
> -S denotes a set of values, rather than a set of continuations: the
> set of A-values which don't satisfy S.
>
> Now, how does non-contradiction fit in?  Well, there is certainly no
> contradiction about a type like S \times -S: as you said, e.g., this
> could simply denote pairs of prime and non-prime numbers.  However, at
> the extrinsic level we can also consider "logical conjunction" as
> intersection rather than product.  And the type S \cap -S is
> contradictory in a very concrete sense: it denotes the set of A-values
> which both satisfy S and don't satisfy S -- in other words the empty
> set.
>
> Noam
>
> On Fri, May 21, 2010 at 4:01 PM, Xuhui Li <xhli06 at 163.com> wrote:
>> Hi Noam,
>>
>> Thanks for your patient reply. Sorry for the wrong "negation"  
>> symbol that
>> confused you.
>>
>> I know that ~A can be defined as A->_|_. However, this  
>> interpretation is not
>> "intuitive".
>> Firstly, A and ~A is interpreted as complementary sets in common  
>> models, but
>> here ~A is a function.
>> Secondly, for x:A and y:(~A),  (x,y):(A & ~A) = y(x)? this equation  
>> is just
>> applied to A&~A or for any  type A & B ?
>> For example, if we treat ~A is a complementary proposition of A,  
>> lets assume
>> A is prime number, then x:A means x is a prime number, and y:~A  
>> means y is
>> not a prime number. (x,y) means a pair of a prime number with any
>> object other than a prime number. Can this lead to a contradiction?
>>
>> Best Regards
>> Xuhui
>>
>>
>>
>> > -----原始邮件-----
>>> 发件人: "Noam Zeilberger" <noam.zeilberger at gmail.com>
>>> 发送时间: 2010年5月21日 星期五
>>> 收件人: "Xuhui Li" <xhli06 at 163.com>
>>> 抄送:
>>> 主题: Re: [TYPES] what does a negative proposition represent in  
>>> type
>>> theory?
>>>
>>> Hello Xuhui,
>>>
>>> I am unfamiliar with your notation: what is the "Ø" connective?  If
>>> you mean negation (which I've usually seen written ~ or ¬), then  
>>> the
>>> standard interpretation of an element of type ~A is as a
>>> "continuation".  There is a close link between the different
>>> double-negation translations of classical into intuitionistic/ 
>>> minimal
>>> logic (by Kolmogorov, Gödel, etc.), and different
>>> "continuation-passing transformations" on the lambda calculus.   
>>> I'd be
>>> happy to point you to references if you're interested (and apologies
>>> if this was not what you were talking about).
>>>
>>> Noam
>>>
>>> On Fri, May 21, 2010 at 4:56 AM, Xuhui Li <xhli06 at 163.com> wrote:
>>>> [ 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
>>>>
>>
>>
>> ________________________________
>> 网易为中小企业免费提供企业邮箱（自主域名）