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

Noam Zeilberger noam.zeilberger at gmail.com
Fri May 21 17:25:33 EDT 2010


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
>> >
>
>
> ________________________________
> 网易为中小企业免费提供企业邮箱(自主域名)


More information about the Types-list mailing list