Re: [mizar] structures

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

On Sun, 29 Sep 2002, Andrzej Trybulec wrote:

> I doubt if I want structures widen to the type 'Function'. I do not see what
> is the gain, besides the general fact that we would may to instantiate the
> theorems about function by structures (for what purpose? ). But it will cause
> problems with overloading the symbols, putting the proper order in the
> 'notation' directive will be, perhaps, even more difficult.
> 
> Actually I am not certain, if I want structures to widen to 'set'. If we have
> another root type,
> say 'something', that it would be enough if they widen to 'something' (I do
> not want to have urelements, we just have restore TARSKI:1 (now cancelled) :
> 'everything is a set').

OK, we can go in the direction of "hard-wiring" things, but that means 
at least two things: 
We have to implement them and we have to describe what is hard-wired 
(implemented). 
There is a list of things not implemented for structures in my previous 
mail (I doubt it is complete). 

And even if someone gets happy implementing them, we can use a  
requirement directive for that later. This would be similar to 
requirements about numbers: they are useful, but surely, they do not 
implement all the things in MML about numbers. This is also advantage of 
Mizar over normal programming languages: we can prove things, and only 
then implement them, always having the possibility to use the theorems, 
when the implementation is insufficient, or wrong (to show it by 
contradiction (such things have happened, if I remember correctly :-)).

So I think it would be good to know in Mizar what structures are at all, 
maybe the fact that they are Functions is not that important (but could be 
useful, there are about 5000 theorems containing Function-like in MML).

It is as useful as knowing what numbers are, or what (ordered) pairs are - 
these are in Mizar also just some particular models of some abstract 
objects with some properties, but that allows us to prove and check them 
and their mutual consistency.
 
This not just theory, e.g. the current implementation now often enforces 
to write only "strict" versions of theorems (exactly because we do not 
know, what structures are). Have you seen such things anywhere in normal 
mathematics?

As for the "notation" directive and its use for overloading, I think this 
is a separate problem, that we should discuss.  It has happened to me, 
that I needed two different redefinitions of the same constructor in one 
article, and with the growth of MML, such things will occur more 
frequently.

Josef