The functions GLB[DIV] and LUB[DIV]

Johan G. F. Belinfante
2005 October 5

SetDirectory["l:"];  << goedel74.02c; << tools.m

summary

Divisibility is usually studied using the domain of integers instead of the set of natural numbers in order to take advantage of the fact that the integers form a principal ideal domain.  The principal ideal corresponding to the greatest lower bound of a nonempty set of integers is the intersection of the set of principal ideals generated by the members of that set.  In this notebook a rather similar theory is developed, but always staying within the framework of the natural numbers.  Formulas for the domain and range of the functions GLB[DIV] and LUB[DIV] are derived.  It is shown that every set of natural numbers has a greatest lower bound by explicitly constructing it.  It follows that set of the natural numbers, ordered by divisibility, forms a complete lattice.  The formula for the domain of  LUB[DIV] is derived from a general fact about complete lattices.  The explicit construction of greatest lower bounds yields simple formulas connecting the functions GLB[DIV] and HULL[image[VERTSECT[DIV],omega]].  This connection can be considered to be the analog for natural numbers of the usual characterization of greatest lower bounds of a set of numbers in terms of the principal ideal generated by that set.

range of GLB[DIV] and LUB[DIV]

The range formulas follow directly from general results applicable to any partial order relation.

SubstTest[range, GLB[po[x]], x -> DIV]

range[GLB[DIV]] := omega

SubstTest[range, LUB[po[x]], x -> DIV]

range[LUB[DIV]] := omega

an upper bound for domain[GLB[DIV]]

An upper bound for domain[GLB[DIV]] follows from  a general result.

SubstTest[subclass, domain[GLB[x]], domain[LB[x]], 
      x -> DIV]

% /. Equal -> SetDelayed

range[VERTSECT[DIV]] and image[VERTSECT[DIV],omega]

Although the set omega is not a principal ideal domain, it behaves rather similarly.  The natural analog for omega of the principal ideals of the domain  Z  of integers are the sets of the form image[DIV,set[x]].   If  x  is a natural number, the set  image[DIV,set[x]] holds all multiples of  x.  When  x  is not a natural number, one obtains the empty set.  The members of the set range[VERTSECT[DIV]] are all these sets, including the empty set.   The empty set is omitted by working with image[VERTSECT[DIV], omega].

member[image[DIV, set[x]], image[VERTSECT[DIV], omega]] // 
      AssertTest

member[image[DIV, set[x_]], image[VERTSECT[DIV], omega]] := 
      member[x, omega]

Both of the sets  range[VERTSECT[DIV]] and image[VERTSECT[DIV], omega] are closed under arbitrary intersections.  They are related as follows:

union[set[0],image[VERTSECT[DIV],  omega]]

HULL[range[VERTSECT[DIV]]] and HULL[image[VERTSECT[DIV],omega]]

Both of the sets are closed under arbitrary intersections.    The set hull[image[VERTSECT[DIV], omega], x]  is the intersection of all sets of the form  image[DIV,set[y]], where y is a natural number, that contain a given set  x  of natural numbers.  (This hull is akin to the principal ideal generated by a set of integers.)  Note that the hull is a set because any set of natural numbers is contained in at least one of the sets image[DIV,set[y]] , namely the set of multiples of  1 = set[0].

These two functions have the same domain, but different ranges.

domain[HULL[range[VERTSECT[DIV]]]]

domain[HULL[image[VERTSECT[DIV], omega]]]

Lemma.

Assoc[HULL[image[VERTSECT[DIV], omega]], id[P[omega]], 
      id[x]]

composite[HULL[image[VERTSECT[DIV], omega]], 
        id[intersection[x_, P[omega]]]] := 
      composite[HULL[image[VERTSECT[DIV], omega]], id[x]]

The two functions agree on all nonempty sets.

