Re: [mizar] structures

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

On Sun, 27 Oct 2002, Andrzej Trybulec wrote:

> 
> I meant that is (ground) terms
>     the fixed theta_1 of  args_1      and
>     the fixed theta_2 of args_2
> occur in an inference, and
>     the fixed theta_1 of arg_1 is theta_2 of args_2
> occurs in the inference, too, then
>       the fixed theta_1 of  args_1  = the fixed theta_2 of args_2
> is appended to the premises. I would rather restrict it to the case when
>     'the fixed theta_2 of  args_2'   widens to   'the fixed theta_1 of args_1'.   (*)
> 
> It looks like other "additional inference rules" added to the obviousness, so it is
> nothing special.


But then the undecidability can prevent you from setting a suitable 
(actually any) default for some type (because until we (dis)prove the "is" 
statement, we risk contradiction with your rule). For instance, we will 
never be able to say what the default is for all types, that are 
undecidable for containing the empty set (e.g. all structures now :-) ) 
(actually, if we really _know_ that it is undecidable, we can choose any 
consistent variant and thus strengthen the axiomatics, but we may fail to 
know even that).
The restriction to the widening case (I suppose you meant 'theta_2 of 
args_2' widens to 'theta_1 of args_1') does not help this.

That does not mean I am against it, all this "Practical Calculus of 
Nonsense" is quite interesting, and both the "more rules" and the "more 
arbitrariness" approaches have some advantages.
To say something about the more liberal approach, I think it could 
introduce more "coding on exceptions" into Mizar and e.g. allow the users 
to set their own default for some subtype in domains, where such default 
is common or advantageous.

It seems to me that we should get some statistics on how and how much is
the "Calculus of Nonsense" used now in MML, to know better what we discuss
( in fact MML is unique in managing (hopefully) consistently such large
system of defaults, so someone could do a serious research work on that).
That means e.g. counting the amount of checker inferences, where the
"nonsensical" parts of conditional definitions are (directly or 
indirectly) used, having some overall statistics about definitions with 
assumptions, etc.

Josef