well-founded trichotomous relations

Johan G. F. Belinfante
2009 October 27

SetDirectory["l:"];  <<  goedel.09oct26a; << tools.m

summary

If a well-founded relation is trichotomous on the union of its domain and range, then its reflexive closure is a well-ordering.

temporary definitions

The following temporary abbreviations will be used.

irreflexive[r_, s_] := disjoint[s, fix[r]]

transitive[r_, s_] := TRANSITIVE[restrict[r, s, s]]

trichotomous[r_, s_] := 
      subclass[cart[s, s], union[Id, r, inverse[r]]]

strictwellorder[r_, s_] := 
      and[trichotomous[r, s], WELLFOUNDED[composite[id[s], r]]]

Reference:

"Patrick Suppes, Axiomatic Set Theory, Dover Publications, New York, 1972.";

derivation

Lemma.   (Corollary of Suppes’s Theorem 62.)

SubstTest[implies, strictwellorder[r, s], 
        transitive[r, s], {r -> wf[x], s -> udora[wf[x]]}] // 
      Reverse

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

Lemma.  If a strict order is trichotomous on the union of its domain and range, then its reflexive closure is a total-order.

SubstTest[implies, 
        and[equal[0, fix[r]], 
          subclass[
            cart[union[domain[r], range[r]], union[domain[r], range[r]]], 
            union[Id, r, inverse[r]]], TRANSITIVE[r]], 
        TOTALORDER[union[r, id[union[domain[r], range[r]]]]], 
        r -> wf[x]] // Reverse

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

Lemma.  A total order whose strict part is well-founded is a well-ordering.

Map[
      implies[TOTALORDER[
            union[id[union[domain[wf[x]], range[wf[x]]]], wf[x]]], #] &, 
      SubstTest[and, TOTALORDER[t], WELLFOUNDED[intersection[Di, t]], 
        t -> union[id[union[domain[wf[x]], range[wf[x]]]], 
            wf[x]]]]

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

Lemma.  (Combining the preceding lemmas.)

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
          implies[p3, p4], 
          not[implies[p1, p4]], {p1 -> 
              trichotomous[wf[x], udora[wf[x]]], p2 -> TRANSITIVE[wf[x]], 
            p3 -> TOTALORDER[
                union[id[union[domain[wf[x]], range[wf[x]]]], wf[x]]], 
            p4 -> 
              WELLORDER[
                union[id[union[domain[wf[x]], range[wf[x]]]], wf[x]]]}]] // 
      Reverse

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

The main theorem is obtained by removing the wf wrapper.

Theorem.  If a well-founded relation is trichotomous on the union of its domain and range, then its reflexive closure is a well-ordering.

SubstTest[implies, and[equal[x, wf[t]], trichotomous[x, udora[x]]], 
        WELLORDER[union[x, id[udora[x]]]], t -> x] // Reverse

or[not[
          subclass[
            cart[union[domain[x_], range[x_]], union[domain[x_], range[x_]]], 
            union[Id, x_, inverse[x_]]]], not[WELLFOUNDED[x_]], 
        WELLORDER[union[x_, id[union[domain[x_], range[x_]]]]]] := 
      True