Structure typed loci

We would like to make some comments on a certain ``obnoxious'' property of the current implementation of MIZAR concerning constructors whose arguments are structures. The remarks below apply to all structures, but we will use algebraic lattices as an example. Currently, there is a need to prove theorems of the following form

theorem                                                 :: WAYBEL_8:17 
for L1, L2 be non empty reflexive antisymmetric RelStr
 st the RelStr of L1 = the RelStr of L2 & L1 is algebraic
  holds L2 is algebraic;

The forgetful functor the RelStr of when given a structure derived from a RelStr returns the strict RelStr structure, that is, a structure with exactly two fields: carrier and InternalRef. Because of this formulation, the theorem can be applied to objects of type, say, TopRelStr (see Section ).

The attribute algebraic was defined above for non empty reflexive RelStr. One would suspect that if the RelStr of L1 = the RelStr of L2 and L1 is algebraic, then obviously L2 is also algebraic, but this is not obvious to the MIZAR checker. In the case of the attribute algebraic as defined above, it is really puzzling why not. However, in general, the simplest of reasons for a theorem of this form not being obvious to the checker is that it can be false. For the sake of illustration, let us consider the following, simplified and twisted, example. First, we define an attribute

definition
 let R be RelStr;
 attr R is funny means                                           :LFD:
  ex T being TopRelStr st R = T;
end;

(TopRelStr is discussed in Section .) The argument R is used improperly in the definiens. Instead of only examining its fields, we try to say something about R in its entirety. This abuse renders proving the following claim impossible

theorem FALSE:
for R, T being RelStr st the RelStr of R = the RelStr of T & R is funny
 holds T is funny;

There is no way we can succeed because of the following counterexample

   reconsider IR = {} as Relation of {} by RELSET_1:25;
   set  R = RelStr(# {}, IR #);
   consider TL being empty  Subset-Family of {};
   set T = TopRelStr(# {}, IR, TL #);

  T is funny by LFD; 
  then R is funny by FALSE;

where we have constructed two objects R and T which satisfy premises of the theorem yet the conclusion is false.

Let us note that in the present implementation of MIZAR we cannot prove the negation of the claim named FALSE. Currently, there is considerable discussion in the MIZAR project about an implementation of constructors with arguments that are structures which would allow similar properties to be discovered automatically by the processor when they hold. As of now, we have to prove sequences of theorems, sometimes long, similar to WAYBEL_8:17 above.

Another not very pleasant aspect of the MIZAR system, also concerning structures, is that we cannot define a general notion of an isomorphism between structures. Such a definition is possible for structures defined within a universal algebra, but there is no way to introduce the general notion of an isomorphism for structures occurring at the language level.