Re: [mizar] Formalizing undefinedness

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Dear prof. Farmer,

I have just superficially read your paper, and it seems to me that there 
are two problems or tasks:

(1)  Finding the most natural syntax for dealing with undefinedness.
(2)  Finding the most natural semantics for such "natural" syntax.

It is tempting to say, that these tasks are a bit contradictory :-).

>From the (1)'s point of view (ignoring any semantics issues for the 
moment), I agree that having things like "=~" seems to be an improvement, 
since it at least provides a kind of a "warning" to anyone who is dealing 
with formulas like "x/x = 1".
>From this "user's point of view", it feels much easier to read the formula 

"x/x =~ 1 - 0/x" , being advised by "=~" that "there is a catch",

than to read the Mizar theorem

"x/x = 1 - 0/x" , wondering "What the Hell is happening here??", and being

answered: "So they did not teach you that 0/0 = 0 ?" :-).

Freek wrote earlier that he hates such "accidental" theorems, which seems 
to be the proper name for that. Such defaults lead to all kinds of 
"clever hacks", which make the text incomprehensible to anyone below the 
level of High Initiate.

In the purely syntactical sense, this "warning" approach for 
"possibly undefined" terms could even be used more widely - one could imagine 
e.g. some syntactic conventions for "possibly empty" types, etc. 

It is for exactly the same reason, that I do not like the "default" value  
of predicates on undefined terms in your approach. E.g. 

"x/y = 1 implies x = y"

is just simply true in your system, leading to the same kind of confusion 
as the Mizar "0/0 = 0" default above. But it is the only default you 
propose, while Mizar allows (and uses) many ad hoc defaults of this kind.

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. 
Such detailed marking reminds me a bit of using explicit retracting 
operators in the "partiality via subtypes" approach.

I think (2) (i.e. getting "natural" semantics) is the big problem (prof. 
Goguen in http://www.cs.ucsd.edu/users/goguen/pps/ftp97.ps cites Rolling 
Stones' "I can't get no satisfaction" :-).

Being no expert, I believe that this has both the "rational" side - more 
options come to mind than in the classical Tarski's approach, and also 
some more "irrational" side - I do not know why, but it seems to me that 
many "normal" mathematicians are generally distracted from working inside 
"nonstandard" formalisms, be it nonstandard set theory, constructive 
logic, type theory, or just nonstandard analysis.


Best regards,
Josef Urban