Re: [mizar] Another factor...

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

n Tue, 14 Jan 2003, Freek Wiedijk wrote:

> I would like to be able to say "the MML contains on the order
> of so-and-so many theorems" and then be talking about usual
> theorems instead of about _Mizar_ theorems (which are a bit
> more light-weight, it seems to me.)  So there are about
> 40,000 Mizar theorems there, right?  So how many _book_
> theorems would that be? :-)

It seems to me that the Mizar keyword "theorem" is a bit misleading for
this purpose. Its real meaning is something like "export", it just  makes
the proposition available in other articles. The syntax simply does not 
allow the authors to categorize the propositions yet.

What I often encounter could be called the "proposition stating problem":
Given a piece of reasoning, is there a good way how to capture it by a 
proposition? Will it pay, when compared to the copy&paste method applied 
to the piece of reasoning? Or just in terms of "proof elegance"? 
My impression is that copy&paste (combined with search&replace) wins 
over "proof elegance" quite often in Mizar. It is often faster, produces 
more lines (which some people count for various doubtful measures ;-),  
and requires less thinking.

Another part of the problem is, that sometimes you can think not of just 
one proposition, but of a chain of more general propositions, but the 
Mizar type systems deters you from stating it too generally, as it may be 
quite a pain to use e.g. some "obviously applicable" category theorem in a 
concrete situation.

Also, the situation differs from book writing in that you never know 
exactly, what your article will be later used for.
i find much more analogy with developement of e.g. software libraries.


Josef