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