Lattices in MML

There are at least two approaches to lattices in literature:

1. A lattice is an algebra with two binary operations $\sqcup$ and $\sqcap$ which satisfy the conditions of idempotence, associativity, commutativity, and absorption.
2. A lattice is a partially ordered set (poset) with suprema and infima for non empty finite subsets.

Both approaches were already present in MML and the correspondence between them has been proved. The CCL-book employs the second approach, but we briefly describe here how the first approach was developed in LATTICES [63] as it illustrates well a typical way of working with MIZAR structure types.

The ``mother'' of almost all structure types is defined in STRUCT_0 [36] as

definition
  struct 1-sorted(# carrier -> set #);
end;

The ``backbone'' structures for lattices are defined as

definition
  struct(1-sorted) /\-SemiLattStr
    (# carrier -> set, L_meet -> BinOp of the carrier #);
  struct(1-sorted) \/-SemiLattStr
    (# carrier -> set, L_join -> BinOp of the carrier #);
end;

definition
  struct(/\-SemiLattStr,\/-SemiLattStr) LattStr
    (# carrier -> set, L_join, L_meet -> BinOp of the carrier #);
end;

These definitions are only the ``building blocks'' without any lattice-like properties. The LattStr structure merely combines the fields of /\- and \/-SemiLattStr.

It is typical to introduce more convenient notations for the semi-lattice operations. In the remainder of this paper we omit all the proofs which appear in MIZAR articles.

definition 
 let G be non empty \/-SemiLattStr, p,q be Element of the carrier of G;
 func p"\/"q -> Element of G equals                  :: LATTICES:def 1
  (the L_join of G).(p,q);
end;

definition 
 let G be non empty /\-SemiLattStr, p,q be Element of the carrier of G;
 func p"/\"q -> Element of G equals                  :: LATTICES:def 2
  (the L_meet of G).(p,q);
end;

The attributes to be applied to our ``backbone'' structures in order to form the concept of a lattice are the following semi-lattice properties

definition let L be non empty \/-SemiLattStr;
  attr L is join-commutative means                   :: LATTICES:def 4 
   for a, b being Element of the carrier of L holds a"\/"b = b"\/"a;
  attr L is join-associative means                   :: LATTICES:def 5 
   for a, b, c being Element of the carrier of L 
    holds a"\/"(b"\/"c) = (a"\/"b)"\/"c;
end;

definition let L be non empty /\-SemiLattStr;
  attr L is meet-commutative means                   :: LATTICES:def 6 
   for a, b being Element of the carrier of L holds a"/\"b = b"/\"a;
  attr L is meet-associative means                   :: LATTICES:def 7 
   for a, b, c being Element of the carrier of L 
    holds a"/\"(b"/\"c) = (a"/\"b)"/\"c;
end;

and to define absorption laws we need the entire lattice structure

definition let L be non empty LattStr;
  attr L is meet-absorbing means                     :: LATTICES:def 8 
   for a, b being Element of the carrier of L holds (a"/\"b)"\/"b = b;
  attr L is join-absorbing means                     :: LATTICES:def 9 
   for a, b being Element of the carrier of L holds a"/\"(a"\/"b) = a;
 end;

At this point, we can finally say what it means for a structure to be lattice-like.

definition let L be non empty LattStr;
  attr L is Lattice-like means                      :: LATTICES:def 10 
   L is join-commutative join-associative meet-absorbing
        meet-commutative meet-associative join-absorbing;
end;

Next, we demonstrate that there are LattStrs which are Lattice-like; this is expressed by the following existential registration Clusters are used to express the following relationships:

Conditional registrations

are used to say that objects having a property expressed by some attributes also have another property expressed by other attributes. For example,

cluster non trivial -> non empty set;

says that every non trivial set is non empty. We have to prove that it is indeed the case.

Term adjective registrations

say that a term constructed with a specific functor $^{\:\alph{functors}}$ has a certain property expressed by attributes. For example, if A is a poset then we may have

cluster the InternalRel of A -> Order-like;

which we have to prove. These registrations are frequently called functorial registrations although they are applicable to terms.

Existential registrations

are used to define new type expressions that involve attributes. For example,

cluster non empty reflexive transitive antisymmetric strict RelStr;

and it requires a proof of existence of such an object as MIZAR types are non empty.

The relationships expressed by clusters are automatically processed by the MIZAR processor.

definition
  cluster strict Lattice-like (non empty LattStr);
end;

Assured of their existence, we can finally introduce the needed type for lattices in the following expandable type definition

definition
  mode Lattice is Lattice-like (non empty LattStr);
end;

Now we can prove properties of lattices, for example

reserve L for Lattice;
reserve a, b, c for Element of the carrier of L;

theorem                                                 :: LATTICES:19 
  (for a,b,c holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c))
                         iff
  (for a,b,c holds a"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c));

However, it is quite typical that for proving some lattice property we do not need all the attributes of a lattice. In such a case, we use only the required subset of attributes.

for L being meet-absorbing join-absorbing meet-commutative
       (non empty LattStr),
    a being Element of the carrier of L
 holds a"\/"a = a &  a"/\"a = a by LATTICES:17,18;

Of course, the above theorem works also for objects that share the super-set of the required attributes, for example all Lattice-like objects. One may define further attributes for lattices, such as complete or distributive, and prove more interesting theorems (see LATTICES [63].)

The second of the earlier mentioned approaches to lattices gives wider usage, is easier to generalize (by weakening conditions of partial ordering), and was the basic approach in the CCL-book. Adopting this approach as the basic one prompted the first revision of MML which consisted in the generalization of posets and some lattice-theoretical concepts (see Section ).

RelStr is the base relational structure which serves as an ancestor to quasi ordered sets, posets, semi-lattices, and lattices and is introduced (cf. Section ) in ORDERS_1 [56] as follows

definition
  struct (1-sorted) RelStr (#
    carrier     -> set,
    InternalRel -> Relation of the carrier
  #);
end;

If $R$ is a RelStr, then $R$ is a structure with at least 2 fields: carrier and InternalRel. A structure $S$ can be a RelStr and may have more fields when its type is derived from RelStr, i.e., when RelStr prefixes the type of $S$. (The details of MIZAR structure definitions are presented in [45].) The concept of a poset was introduced in ORDERS_1 [56] after first defining the needed attributes.

definition let A be RelStr;
 attr A is reflexive means                           :: ORDERS_1:def 4
  the InternalRel of A is_reflexive_in the carrier of A;
 attr A is transitive means                          :: ORDERS_1:def 5
  the InternalRel of A is_transitive_in the carrier of A;
 attr A is antisymmetric means                       :: ORDERS_1:def 6
  the InternalRel of A is_antisymmetric_in the carrier of A;
end;

The predicates used in the definiens come from RELAT_2 [62].

reserve X, x, y, z for set;
definition let R, X;
   pred R is_reflexive_in X means                     :: RELAT_2:def 1
      x in X implies [x,x] in R;
   pred R is_antisymmetric_in X  means                :: RELAT_2:def 4
      x in X & y in X & [x,y] in R & [y,x] in R implies x = y;
   pred R is_transitive_in X  means                   :: RELAT_2:def 8
      x in X & y in X & z in X & [x,y] in R & [y,z] in R 
        implies [x,z] in R;
end;

Before defining the Poset type we first $\mathrm{register}^{\:\alph{registrations}}$ the following existential cluster of attributes

definition
  cluster non empty reflexive transitive antisymmetric strict RelStr;
end;

The above cluster assures the existence of an object of type RelStr with any subset of the listed attributes. Attribute strict is built-in. It means that a structure branded strict has only the fields of the named structure and in particular is not derived from this structure by adding other fields. Thus, a strict RelStr has only two fields: carrier and InternalRel. Knowing that such objects exist we define

definition
  mode Poset is reflexive transitive antisymmetric RelStr;
end;

For convenience and to be closer to the usual notation, we introduce the following infix predicate

definition
  let R be RelStr, x, y be Element of the carrier of R;
  pred x <= y means                                  :: ORDERS_1:def 9
   [x,y] in the InternalRel of R;
  synonym y >= x;
end;

In order to define the concept of a lattice based on a poset we need the following attributes from LATTICE3 [4]

definition let R be RelStr;
  attr R is with_suprema means                      :: LATTICE3:def 10
    for x, y being Element of R
     ex z being Element of R st x <= z & y <= z &
      for z' being Element of R st x <= z' & y <= z' holds z <= z';
  attr R is with_infima means                       :: LATTICE3:def 11
    for x, y being Element of R
     ex z being Element of R st z <= x & z <= y &
      for z' being Element of R st z' <= x & z' <= y holds z' <= z;
end;

Now we register the existence of a cluster of attributes

definition
 cluster with_suprema with_infima strict (non empty Poset);
end;

and this delivers our poset based lattice. The correspondence between our new notion and Lattice is established with the help of the following functors.Functors are constructors of terms. We borrowed the name ``functor'' from [42, p. 148]:

... some signs in the formalized language should correspond to the mappings and functions being examined. These signs are called functors, or--more precisely--m-argument functors provided they correspond to m-argument mappings from objects to objects (m = 1, 2, ...).

The definition of a functor includes a proof of correctness in which one must demonstrate the existence and uniqueness of the functor being defined. Mizar functors must not be confused with functors as used in category theory.

definition let L be Lattice;
  func LattRel L -> Relation equals                  :: FILTER_1:def 8
    { [p,q] where p, q is Element of the carrier of L: p"\/"q = q };
end;

definition let L be Lattice;
 func LattPOSet L -> strict Poset equals             :: LATTICE3:def 2 
    RelStr(#the carrier of L, LattRel L#);
end;

For the correctness of the latter definition one needs to prove that LattRel L is an Order on the carrier of L. LattPOSet enjoys the following properties.

theorem                                                 :: LATTICE3:6 
 for L1,L2 being Lattice st LattPOSet L1 = LattPOSet L2 
  holds the LattStr of L1 = the LattStr of L2;

theorem                                                :: LATTICE3:11
 for L being Lattice holds LattPOSet L is with_suprema with_infima;

theorem                                                :: LATTICE3:19 
 for A being with_suprema with_infima non empty Poset
   ex L being strict Lattice st the RelStr of A = LattPOSet L;

The existence in the last theorem is in fact unique and thus we introduce a third functor

definition 
 let A be RelStr such that A is with_suprema with_infima Poset;
 func latt A -> strict Lattice means               :: LATTICE3:def 15
  the RelStr of A = LattPOSet it;
end;

The promised correspondence between these two kinds of lattices is nowhere explicitly stated in MML although it can be proven in a straightforward way as follows:

for P being strict with_infima with_suprema Poset 
 holds LattPOSet latt P = P                        by LATTICE3:def 15;

for L being strict Lattice holds latt LattPOSet L = L
proof let L be strict Lattice;
  LattPOSet L is with_suprema with_infima           by LATTICE3:11;
  then LattPOSet latt LattPOSet L = LattPOSet L by LATTICE3:def 15; 
 hence latt LattPOSet L = L                         by LATTICE3:6;
end;

These two facts raise an interesting issue for any computerized knowledge base for mathematics: should the simple consequences of facts already stored in the data base also be included in the data base? This is an important question for the process of automating searches of the data base. If one answers

yes:

this would clutter the data base with a lot of trivialities,

no:

there is overwhelming evidence that such simple consequences are sometimes not that simple for humans to find.

Probably a good solution would be to have the search engine generate such simple consequences on the fly. This would require some reasonably modest definition of simple consequence in order to curb the complexity of searching algorithms.