Re: NULLs: theoretical problems?

From: Jan Hidders <hidders_at_gmail.com>
Date: Thu, 30 Aug 2007 09:02:36 -0000

On 30 aug, 06:12, "V.J. Kumar" <vjkm..._at_gmail.com> wrote:
> Jan Hidders <hidd..._at_gmail.com> wrote innews:1188272437.208915.202690_at_22g2000hsm.googlegroups.com:
>
> > On 27 aug, 23:30, "V.J. Kumar" <vjkm..._at_gmail.com> wrote:
>
> >> and we are forced to have the
> >> 'def(x) :(x or not x)' which evaluates to 'false' ,
>
> > That is not the only option. If you interpret the formula 'x' as 'x is
> > defined and true' then the proper corresponding formula in DEF logic
> > would be '(def(x):x) or not(def(x):x)' which of course evaluates to
> > true.
>
> Oh, man... You should have said it: '(def(x):x) or not(def(x):x)' at the
> very beginning. We would have saved a lot of virtual trees !

Stuff happens.

> What you are proposing here is a Z crowd way to handle undefinedness,
> one of many really.

Of course. I never said it was something new, just that it was my favorite.

> It's an old, very well know approach called "all
> predicates denote" that some like and some others dislike. One of other
> Z alternatives to do the same is of course a multi-valued Lukasiewicz-
> like trick called LPF. You do not like LPF, I know. It does not have
> LEM and deduction theorem, but LPF's expressivity with weak equality is
> provably equivalent to "all predicates denote"/FOPC+existential equality.

Sure, the expressive power in terms of what can and cannot be expressed is almost always the same and not really an issue. In fact, I would say it is besides the point.

> Or something like that. Anyway, if I remember correctly, FOPC+exist.
> eq. was criticised for being too verbose in expressing the same specs. as
> LPF did, required two notions of equality, weak and existential, and
> could not express complex predicates well. On the whole, it was a tie,
> so in my mind neither was "better" than the other. Also, intuitively,
> "all predicates denote" when some terms don't sounds rather fishy, don't
> you agree ? How do you determine that a term does not denote,
> practically speaking ?