Re: "Formalized Mathematics"

Jesse Alama wrote:

>These five articles ("Tarski-Grothendieck set theory", "Properties of
>subsets", "Functions and their basic properties", "Relations and their
>basic properties", "Functions from a set to a set") are in the top 20
>for a simple reason: the articles in the citeseer database that cite
>them are also FM articles, and virtually all the MML depends on TARSKI.
>
>The citation structure of FM articles is rather different from that of
>other journals.  In mizar everything -- everything! -- that is logically
>required for your article gets cited.  If other journals required
>citations like that, then the citeseer top 20 would probably look very
>different.  (What might be at the top of the pile?  Feller's probability
>books?  Spivak's Calculus?  Halmos's Naive Set Theory?)
>
>  
>
Roman agreed to suppress all citation to TARSKI in next issues of FM. 
So, it will be not so often cited, in FM not at all.

You are not quite right about the citation structure of FM. The articles 
are cited only when the notation introduced in them is used. So, TARSKI 
is so often cited because of the singleton , the unordered pair, the 
ordered pair,, and the inclusion are defined in it.

And we would cite, if not Euclid or Newton, then Cantor or Peano rather 
than Halmos or others.

There are not citation to the Encyclopedia articles (these with the name 
starting with 'X') nor even for addenda like VALUED_0. When an 
Encyclopedia file XRELA_0 for binary relations is eventually ready, that 
the citation to RELAT_1 will vanish.

The TARSKI is an exception, it cannot be overridden by an Encyclopedia 
article, and it is axiomatics. So, probably it should be not cited.

Regards,
Andrzej