Re: [mizar] [piotr@sedalia.cs.ualberta.ca: A request from W W Armstrong]

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

I am still in Japan, but we gor the maintenance day here. So I use the Polish 
address.

Quoting Piotr Rudnicki <piotr@cs.ualberta.ca>:

> 
> Bill Armstrong, Y. Nakamura and I are finishing formalization of the
> celebrated 1974 Bill's paper on the functional dependencies in
> relational data bases.  Bill joined the effort quite late but is very

Good news!

> helpful in improving the final editing.  He took seriously my claim
> that Mizar texts are readable with routine effort and studies on his
> own the parts of the paper done before he joined.  He wanted me to
> pass the following comment.  When trying to understand the following
> completely on his own
> 
> 	definition
> 	  let X be set;
> 	  cluster (B1) (B2) Subset-Family of X;
> 	end;

I completely agree. The choice of the reserved word is the problem, 
'registration' seems to be too long, and 'register' is in the imperative style.
There is an additional argument: the syntax of a registration block is 
different, because assumptions are nor allowed. Now they are simply ignored.
The same goes for (actual) redefinitions, so maybe also 'register' should be 
used, not 'definition'.
> 
> he got stuck and was totally confused.  The attributes and the type are
> earlier defined in the paper.  The source of his confusion was the word
> "definition" because what on Earth is being defined here.  Bill says that
> if instead of "definition" there was some other keyword, his confusion would
> probably be not as frustrating.
> 
> And also, Bill wishes that Mizar has numerous synonyms for the keyword
> "theorem" because as of now, facts that differ by orders of magnitude
> in importance and difficulty are announce as "theorem" which makes him laugh
> at times.
>

Maybe we should use a different reserved word, e.g. 'fact' instead of 
'theorem'. On the other hand a good laugh is always good :-)

Greetings,
Andrzej

----------------------------------------------------------------------
This mail sent through web e-mail system:  https://mathmail.uwb.edu.pl
powered by IMP: http://horde.org/imp/