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

[Uday S Reddy]

This exchange suggests that you are not talking about intuitionistic
type theory, but something else.  But it is not clear what.


> > 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?

This example is misleading.  "prime number" is not a proposition, but
rather a predicate.  You can regard "there exists a prime number" as a
proposition, and a particular prime number x as its witness.
However, note that ~A is then "there does not exist a prime number",
for which there is no proof.  

If you are trying to produce a logic where A & ~A has a proof, it is
not likely to be a very good logic, is it?

Cheers,
Uday Reddy



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