ordinal addition, part 5.

Johan G. F. Belinfante
2010 December 17

SetDirectory["l:"];  << goedel.10dec16b

summary

This fifth notebook in a series about ordinal addition is concerned with a strict monotonicity property of ordinal addition.  Some results are derived first using ord wrappers, and later generalized, removing the ord wrappers.

monotonicity properties of ordplus[x]

Both ordplus[x] and its inverse are monotone with respect to membership.

Theorem.

SubstTest[subclass, enum[t], composite[S, IMAGE[enum[t]]], 
        t -> 
          intersection[OMEGA, complement[x], 
            image[V, intersection[OMEGA, set[x]]]]] // Reverse

subclass[ordplus[x_], composite[S, IMAGE[ordplus[x_]]]] := 
      True

Theorem.

SubstTest[subclass, inverse[enum[t]], 
        composite[S, IMAGE[inverse[enum[t]]]], 
        t -> 
          intersection[OMEGA, complement[x], 
            image[V, intersection[OMEGA, set[x]]]]] // Reverse

subclass[inverse[ordplus[x_]], 
        composite[S, IMAGE[inverse[ordplus[x_]]]]] := True

Theorem.

SubstTest[subclass, enum[t], S, 
        t -> intersection[OMEGA, complement[x], 
            image[V, intersection[OMEGA, set[x]]]]] // Reverse

subclass[ordplus[x_], S] := True

monotonicity of ordadd[x, – ]

In this section a rewrite rule is derived about monotonicity of  ordadd[x, – ] when  x  is fixed.   Since there are three variables and each may or may not be an ordinal, many lemmas are needed to cover all possible cases.

Lemma.  A result obtained by specializing a general theorem about  enum[x].

SubstTest[implies, and[member[y, z], member[z, domain[enum[t]]]], 
        member[APPLY[enum[t], y], APPLY[enum[t], z]], 
        t -> intersection[OMEGA, complement[x], 
            image[V, intersection[OMEGA, set[x]]]]] // Reverse

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

Lemma.   If  ordadd[x, y]  is a set, then  x  is an ordinal.

Map[or[member[x, OMEGA], #] &, 
        SubstTest[implies, member[t, z], member[t, V], 
          t -> ordadd[x, y]]] // Reverse

or[member[x_, OMEGA], not[member[ordadd[x_, y_], z_]]] := 
      True

Lemma.   If  ordadd[x, y]  is a set, then  y  is an ordinal.

Map[or[member[y, OMEGA], #] &, 
        SubstTest[implies, member[t, z], member[t, V], 
          t -> ordadd[x, y]]] // Reverse

or[member[y_, OMEGA], not[member[ordadd[x_, y_], z_]]] := 
      True

Theorem.  The case that  x  and  y  are ordinals but   z  is not.

SubstTest[implies, and[member[u, v], equal[v, w]], 
        member[u, w], {u -> ordadd[x, y], v -> V, 
          w -> ordadd[x, z]}] // Reverse

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

Lemma.     A result obtained by specializing a general theorem about  enum[x].  (This has a redundant literal)

SubstTest[or, member[y, z], not[member[z, domain[enum[t]]]], 
        not[member[APPLY[enum[t], y], APPLY[enum[t], z]]], 
        t -> intersection[OMEGA, complement[x], 
            image[V, intersection[OMEGA, set[x]]]]] // Reverse

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

Theorem.  (Removing a redundant literal from the result obtained in the preceding lemma.

SubstTest[and, implies[p, q], 
      or[p, q], {p -> member[x, OMEGA], 
        q -> or[member[y, z], not[member[z, OMEGA]], 
            not[member[ordadd[x, y], ordadd[x, z]]]]}]

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

Main Theorem.   A general rewrite rule about strict monotonicity of ordadd[x, – ] for fixed  x.

equiv[member[ordadd[x, y], ordadd[x, z]], 
          or[and[member[x, OMEGA], member[y, OMEGA], not[member[z, OMEGA]]], 
            and[member[x, OMEGA], member[y, z], member[z, OMEGA]]]] // not // 
      not

member[ordadd[x_, y_], ordadd[x_, z_]] := 
      or[and[member[x, OMEGA], member[y, OMEGA], not[member[z, OMEGA]]], 
        and[member[x, OMEGA], member[y, z], member[z, OMEGA]]]

corollaries

Corollary.   A case where one of the variables is  0.

SubstTest[member, ordadd[x, y], ordadd[x, t], t -> 0] // 
      Reverse

member[ordadd[x_, y_], x_] := False

A similar result will be obtained using  subclass  in place of  member.   Inclusions for ordinals can be restated as negated reversed membership.  For this it is convenient to introduce  ord  wrappers.

Corollary.

SubstTest[subclass, ord[x], ord[t], t -> ordadd[ord[x], ord[y]]] // 
      Reverse

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

Lemma.  (Removing the two  ord  wrappers.)

SubstTest[implies, and[equal[x, ord[u]], equal[y, ord[v]]], 
        subclass[x, ordadd[x, y]], {u -> x, v -> y}] // 
      Reverse

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

Lemma.  (Needed to eliminate two redundant literals in the preceding lemma.)

SubstTest[implies, equal[v, V], subclass[w, v], 
          v -> ordadd[x, y]] // Reverse // MapNotNot

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

The above two lemmas can be combined, eliminating two redundant literals.

Theorem.

SubstTest[and, implies[p, q], 
      or[p, q], {p -> and[member[x, OMEGA], member[y, OMEGA]], 
        q -> subclass[x, ordadd[x, y]]}]

subclass[x_, ordadd[x_, y_]] := True