Re: [mizar] Formalizing undefinedness

["William M. Farmer" <wmfarmer@mcmaster.ca>]

Dear Freek,

Your "guess" is correct:  

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

is false for the reason you mentioned.

It is not possible to define a predicate like 

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

All predicates are "strict" in the sense that the application of a
predicate to an undefined term is always false.  However, there is no
reason why the logic could not be extended to include "nonstrict
predicates" like =~.  (In STTwU =~ is just an abbreviation.)  So you
are not confused.

I claim that both = and =~ are commonly used in traditional
mathematics.  Although Spivak definitely uses both of them, he
represents each of them by =.  My guess is that he thought two
different explicit notions of equality would be just one more thing to
confuse calculus students, and in most cases which one is being used
can be determined from context.

Best regards,

Bill

===========================================================================

From: Freek Wiedijk <freek@cs.kun.nl>
Subject: Re: [mizar] Formalizing undefinedness
To: mizar-forum@mizar.uwb.edu.pl
Date: Mon, 12 Jan 2004 21:10:40 +0100 (MET)

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