[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Re: strict



On Tue, 9 Jan 2007, Jesse Alama wrote:

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

Yes, it's a clear-cut example of a trade-off between sticking close to the mathematical vernacular and adding more automation with new language constructs. In this case, however, the registrations look painfully technical in their *.miz form, but various forms of presentation may 'smooth' them a bit - e.g. the relevant theorems could be printed in the *.xml presentation next to the registrations. And in the TEX'ed form of Formalized Mathematics the presentation looks more or less like a mathematical statement, e.g.: "One can verify that ... is ...".

Best,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================