Re: [mizar] Formalizing undefinedness

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

Dear Andrzej,

I am glad that you read my paper.  A logic with undefinedness works
exactly like a traditional logic if there is no use of undefined
terms.  Hence, the statement
  
  for x,y holds x <= y iff not y < x      [1]

is true.  Undefinedness does not play a role here because x and y
range over values, not terms.  You may have been thinking of the
schema

  S <= T iff not T < S                    [2]

where S and T are terms.  A member of this schema is true iff S
and T are defined.  For example,

  1/0 <= 2 iff not 2 < 1/0                [3]

is false; it reduces to

  false iff not false

because the application of a predicate (in this case, <= and <) to an
undefined term is false.

Note that [3] is not an instance of [1] since only defined terms can be
substituted for the quantified variables in a universal statement.

The distinction between (1) a predicate and its predicate complement
(e.g., = and <>) and (2) a predicate and its negation (e.g., = and "not
=") is crucial.  <> is not the same as "not =" for undefined terms.
In particular,

  x <> 1/0

is false because the predicate <> is applied to the undefined term
1/0, but

  not x = 1/0

reduces to 

  not false 

because similarly the predicate = is applied to the undefined term
1/0.

Best regards,

Bill

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

Date: Sun, 11 Jan 2004 19:25:25 +0100
From: Andrzej Trybulec <trybulec@math.uwb.edu.pl>
To: mizar-forum@mizar.uwb.edu.pl
Subject: Re: [mizar] Formalizing undefinedness

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