Re: [mizar] Formalizing undefinedness

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

Dear Josef,

Here is a way to characterize the difference between = and =~.  A = B
means A and B have the same value, while A =~ B means A and B are
equivalent terms in the sense that A can be freely substituted for B.
The latter implies that all undefined terms of the same type are
indiscernible, i.e., there is no way to distinguish them.  Nothing can
be said about an undefined term except that it is undefined.

I interpret the statement

  x/y = 1 implies x = y

as saying that, if there are two values x and y whose quotient is 1,
then the two values are equal -- which is obviously true.  This
seems to me to be the simplest, most natural interpretation.

> Perhaps it would suffice to mend it with some additional syntactic
> sugar.  From this syntactical point of view, the thing that we want
> to have marked is the smallest undefined subterm.

I don't think the "smallest undefined subterm" is well defined because
the undefinedness of a term depends on the context of the term.  For
example, what is the smallest undefined subterm of sqrt(1 + 1/x)?  It
is 1/x if x = 0 and is the whole term if -1 < x < 0.

Best regards,

Bill