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

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

On Mon, 26 Aug 2002, Piotr Rudnicki wrote:

>
> 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.
>
> --
> Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
> email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr
>


A few years ago we tried to classify all facts in the Mizar Mathematical
Library. We proposed the following synonyms for "theorem": lemma, remark,
proposition, statement, fact, theorem. Criteria were based on the length
of the proof of the "theorem" and the quantity of information taken from
MML by the "theorem". We did a 2-dimensional table with length of the
proof and information as axis. Unfortunately, results were not so
interesting.  There was to strong correlation between length of the proof
and information. The table was quite sparse.

Maybe we should return to the subject, and repeat all tests.

Another possiblity is to introduce similar synonyms to the grammar and
let authors decide what is what.  However, haveing solid naming
conventions would be better.

Greetings
Artur