Map[composite[VERTSECT[reify[x, #]], id[complement[set[0]]]] &, 
      SubstTest[hull, union[u, v], 
        x, {u -> image[VERTSECT[DIV], omega], 
          v -> set[0]}]]

The only difference is the value assigned to the empty set:

APPLY[HULL[range[VERTSECT[DIV]]], 0]

APPLY[HULL[image[VERTSECT[DIV], omega]], 0]

temporary rewrite rules

It is easy to write either one of the two functions in terms of the other.  In this notebook the function HULL[image[VERTSECT[DIV],omega]] is favored because it is the one that appears in the final results.

SubstTest[implies, and[member[x, domain[y]], FUNCTION[y]], 
      member[APPLY[y, x], range[y]], 
      y -> HULL[image[VERTSECT[DIV], omega]]]

(% /. x -> x_) /. Equal -> SetDelayed

Conversely:

Map[or[#, subclass[x, omega]] &, 
      SubstTest[implies, and[member[u, v], subclass[v, w]], 
        member[u, w], {u -> hull[image[VERTSECT[DIV], omega], x], 
          v -> image[VERTSECT[DIV], omega], w -> P[omega]}]]

(% /. x -> x_) /. Equal -> SetDelayed

These results can be combined:

equiv[
      member[hull[image[VERTSECT[DIV], omega], x], 
        image[VERTSECT[DIV], omega]], subclass[x, omega]]

member[hull[image[VERTSECT[DIV], omega], x_], 
        image[VERTSECT[DIV], omega]] := subclass[x, omega]

Lemma.

hull[set[0], x] // Normality

hull[set[0], x_] := image[V, x]

The following temporary rewrite rules force the elimination of hulls involving range[VERTSECT[DIV]] in favor of those for image[VERTSECT[DIV], omega].

SubstTest[hull, union[u, v], 
      x, {u -> image[VERTSECT[DIV], omega], 
        v -> set[0]}]

hull[range[VERTSECT[DIV]], x_] := 
      intersection[hull[image[VERTSECT[DIV], omega], x], 
        image[V, x]]

Map[VERTSECT, 
        SubstTest[reify, x, hull[y, x], y -> range[VERTSECT[DIV]]]] // 
      Reverse

HULL[range[VERTSECT[DIV]]] := 
      union[cart[set[0], set[0]], 
        composite[HULL[image[VERTSECT[DIV], omega]], 
          id[complement[set[0]]]]]

equal[0,hull[x,y]]

This section is concerned with a general characterization of the condition that a hull is empty.  Two lemmas are needed:

Map[implies[#, equal[0, y]] &, 
      SubstTest[and, subclass[y, z], equal[0, z], 
        z -> hull[x, y]]]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
        not[implies[p1, p3]], 
{p1 -> equal[0, hull[x, y]], 
          p2 -> equal[0, y], p3 -> equal[0, A[x]]}]]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

This yields the following rewrite rule:

equiv[equal[0, hull[x, y]], and[equal[0, y], equal[A[x], 0]]] // 
        not // not

equal[0, hull[x_, y_]] := and[equal[0, y], equal[0, A[x]]]

Corollary 1.

image[inverse[HULL[x]], set[0]] // Renormality

image[inverse[HULL[x_]], set[0]] := 
      intersection[complement[image[V, A[x]]], set[0]]

Corollary 2.

equal[
      composite[id[complement[set[0]]], HULL[image[VERTSECT[DIV], omega]]], 
      HULL[image[VERTSECT[DIV], omega]]]

composite[id[complement[set[0]]], HULL[image[VERTSECT[DIV], omega]]] := 
      HULL[image[VERTSECT[DIV], omega]]

using hulls to construct greatest lower bounds

Lemma.  The set hull[[image[VERTSECT[DIV], omega], x] is contained in  any upper bound  y  for the set x.

SubstTest[implies, member[u, v], 
      subclass[A[v], 
        u], {v -> 
          intersection[image[VERTSECT[DIV], omega], image[S, set[x]]], 
        u -> image[DIV, set[y]]}]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The above statement contains a redundant literal:

SubstTest[implies, and[subclass[x, z], member[z, V]], member[x, V], 
      z -> image[DIV, set[y]]]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Removing the redundant literal yields:

Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
        not[implies[p1, p3]], {p1 -> 
            and[member[y, omega], subclass[x, image[DIV, set[y]]]], 
          p2 -> member[x, V], 
          p3 -> subclass[hull[image[VERTSECT[DIV], omega], x], 
              image[DIV, set[y]]]}]]

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Restatement:

implies[member[z, intersection[omega, lb[DIV, x]]], 
      subclass[hull[range[VERTSECT[DIV]], x], image[DIV, set[z]]]]

Lemma.

Map[or[not[member[pair[y, z], DIV]], #] &, 
      SubstTest[implies, and[subclass[x, u], subclass[u, v]], 
        subclass[x, v], {u -> image[DIV, set[z]], 
          v -> image[DIV, set[y]]}]]

(% /. {x -> x_, y -> y_, z -> z_}) /. 
      Equal -> SetDelayed

Lemma.  If the hull of a set  x  is the set of multiples of a natural number  y, and if every member of  x  is divisible by  z, then  z  divides y.

Map[not, 
      SubstTest[and, implies[and[p2, p4], p5], implies[and[p1, p5, p6], p3], 
        not[implies[and[p1, p2, p4, p6], p3]], {p1 -> 
            equal[hull[image[VERTSECT[DIV], omega], x], image[DIV, set[y]]], 
          p2 -> member[z, omega], p3 -> member[pair[z, y], DIV], 
          p4 -> subclass[x, image[DIV, set[z]]], 
          p5 -> subclass[hull[image[VERTSECT[DIV], omega], x], 
              image[DIV, set[z]]], p6 -> member[y, omega]}]]

(% /. {x -> x_, y -> y_, z -> z_}) /. 
      Equal -> SetDelayed

Restatement, removing the variable  z.

Map[equal[V, #] &, 
        SubstTest[class, z, 
          implies[and[member[y, omega], equal[r, s], member[z, u]], 
            member[z, v]], {r -> hull[image[VERTSECT[DIV], omega], x], 
            s -> image[DIV, set[y]], 
            u -> intersection[omega, lb[DIV, x]], 
            v -> image[inverse[DIV], set[y]]}]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Conversely, if the hull of a set  x  is the set of multiples of a natural number  y, and if  z divides  y, then  z  divides every member of  x.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p2, p3], p4], 
        not[implies[and[p1, p3], p4]], {p1 -> 
            equal[hull[image[VERTSECT[DIV], omega], x], image[DIV, set[y]]], 
          p2 -> subclass[x, image[DIV, set[y]]], 
          p3 -> member[pair[z, y], DIV], 
          p4 -> subclass[x, image[DIV, set[z]]]}]]

(% /. {x -> x_, y -> y_, z -> z_}) /. 
      Equal -> SetDelayed

removing the remaining variables

Lemma.

ImageComp[inverse[VERTSECT[DIV]], VERTSECT[DIV], omega] // 
      Reverse

image[inverse[VERTSECT[DIV]], image[VERTSECT[DIV], omega]] := 
      omega

composite[inverse[VERTSECT[DIV]], id[image[VERTSECT[DIV], omega]]] // 
      DoubleInverse

composite[inverse[VERTSECT[DIV]], id[image[VERTSECT[DIV], omega]]] := 
      composite[id[omega], inverse[VERTSECT[DIV]]]

Lemma.

or[and[subclass[x, image[DIV, set[y]]], 
          subclass[intersection[omega, lb[DIV, x]], 
            image[inverse[DIV], set[y]]]], 
        not[equal[hull[image[VERTSECT[DIV], omega], x], image[DIV, set[y]]]], 
        not[member[x, V]], not[member[y, omega]]] // NotNotTest

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The remaining two variables can now be eliminated:

Map[
      implies[equal[0, composite[Id, complement[#]]], 
          subclass[
            composite[id[omega], inverse[VERTSECT[DIV]], 
              HULL[image[VERTSECT[DIV], omega]]], GLB[DIV]]] &, 
      SubstTest[class, pair[x, y], 
        implies[and[member[x, V], member[y, omega], 
            equal[hull[r, x], image[v, set[y]]]], 
          member[pair[x, y], z]], {r -> image[VERTSECT[DIV], omega], 
          v -> DIV, z -> GLB[DIV]}]]

% /. Equal -> SetDelayed

domain formulas

The hull construction yields a lower bound for domain[GLB[DIV]].

SubstTest[implies, subclass[u, v], 
      subclass[domain[u], 
        domain[v]], {u -> 
          composite[id[omega], inverse[VERTSECT[DIV]], 
            HULL[image[VERTSECT[DIV], omega]]], v -> GLB[DIV]}]

subclass[P[omega], domain[GLB[DIV]]] := True

The final step is to combine this result with the upper bound found earlier.  This results in an equation that is made into a rewrite rule.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> domain[GLB[DIV]], 
        v -> P[omega]}]

domain[GLB[DIV]] := P[omega]

It follows from this that the natural numbers, ordered by divisibility, forms a complete lattice.  Since DIV is a complete lattice, one can get the formula for the domain of  LUB[DIV]  as a corollary of the formula for domain[GLB[DIV]].

SubstTest[implies, 
      and[member[x, PO], equal[domain[GLB[x]], P[fix[x]]]], 
      equal[domain[LUB[x]], P[fix[x]]], x -> DIV]

domain[LUB[DIV]] := P[omega]

formulas relating GLB[DIV] to HULL[image[VERTSECT[DIV],omega]]

Lemma.

Assoc[GLB[DIV], id[P[omega]], id[x]]

composite[GLB[DIV], id[intersection[x_, P[omega]]]] := 
      composite[GLB[DIV], id[x]]

Any subclass of a function is a restriction.

SubstTest[implies, and[subclass[u, v], FUNCTION[v]], 
      equal[u, composite[v, id[domain[u]]]], 
{u -> 
          composite[id[omega], inverse[VERTSECT[DIV]], 
            HULL[image[VERTSECT[DIV], omega]]], 
        v -> GLB[DIV]}]

composite[inverse[VERTSECT[DIV]], HULL[image[VERTSECT[DIV], omega]]] := 
      GLB[DIV]

Lemma.

Assoc[id[range[VERTSECT[DIV]]], id[image[VERTSECT[DIV], omega]], 
      HULL[image[VERTSECT[DIV], omega]]]

composite[id[range[VERTSECT[DIV]]], HULL[image[VERTSECT[DIV], omega]]] := 
      HULL[image[VERTSECT[DIV], omega]]

Corollary.

Assoc[VERTSECT[DIV], inverse[VERTSECT[DIV]], 
      HULL[image[VERTSECT[DIV], omega]]]

composite[VERTSECT[DIV], GLB[DIV]] := 
      HULL[image[VERTSECT[DIV], omega]]

serendipity

The following results were discovered in the course of this work, but were not used in the preceding sections.

equal[0, lb[setpart[x], V]] // AssertTest

lb[setpart[x_], V] := 0

In particular:

SubstTest[lb, setpart[x], V, x -> DIV]

lb[DIV, V] := 0

Dual results:

equal[0, ub[setpart[x], V]] // AssertTest

ub[setpart[x_], V] := 0

SubstTest[ub, setpart[x], V, x -> DIV]

ub[DIV, V] := 0