[mizar] Re: strict

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> BTW: it's better to state such properties of F2 as functorial
> registrations rather than theorems - this way they could be used
> automatically by the checker when one would import your registrations.

I see your point, and when I was looking in the MML for examples on
which I could base my definition of F2, I found that functorial
registrations were the customary way of accomplishing my task.
Although I don't want to break with the custom and I understand the
value for the checker if I follow it, I do think that it is more
natural to express the properties of a new term as theorems rather
than as functorial registrations.  By expressing properties in terms
of functorial registrations, one is writing for the MIZAR checker, not
for human readers.  It seems to me that using functorial registrations
takes MIZAR away from rather than toward the mathematical vernacular.
(Though perhaps one could argue that the MIZAR custom of functorial
registrations is actually captures what's going on in the mathematical
vernacular.)

This is just a comment about the relationship between the MIZAR
language and the mathematical vernacular, not about the utility of
adhering to custom when preparing a MIZAR article.  Now that you've
reminded me of the value of using functorial registrations, I will
edit my file and express what are now theorems in the form of
functorial registrations.

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference