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

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> 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.

I believe we have to distinguish:
- semantically fictitious arguments, e.g. for a predicate the second argument
is fictitious if
    P[x,y,z] iff P[x,y',z] for all x,y,y',z
 and similarly for functors, modes or attributes

This I had in mind when answered Chen, I meant that equivalence of formulae is
accidental.
To implement a program that recognizes them is difficult :-) (mostly because
it is undecidable)

- syntactically fictitious, here we have to be careful
 if we define the syntactically fictitious arguments as such argument that may
be removed (with changing pattern, namely substituting for them the loci that
they depend on), the they must be visible, if not we will get error #100. It
is not the case in the Chen's example; in his example is something more
complicated: locus becomes inaccessible, after widening the type of another
locus. If the locus does not occur either in definiens or in the type
involved, then it may be removed without any problem. What Josef wrote it is
not the case (because the locus occurs in the Result Type).

Andrzej Trybulec