Re: If A=B & (A contains C), why mizar doesn't infer (B contains C)

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

On Wed, 27 Jun 2001, Piotr Rudnicki wrote:

> I would like to see a real example for a need of ficticious arguments
> besides for (how Andrzej puts it) creating fictitious theories.

I don't have a good example and I think that fictitious arguments should
be avoided. The hypothetical case I had in mind is, when a good "hacker"
notices, that the type/cluster system is very advantageous for him, if he
uses some more special type, than is actually needed (e.g. "Element of X"
instead of "set"), and thus he saves a lot of work with establishing the
clusters and type hierarchy for the more general case. That is also why I
think that removing fictitious arguments can become quite difficult.

It should be avoided, but it can become the same as when one proves just a
special version of some theorem, because it is easier ... everyone is
tempted to save some work this way sometimes.


Josef Urban

---------------------------------------
A very stupid (and incorrect) case:

definition let X be set;
  attr X is contained means ex y being set st X in y;
end;

definition let X be set;
  cluster -> contained Element of X;
end;

definition let X be set; let Y be Element of X;
 redefine func bool Y -> Subset of bool union X;
end; 

definition let X,Y be contained set;
  pred bla1 X,Y means X=Y; :: or whatever else
end;
  
definition let X be set; let Y be Element of X;
  pred bla2 Y means bla1 Y, bool Y;
end; 


Now bla2 has fictitious argument X, but if I defined it just for Y being
contained set, I would have to add something to ensure, that bool Y is
contained. So I saved some work. More can be saved as the type/cluster
system becomes deeper.