intersections of rationals

Johan G. F. Belinfante
2012 July 24

SetDirectory["l:"];  << goedel.12jul23a

summary

If  x  and  y  are rational numbers, then either  x = y  or  x ⋂ y = {id[ω]} × {id[ω]}.

general results

Theorem.  A general result.

SubstTest[implies, equal[u, v], 
        equal[union[u, w], union[v, w]], {u -> dif[x, z], 
          v -> dif[y, z], w -> z}] // Reverse

or[equal[union[x_, z_], union[y_, z_]], 
        not[equal[intersection[complement[z_], x_], 
            intersection[complement[z_], y_]]]] := True

Theorem.  Another general result.

SubstTest[implies, and[equal[t, u], equal[v, w]], 
        equal[union[t, v], union[u, w]], {t -> dif[x, z], 
          u -> dif[y, z], v -> intersection[x, z], 
          w -> intersection[y, z]}] // Reverse

or[equal[x_, y_], 
        not[equal[intersection[complement[z_], x_], 
            intersection[complement[z_], y_]]], 
        not[equal[intersection[x_, z_], intersection[y_, z_]]]] := 
      True

Corollary.

Map[not, 
        SubstTest[and, implies[and[p2, p3], p4], implies[and[p1, p4], p5], 
          not[implies[and[p1, p2, p3], p5]], {p1 -> 
              equal[dif[x, z], dif[y, z]], p2 -> subclass[z, x], 
            p3 -> subclass[z, y], 
            p4 -> equal[intersection[x, z], intersection[y, z]], 
            p5 -> equal[x, y]}]] // Reverse

or[equal[x_, y_], 
        not[equal[intersection[complement[z_], x_], 
            intersection[complement[z_], y_]]], not[subclass[z_, x_]], 
        not[subclass[z_, y_]]] := True

Corollary.

Map[implies[and[member[w, x], member[w, y]], #] &, 
      SubstTest[implies, 
          and[equal[dif[x, t], dif[y, t]], subclass[t, x], subclass[t, y]], 
          equal[x, y], t -> set[w]] // Reverse]

or[equal[x_, y_], 
        not[equal[intersection[complement[set[w_]], x_], 
            intersection[complement[set[w_]], y_]]], not[member[w_, x_]], 
        not[member[w_, y_]]] := True

derivation

Lemma.  Introduce variables.

SubstTest[implies, and[member[u, v], subclass[v, w]], 
        member[u, w], {u -> pair[x, y], 
          v -> cartsq[
              image[IMAGE[id[complement[id[set[id[omega]]]]]], RATS]], 
          w -> union[Id, DISJOINT]}] // Reverse

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

Lemma.  For rationals, removing the point at the origin is equivalent to removing the vertical axis in the  Z × Z  plane.

SubstTest[implies, member[x, z], 
        member[dif[x, y], 
          image[IMAGE[id[complement[y]]], z]], {y -> 
            cart[set[id[omega]], set[id[omega]]], z -> RATS}] // 
      Reverse

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

Lemma.

SubstTest[or, equal[0, intersection[u, v]], equal[u, v], 
        not[member[u, 
            image[IMAGE[id[cart[complement[set[id[omega]]], V]]], RATS]]], 
        not[member[v, 
            image[IMAGE[id[cart[complement[set[id[omega]]], V]]], 
              RATS]]], {u -> 
            dif[x, cart[set[id[omega]], set[id[omega]]]], 
          v -> dif[y, cart[set[id[omega]], set[id[omega]]]]}] // 
      Reverse

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

Lemma.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p2, p3], or[p4, p5]], 
          not[implies[p1, or[p4, p5]]], {p1 -> 
              member[pair[x, y], cart[RATS, RATS]], 
            p2 -> 
              member[intersection[x, 
                  complement[cart[set[id[omega]], set[id[omega]]]]], 
                image[IMAGE[id[cart[complement[set[id[omega]]], V]]], RATS]], 
            p3 -> member[
                intersection[y, 
                  complement[cart[set[id[omega]], set[id[omega]]]]], 
                image[IMAGE[id[cart[complement[set[id[omega]]], V]]], RATS]], 
            p4 -> 
              equal[intersection[x, 
                  complement[cart[set[id[omega]], set[id[omega]]]]], 
                intersection[y, 
                  complement[cart[set[id[omega]], set[id[omega]]]]]], 
            p5 -> 
              disjoint[
                intersection[x, 
                  complement[cart[set[id[omega]], set[id[omega]]]]], 
                intersection[y, 
                  complement[cart[set[id[omega]], set[id[omega]]]]]]}]] // 
      Reverse

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

Corollary.  (A particular case of a general result that is needed here.)

SubstTest[or, equal[x, y], 
        not[equal[intersection[x, complement[set[w]]], 
            intersection[y, complement[set[w]]]]], not[member[w, x]], 
        not[member[w, y]], w -> PAIR[id[omega], id[omega]]] // 
      Reverse

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

Lemma.

Map[
        implies[#, 
            equal[cart[set[id[omega]], set[id[omega]]], 
              intersection[x, y]]] &, 
        SubstTest[and, subclass[u, v], 
          subclass[v, u], {u -> intersection[x, y], 
            v -> cart[set[id[omega]], set[id[omega]]]}]] // 
      Reverse

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

Theorem.

Map[not, 
        SubstTest[and, implies[p1, or[p2, p3]], implies[p1, p4], 
          implies[p1, p5],    
          not[implies[p1, or[p6, p7]]], {p1 -> 
              member[pair[x, y], cart[RATS, RATS]], 
            p2 -> equal[
                intersection[x, 
                  complement[cart[set[id[omega]], set[id[omega]]]]], 
                intersection[y, 
                  complement[cart[set[id[omega]], set[id[omega]]]]]], 
            p3 -> subclass[intersection[x, y], 
                cart[set[id[omega]], set[id[omega]]]], 
            p4 -> subclass[cart[set[id[omega]], set[id[omega]]], x], 
            p5 -> subclass[cart[set[id[omega]], set[id[omega]]], y], 
            p6 -> equal[x, y], 
            p7 -> 
              equal[intersection[x, y], 
                cart[set[id[omega]], set[id[omega]]]]}]] // 
      Reverse

or[equal[cart[set[id[omega]], set[id[omega]]], intersection[x_, y_]], 
        equal[x_, y_], not[member[x_, RATS]], not[member[y_, RATS]]] := 
      True