a reify rule for wo[x]

Johan G. F. Belinfante
2007 May 2

SetDirectory["l:"]; <<  goedel93.02a; << tools.m

summary

A reify rule for the well-ordering wrapper wo[x] is derived.  The inspiration for this derivation is the following rewrite rule that expresses the fact that a relation is a well-order if every restriction of it is:

subclass[image[IMAGE[id[x]], image[CART, Id]], WO]

The idea is to hide most of the details of the rather complicated definition of wellordering into the constant WO, which is independent of x, and therefore plays little role in the reification process.  An example is provided to show that this all works just fine.

derivation

Lemma.   (Temporary rewrite rule.)

wo[x] // Normality // Reverse

composite[Id, 
        intersection[
          complement[
            image[V, intersection[complement[fix[x_]], domain[x_]]]], 
          complement[image[V, intersection[complement[fix[x_]], range[x_]]]], 
          complement[
            image[V, 
              intersection[complement[domain[funpart[LEAST[x_]]]], 
                complement[set[0]], P[fix[x_]]]]], x_]] := wo[x]

Main Theorem.  (A succinct formula for wo[x] that hides the complexities of the definition into the constant WO.)

composite[
        id[complement[
            image[V, 
              intersection[complement[WO], 
                image[IMAGE[id[x]], image[CART, Id]]]]]], x] // 
      Normality

composite[
        id[complement[
            image[V, 
              intersection[complement[WO], 
                image[IMAGE[id[x_]], image[CART, Id]]]]]], x_] := 
      wo[x]

reify rule for wo[x]

Theorem.

SubstTest[reify, x, 
        composite[
          id[complement[
              image[V, 
                intersection[complement[w], 
                  image[IMAGE[id[f[x]]], image[CART, Id]]]]]], f[x]], 
        w -> WO] // Reverse

reify[x_, wo[y_]] := 
      composite[id[cart[V, V]], reify[x, y], 
        id[image[inverse[SINGLETON], 
            lb[image[inverse[CART], 
                image[inverse[IMAGE[id[reify[x, y]]]], 
                  image[inverse[IMAGE[SECOND]], WO]]], 
              image[CART, Id]]]]]

an elementary example

In this section the new reify rule is used to obtain a variable-free reformulation of the following basic fact:

range[wo[x]]

Lemma.

equal[
      intersection[WO, 
        complement[image[inverse[IMAGE[id[cart[V, V]]]], WO]]], 0]

intersection[WO, 
        complement[image[inverse[IMAGE[id[cart[V, V]]]], WO]]] := 
      0

Map[composite[VERTSECT[#], id[WO]] &, 
      SubstTest[reify, x, range[f[x]], f -> wo]]

composite[IMAGE[SECOND], id[WO]] := 
      composite[IMAGE[inverse[DUP]], id[WO]]