Re: [mizar] Formalizing undefinedness

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Bill,

I have read your paper (it does not mean that I completely understand it
:-)). I rather like the idea that, if you allow for Mizar notation,

    for x holds x <> 1/0

is true because

   for x holds x*0 <> 1

is definitely true. However, if I am correct,

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

is false. And this I do not like at all.

All the best,
Andrzej

"William M. Farmer" wrote:

> The discussion a few weeks ago about formalizing undefinedness on the
> Mizar Forum inspired me to write a paper entitled "Formalizing
> Undefinedness Arising in Calculus" which is available at
>
>   http://imps.mcmaster.ca/doc/calculus.pdf
>   http://imps.mcmaster.ca/doc/calculus.ps
>
> The paper attempts to show that the traditional way of handling
> undefinedness in informal mathematics can be very directly formalized
> in a standard logic if the standard logic is modified slightly to
> admit undefined terms and statements about definedness.
>
> Bill Farmer
>