a wrapper for well-founded relations

Johan G. F. Belinfante
2004 September 18

SetDirectory["i:"];  << goedel61.14a; << tools.m

summary

A wrapper wf[x] for well-founded relations is introduced, and some of its basic properties are deduced.

definition

The wrapper wf[x] is defined by the following membership rule:

member[w_, wf[x_]] := 
      and[member[w, x], member[first[w], V], 
        not[member[second[w], U[subvar[x]]]]]

normalization

The basic normalization result:

wf[x] // Normality // Reverse

composite[id[complement[U[subvar[x_]]]], x_] := wf[x]

A related rewrite rule:

Assoc[id[x], id[complement[U[subvar[y]]]], y] // Reverse

composite[id[intersection[x_, complement[U[subvar[y_]]]]], y_] := 
      composite[id[x], wf[y]]

basic properties

Simplification rule.

Assoc[Id, id[complement[U[subvar[x]]]], x]

composite[Id, wf[x_]] := wf[x]

The well-founded part of  composite[Id, x] is the same as the well-founded part of  x.

wf[composite[Id, x]] // Normality

wf[composite[Id, x_]] := wf[x]

using wf to remove literals involving the WELLFOUNDED predicate

Lemma.

equal[intersection[x, P[complement[U[x]]]], 
        intersection[x, singleton[0]]] // AssertTest

intersection[x_, P[complement[U[x_]]]] := 
      intersection[x, singleton[0]]

The only set subvariant under wf[x] is the empty set.

subvar[wf[x]] // Renormality

subvar[wf[x_]] := singleton[0]

The relation wf[x] is well-founded.  This rewrite rule can be used to remove literals involving the WELLFOUNDED predicate by introducing wf wrappers.

WELLFOUNDED[wf[x]] // AssertTest

WELLFOUNDED[wf[x_]] := True

For example, the theorem that any well-founded relation is irreflexive can now be expressed using a single literal:

SubstTest[implies, WELLFOUNDED[w], equal[fix[w], 0], 
      w -> wf[x]]

fix[wf[x_]] := 0

Similarly:

SubstTest[implies, WELLFOUNDED[w], equal[fix[trv[w]], 0], 
      w -> wf[x]]

fix[trv[wf[x_]]] := 0

wrapper removal

This section is concerned with rules needed to remove the wf wrapper, restoring the WELLFOUNDED predicate.  We begin with a simple lemma:

equal[intersection[range[x], U[subvar[x]]], U[subvar[x]]]

This justifies adding the following rewrite rule:

intersection[range[x_], U[subvar[x_]]] := U[subvar[x]]

The following rule can be used to remove  wf  wrappers.  Note that this also implies that every well-founded relation can be written in the form  wf[x].

equal[x, wf[x]] // AssertTest

equal[x_, wf[x_]] := WELLFOUNDED[x]

Corollary:  The  wf  wrapper satisfies the following idempotence property:

equal[wf[wf[x]], wf[x]]

wf[wf[x_]] := wf[x]

subclass and intersection results

The well-founded part of  x  is contained in  x.

subclass[wf[x], x] // AssertTest

subclass[wf[x_], x_] := True

The reverse inclusion holds if and only if  x  is well-founded.

subclass[x, wf[x]] // AssertTest

subclass[x_, wf[x_]] := WELLFOUNDED[x]

Every subclass of a well-founded relation is well-founded.

SubstTest[implies, and[subclass[x, v], WELLFOUNDED[v]], WELLFOUNDED[x], 
      v -> wf[y]]

or[not[subclass[x_, wf[y_]]], WELLFOUNDED[x_]] := True

Two corollaries of this are:

SubstTest[implies, and[subclass[u, v], WELLFOUNDED[v]], 
      WELLFOUNDED[u], {u -> intersection[x, wf[y]], 
        v -> wf[y]}]

WELLFOUNDED[intersection[x_, wf[y_]]] := True

SubstTest[implies, and[subclass[u, v], WELLFOUNDED[v]], 
      WELLFOUNDED[u], {u -> composite[id[x], wf[y]], 
        v -> wf[y]}]

WELLFOUNDED[composite[id[x_], wf[y_]]] := True

Wrapper versions of these results:

equal[wf[intersection[x, wf[y]]], intersection[x, wf[y]]]

wf[intersection[x_, wf[y_]]] := intersection[x, wf[y]]

equal[wf[composite[id[x], wf[y]]], composite[id[x], wf[y]]]

wf[composite[id[x_], wf[y_]]] := composite[id[x], wf[y]]

some examples

The following two examples imply that  wf  cannot be monotone.

wf[0] // Normality

wf[0] := 0

wf[V] // Normality

wf[V] := 0

The following two examples of well-founded relations have been extensively investigated.

SubstTest[composite, id[complement[U[subvar[x]]]], x, x -> E] // 
      Reverse

wf[E] := composite[id[REGULAR], E]

SubstTest[composite, id[complement[U[subvar[x]]]], x, x -> PS] // 
      Reverse

wf[PS] := composite[id[FINITE], PS]

some other examples

wf[Id] // Normality

wf[Id] := 0

wf[id[x]] // Normality

wf[id[x_]] := 0

wf[S] // Normality

wf[S] := 0

wf[inverse[S]] // Normality

wf[inverse[S]] := 0

wf[inverse[E]] // Normality

wf[inverse[E]] := 0

serendipity: wf[Di] = 0

Some unexpected discoveries were made in the course of obtaining a formula for  wf[Di].  The class of sets subvariant under the diversity relation  Di  is the complement of the class of singletons.

subvar[Di]

If one attempts to obtain a formula for  wf[Di]  by using a normality test, one quickly discovers that one needs a formula for the class  U[complement[range[SINGLETON]]].  Most of this section is concerned with obtaining such a formula, and related results concerning the class of sets with precisely two elements,  image[PAIRSET, Di].   This class contains neither singletons nor the empty set:

member[singleton[x], image[PAIRSET, Di]] // AssertTest

member[singleton[x_], image[PAIRSET, Di]] := False

Removing the variable  x  here yields:

SubstTest[class, x, member[singleton[x], y], y -> image[PAIRSET, Di]] // 
      Reverse

image[inverse[SINGLETON], image[PAIRSET, Di]] := 0

From this one readily derives the unsurprising fact that this class is disjoint fron the class of singetons:

ImageComp[SINGLETON, inverse[SINGLETON], image[PAIRSET, Di]]

intersection[image[PAIRSET, Di], range[SINGLETON]] := 0

The needed formula about the union of the complement of the class of singletons can be derived as follows:

Map[assert, 
      SubstTest[implies, subclass[x, y], 
        subclass[U[x], U[y]], {x -> image[PAIRSET, Di], 
          y -> complement[range[SINGLETON]]}]]

U[complement[range[SINGLETON]]] := V

Now one can use Normality to derive a formula for  wf[Di].

wf[Di] // Normality

wf[Di] := 0

empty wf[x]

The following provides a simple criterion for wf[x] to be empty.

SubstTest[equal, 0, composite[id[w], x], 
      w -> complement[U[subvar[x]]]]

equal[0, wf[x_]] := subclass[range[x], U[subvar[x]]]