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

Re: [mizar] Re: Mizar 7.8.04 MML 4.80.962

You may see the order of processing of the articles on MML.LAR. It is worth to look to it, because as a rule it is a good order of articles in the 'notations' directive. 

MML.LAR is divided in three parts:

1. concrete mathematics (up to STRUCT_0)
2. abstract mathematics
3. mixed part, still not divided (probably starts with BINARI_3, or
   maybe MATRIX_1).
The concrete means that it does not depend on the concept of the structure. So it may be called 'structure-free'. We used previously 'classical' and 'modern'. But this 'modern' stuff is already more than 100 years old. The current terminology is borrowed from the Larry Paulson lecture in Cork.
In the last revision the GENEALG1 and FINSEQ_7 articles are moved to the concrete part. 

However the cause of moving the definitions from CQC_LANG, and HENMODEL
to FUNCOP_1, NAT_1 is to put the articles related to logic on the end of the concrete mathematics and to make the real concrete mathematics independent of it. It is 34 of them.
I write "real concrete" because it seems that the articles depending on the concept of the language of logic should be made abstract. The language is basically a universally free structure and this part logic should be part of the lattice theory.
When we worked on the QC_LANG with Piotr (1989) we discussed if it should be done in this way - after introducing proper structure. But ZF_LANG was already submitted and we can use it as a template, so ... 

Regards,
Andrzej



Adam Grabowski wrote:


- We still work to divide the MML into the classical and
  abstract part, so the ordering of articles reflected in
  mml.lar file continuously changes; these changes are
  rather minor, we move some auxiliary definitions and
  lemmas from articles which are - so to say - accidental
  to more appropriate ones. Here the changes are rather
  significant but an ordinary Mizar user probably won't
  notice it (e.g. scheme of the existence of functions from ZFREFLE1
  in now in CLASSES1, or the functor IFEQ which was in CQC_LANG
  is now in FUNCOP_1).