Re: [mizar] Formalizing undefinedness

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

Josef,

> It seems to me now, that (at least in the first-order case) there is
> no need for having any notion of "partial satisfaction" for this,
> because it is cheaply translatable back to the Tarski's semantics by
> using predicates.

I would restate your observation as follows.  The machinery of partial
functions and definite description in a logic with undefinedness, such
as STTwU and the IMPS logic, is no more than a convenience.  In fact,
any theory in a logic with undefinedness can be translated into an
equivalent theory in the corresponding standard logic by eliminating
the use of nonpredicate functions and definite description.
Nonpredicate functions are represented as you noted with predicates,
and definite descriptions are unwound as B. Russell noted in his
famous paper "On Denoting".  A logic with undefinedness is thus just a
convenient version of the standard logic from which it was
derived.

Bill

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

Date: Wed, 14 Jan 2004 11:34:05 +0100 (CET)
From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
To: <mizar-forum@mizar.uwb.edu.pl>
Subject: Re: [mizar] Formalizing undefinedness

Dear prof. Farmer,

> 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.

I think I understand this, you do not speak about _the_ quotient for 
any two x,y, it is a bit like a predicate "Quotient[x,y,z]".

It seems to me now, that (at least in the first-order case) there 
is no need for having any notion of "partial satisfaction" for this, 
because it is cheaply translatable back to the Tarski's semantics by using 
predicates. 
That means that for any "partial" functor f we just state the 
"functionality" ("uniqueness" in Mizar) of its graph G_f, and any 
occurence of f(x,y) (e.g. in predicate P) is replaced by statement
(1) "ex z st G_f[x,y,z] & P[z]". 
The only exception is the "=~" predicate, which translates to
"for z holds G_f1[x,y,z] iff G_f2[x,y,z])". 
Is it correct?

With such interpretation, there is no arbitrariness (as I have thought 
earlier) in having P[f(x,y)] = false, if f(x,y) is undefined - it is simply 
the value of (1). Maybe I should have read your paper more carefully :-).

In Mizar this would correspond to relaxing the "existence" condition, 
which now has to be proved for any new functor (meaning totality). 
Actually, in the previous discussion, I argued for relaxing the 
"existence" condition for types, though there the meaning is a bit 
different (nonemptiness).

I think that a lot of arguments from that discussion applies, it is 
certainly better, if we can prove the "existence" and know that we are 
not talking about nothing, but having it as a hard-wired requirement 
leads to various undesirable "cheats" in some situations.

So the final suggestion for types was to have both, and to retain the 
"existence" conditions, if it is possible to give them without the 
cheating, and probably also have some syntax to tell the two cases apart.
This might be done with functors too, and is simpler than marking terms.

> 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.

Yes, it would rather be "possibly undefined subterm". Your example  
suggests that marking just the smallest would not be enough, and e.g. in 
the retracting analogy, one would also need retracts both for arguments of 
"/" and "sqrt".

Best regards,
Josef