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

[Giuseppe Castagna]

Le 21/05/2010 23:25, Noam Zeilberger a écrit :
> [ 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 _|_.
>    

Or, you can take the "semantic subtyping" setting where types are set of 
values, and union, intersection, containement *and* negationtypes  are 
interpreted set-theoretically. So in particular not(A) is the set of all 
values that do not have type A. However you  end up in a more syntactic 
world since for instance the implication A -> B is the set of  
well-typed lambda abstractiond  that when applied to an expression of  
type A, if they return a value, then this is in B; but for cardinality 
reasons it cannot denote the set of functions from A to B  (For more 
details see JACM vol. 55, n. 4, pag. 1-64, 2008.)

Beppe