Re: [mizar] Formalizing undefinedness

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Bill,

>Hence, the statement
>  
>  for x,y holds x <= y iff not y < x      [1]
>
>is true.

... as it should be :-)  And I guess that

  for x,y holds 1/x <= y iff not y < 1/x

is false?  Because it fails when x = 0: in that case the left
hand side of the iff is false, while the right hand side is
true.

What worries me more is this "=~" relation (the equality sign
that is true when both sides are defined and equal, or when
both are undefined).

I suppose you can't define

  defpred P[real number,real number] means $1 =~ $2

for the non-Mizar people, this is like defining

  P := \x,y. x =~ y

Because if you could define this then

  P[1/0,1/0]

should be true (because 1/0 and 1/0 are both undefined and
P[1/0,1/0] means 1/0 =~ 1/0), but also for _any_ P of type
iota->iota->* we should have that

  P[1/0,1/0]

is the "bottom" of *, which is false.

Or am I confused?

Freek