powers of unary operations

Johan G. F. Belinfante and Lee Martie
2006 July 9

SetDirectory["l:"];  << goedel83.08a; << tools.m

summary

If  x  is a unary operation, then so is any positive power of x.

characterizing unary operations

In this section, a characterization for unary operations is derived.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p1, p3], implies[p1, p4], 
        implies[and[p2, p3, p4], p5], 
        not[implies[p1, p5]], {p1 -> member[x, UNOPS], 
          p2 -> member[x, V], p3 -> FUNCTION[x], 
          p4 -> subclass[range[x], domain[x]], 
          p5 -> member[x, map[domain[x], domain[x]]]}]]

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

This is actually a logical equivalence, which can be made into a rewrite rule.  An application will be given below.

equiv[member[x, map[domain[x], domain[x]]], 
      member[x, UNOPS]]

member[x_, map[domain[x_], domain[x_]]] := member[x, UNOPS]

The following corollary is obtained using reify.

Map[complement[fix[#]] &, 
      SubstTest[reify, x, dif[set[x], map[f[x], f[x]]], 
        f -> domain]]

fix[composite[inverse[E], MAP, DUP, IMAGE[FIRST]]] := UNOPS

powers of a unary operation

An induction argument will be presented using the following class:

class[y, 
        implies[member[w, v], member[image[u, set[y]], v]]] /. {u -> 
          power[w], v -> map[x, x]}

For convenience, a temporary name is given to this class:

ind[w_, x_] := 
      union[complement[image[V, intersection[map[x, x], set[w]]]], 
        image[inverse[VERTSECT[power[w]]], map[x, x]]]

Lemma 1.

SubstTest[implies, and[equal[x, z], member[x, y]], member[z, y], 
      z -> composite[Id, x]]

or[member[composite[Id, x_], y_], not[member[x_, y_]], 
        not[subclass[x_, cart[V, V]]]] := True

Lemma 2.

Map[not, 
      SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
        not[implies[p1, p3]], {p1 -> member[w, map[x, y]], 
          p2 -> subclass[w, cart[V, V]], 
          p3 -> member[composite[Id, w], map[x, y]]}]]

or[member[composite[Id, w_], map[x_, y_]], 
        not[member[w_, map[x_, y_]]]] := True

These two lemmas settle the base case.  Note that the induction starts at one, not at zero.

member[set[0], ind[w, x]]

For the induction step, the following lemma suffices:

Map[equal[V, #] &, 
        SubstTest[class, t, implies[member[t, z], member[succ[t], z]], 
          z -> ind[w, t]]] // Reverse

(% /. {w -> w_, t -> t_}) /. 
      Equal -> SetDelayed

The induction argument itself yields:

SubstTest[implies, and[member[set[0], z], subclass[image[SUCC, z], z]], 
      subclass[dif[omega, set[0]], z], z -> ind[w, x]]

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

Lemma.

SubstTest[implies, subclass[u, v], 
      subclass[image[t, u], 
        image[t, v]], 
{t -> VERTSECT[power[w]], 
        u -> dif[omega, set[0]], 
        v -> image[inverse[VERTSECT[power[w]]], map[x, x]]}]

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

The result derived in the preceding section is now applied to obtain the main theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], implies[p3, p4], 
          not[implies[p1, p4]], 
{p1 -> 
              member[w, map[x, x]], 
            p2 -> subclass[omega, 
                union[image[inverse[VERTSECT[power[w]]], map[x, x]], 
                  set[0]]], 
p3 -> 
              subclass[
                image[VERTSECT[power[w]], 
                  intersection[omega, complement[set[0]]]], 
                map[x, x]], 
p4 -> 
              subclass[
                image[VERTSECT[power[w]], 
                  intersection[omega, complement[set[0]]]], UNOPS]}]] /. 
      x -> domain[w]

(% /. w -> w_) /. Equal -> SetDelayed

In the final section, a variable is introduced to help make this result more understandable.

reintroducing a variable

Lemma.  The y-th positive power of a relation x is a subclass of its transitive closure.

Map[implies[member[y, omega], #] &, 
      SubstTest[implies, subclass[u, v], 
        subclass[image[w, u], 
          image[w, v]], 
{u -> set[y], 
          v -> dif[omega, set[0]], w -> power[x]}]]

or[equal[0, y_], not[member[y_, omega]], 
        subclass[image[power[x_], set[y_]], trv[x_]]] := True

Lemma.  Any subclass of the transitive closure of a small relation is a set.

Map[implies[member[x, z], #] &, 
        SubstTest[implies, and[subclass[u, v], member[v, V]], member[u, V], 
          v -> trv[x]]] // MapNotNot

or[member[u_, V], not[member[x_, z_]], not[subclass[u_, trv[x_]]]] := 
      True

Theorem.  If x is a set, then so are its positive powers.

Map[not, 
      SubstTest[and, implies[p2, p3], implies[and[p1, p3], p4], 
        not[implies[and[p1, p2], p4]], {p1 -> member[x, z], 
          p2 -> member[y, dif[omega, set[0]]], 
          p3 -> subclass[image[power[x], set[y]], trv[x]], 
          p4 -> member[image[power[x], set[y]], V]}]]

or[equal[0, y_], member[image[power[x_], set[y_]], V], 
        not[member[x_, z_]], not[member[y_, omega]]] := True

Lemma.  If they are sets, then the positive powers belong to the class considered in the preceding section.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> set[y], 
        v -> intersection[omega, complement[set[0]]], 
        w -> VERTSECT[power[x]]}]

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

Theorem.  The y-th positive power of a unary operation x is a unary operation.

Map[not, 
      SubstTest[and, implies[and[p1, p2], p3], implies[and[p2, p3], p4], 
        implies[p1, p5], implies[and[p4, p5], p6], 
        not[implies[and[p1, p2], p6]], {p1 -> member[x, UNOPS], 
          p2 -> member[y, dif[omega, set[0]]], 
          p3 -> member[image[power[x], set[y]], V], 
p4 -> 
            member[image[power[x], set[y]], 
              image[VERTSECT[power[x]], 
                intersection[omega, 
                  complement[set[0]]]]], 
p5 -> 
            subclass[
              image[VERTSECT[power[x]], 
                intersection[omega, complement[set[0]]]], 
              UNOPS], 
p6 -> 
            member[image[power[x], set[y]], UNOPS]}]]

or[equal[0, y_], member[image[power[x_], set[y_]], UNOPS], 
        not[member[x_, UNOPS]], not[member[y_, omega]]] := True