∈ characterization of H[x]

Johan G. F. Belinfante
2008 September 1

SetDirectory["l:"];  << goedel.08aug31b;  <<  tools.m

summary

The full core H[x] of a class x is the largest full subclass of x.  Each element w of H[x] is said to belong hereditarily to the class x; not only is w a member of x, but all members of w are members of x, as are all members of members of w, and so on, ad infinitum.  If one assumes the axiom of regularity, then y =H[x] can be characterized as the only class which satisfies the equation y = x ⋂ P[y]  (see for example, the following text by Thomas Jech, page 74):

"Thomas Jech, Set Theory, Academic Press,San Diego, 1978.";

This characterization in fact can only be true if AxReg holds, because if one takes x = V and y = REGULAR, this condition reduces to

equiv[equal[y, H[x]], equal[y, intersection[x, P[y]]]] /. {x -> V, 
        y -> REGULAR}

In the GOEDEL program, the axiom of regularity is not automatically assumed to hold, so this characterization of H[x] must be modified accordingly.  In this notebook it is shown using ∈ induction that this characterization holds if one adds the condition that x is a subclass of the class REGULAR, defined as follows:

class[x, 
      forall[y, 
        implies[member[x, y], 
          exists[w, and[member[w, y], disjoint[w, y]]]]]]

It should be noted that even without assuming any extra hypothesis, an implication in one direction holds:

implies[equal[y, H[x]], equal[y, intersection[x, P[y]]]]

It is only for the reverse implication that one needs an extra hypothesis.

derivation

Lemma.  (Inclusion in one direction.)

Map[implies[#, subclass[y, H[x]]] &, 
      equal[y, intersection[x, P[y]]] // AssertTest]

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

Observation.  The principle of ∈-induction in the absence AxReg holds in the following modified form:

implies[and[full[x], subclass[intersection[x, P[y]], y]], 
      subclass[intersection[REGULAR, x], y]]

Lemma.  From the principle of ∈-induction one obtains the following corollary.

SubstTest[implies, and[full[t], subclass[intersection[t, P[y]], y]], 
        subclass[intersection[REGULAR, t], y], t -> H[x]] // 
      Reverse

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

Corollary.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> subclass[intersection[x, P[y]], y], 
            p2 -> subclass[intersection[H[x], P[y]], y], 
            p3 -> subclass[intersection[REGULAR, H[x]], y]}]] // 
      Reverse

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

Theorem.   (Characterization of y = H[x] when x ⊂ REGULAR as the only solution of the equation y = x ⋂ P[y].)

Map[not, 
        SubstTest[and, implies[p3, p4], implies[and[p4, p5], p6], 
          implies[p2, p7], 
          not[implies[and[p1, p2], p8]], {p1 -> subclass[x, REGULAR], 
            p2 -> equal[y, intersection[x, P[y]]], 
            p3 -> subclass[intersection[x, P[y]], y], 
            p4 -> subclass[intersection[REGULAR, H[x]], y], 
            p5 -> subclass[H[x], REGULAR], p6 -> subclass[H[x], y], 
            p7 -> subclass[y, H[x]], p8 -> equal[y, H[x]]}]] // 
      Reverse

or[equal[y_, H[x_]], not[equal[y_, intersection[x_, P[y_]]]], 
        not[subclass[x_, REGULAR]]] := True

Comment.  The execution time for this theorem is approximately 18 seconds on an HP Pavilion computer.  This execution time has been reduced from almost 62 seconds by simply omitting the following two additional steps that are needed for a complete proof:  implies[p1, p5],  implies[p2, p3].  The rewrite rules of the GOEDEL program automatically supply these two missing steps.

Corollary.  (If the axiom of regularity holds then y = H[x] is the only solution of y = x ⋂ P[y].)

SubstTest[implies, equal[v, REGULAR], 
        or[equal[y, H[x]], not[equal[y, intersection[x, P[y]]]], 
          not[subclass[x, v]]], v -> V] // Reverse

or[equal[y_, H[x_]], not[AxReg], 
        not[equal[y_, intersection[x_, P[y_]]]]] := True