well-foundedness of strict divisibility for natural numbers

Johan G. F. Belinfante
2005 February 3

SetDirectory["i:"]; << goedel66.01a; << tools.m

summary

It is shown in this notebook that the strict divisibility relation  intersection[Di, DIV] is well-founded.  The derivation uses a theorem discovered 2004 September 23 that can be viewed as a generalization of the theorem that lexicographic products of well founded relations are well-founded.  (See the notebook wf-u.nb.)

a conditional rewrite rule

The following example illustrates an opportunity for a new rewrite rule.

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

The wf wrapper can be removed for any well-founded relation.

equal[wf[x], x]

This will be added as a conditional rewrite rule.

wf[x_] := x  /;  WELLFOUNDED[x]

The example cited above now simplifies.

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

well-foundedness for strict divisibility

The main idea is to use the fact that for non-zero natural numbers, if  m  strictly divides  n, then  m  belongs to  n.

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], image[w, v]], {u -> intersection[DIV, Di], 
        v -> union[composite[id[omega], E], 
            cart[dif[omega, set[0]], set[0]]], 
        w -> id[cart[V, complement[set[0]]]]}]

subclass[composite[id[complement[set[0]]], intersection[Di, DIV]], E] := 
      True

Since the restriction of the membership relation to natural numbers is well-founded, so is strict divisibility for non-zero numbers.

SubstTest[implies, and[subclass[u, v], WELLFOUNDED[v]], 
      WELLFOUNDED[
        u], {u -> composite[id[complement[set[0]]], intersection[Di, DIV]], 
        v -> composite[id[omega], E]}]

% /. Equal -> SetDelayed

The complement of this relation is also well-founded;  no new rule is needed for this.

WELLFOUNDED[composite[id[set[0]], intersection[Di, DIV]]]

Lemma.

SubstTest[union, id[x], id[z], z -> set[y]]

union[cart[set[y_], set[y_]], id[x_]] := 
      id[union[x, set[y]]]

Lemma.

SubstTest[composite, union[u, v], 
        w, {u -> id[set[0]], v -> id[complement[set[0]]], 
          w -> intersection[Di, DIV]}] // Reverse

% /. Equal -> SetDelayed

In the course of showing that the lexicographic product of well founded relations is well founded, the following generalization was discovered.

implies[subclass[composite[wf[x], wf[y]], wf[y]], 
      WELLFOUNDED[union[wf[x], wf[y]]]]

This result can be applied here:

SubstTest[implies, subclass[composite[wf[y], wf[x]], wf[x]], 
      WELLFOUNDED[
        union[wf[x], wf[y]]], {x -> 
          cart[intersection[omega, complement[set[0]]], set[0]], 
        y -> composite[id[complement[set[0]]], 
            intersection[Di, DIV]]}]

WELLFOUNDED[intersection[Di, DIV]] := True

another simplification rule

The following simplification rule was not used here, but might be useful in other applications involving explicit intersections with the diversity relation Di.

equal[intersection[Di, wf[x]], wf[x]]

intersection[Di, wf[x_]] := wf[x]