inverse[PRIMESEQ]

Johan G. F. Belinfante
2011 August 12

SetDirectory["l:"]; << goedel.11aug11a

summary

In this notebook a recursive  APPLY  formula for the inverse of  PRIMESEQ  is derived, inspired by the discussion on page 130 of Patrick Suppes’ book Axiomatic Set Theory.

derivation

Theorem.

ApComp[inverse[PRIMESEQ], PRIMESEQ, x]

APPLY[inverse[PRIMESEQ], APPLY[PRIMESEQ, x_]] := 
      union[x, complement[image[V, intersection[omega, set[x]]]]]

Corollary.  An example: the least prime is 2.

ApComp[inverse[PRIMESEQ], PRIMESEQ, 0]

APPLY[inverse[PRIMESEQ], succ[set[0]]] := 0

Theorem.

Map[equal[x, #] &, 
        SubstTest[APPLY, oopart[t], APPLY[inverse[oopart[t]], x], 
          t -> PRIMESEQ]] // Reverse

equal[x_, APPLY[PRIMESEQ, APPLY[inverse[PRIMESEQ], x_]]] := 
      or[equal[V, x], member[x, PRIMES]]

Theorem.  A simplification rule.

IminComp[id[PRIMES], PRIMESEQ, x] // Reverse

image[inverse[PRIMESEQ], intersection[PRIMES, x_]] := 
      image[inverse[PRIMESEQ], x]

Theorem.

SubstTest[image, inverse[PRIMESEQ], intersection[PRIMES, t], 
      t -> APPLY[PRIMESEQ, nat[x]]]

image[inverse[PRIMESEQ], APPLY[PRIMESEQ, nat[x_]]] := nat[x]

Corollary.

SubstTest[implies, equal[x, nat[t]], 
        equal[image[inverse[PRIMESEQ], APPLY[PRIMESEQ, x]], x], t -> x] // 
      Reverse

or[equal[x_, image[inverse[PRIMESEQ], APPLY[PRIMESEQ, x_]]], 
        not[member[x_, omega]]] := True

Theorem.

SubstTest[member, APPLY[funpart[t], x], range[funpart[t]], 
        t -> inverse[PRIMESEQ]] // Reverse

member[APPLY[inverse[PRIMESEQ], x_], omega] := 
      member[x, PRIMES]

Lemma.

SubstTest[or, equal[t, image[inverse[PRIMESEQ], APPLY[PRIMESEQ, t]]], 
        not[member[t, omega]], t -> APPLY[inverse[PRIMESEQ], x]] // 
      Reverse

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

Theorem.

SubstTest[implies, 
        equal[t, APPLY[PRIMESEQ, APPLY[inverse[PRIMESEQ], x]]], 
        or[equal[APPLY[inverse[PRIMESEQ], x], image[inverse[PRIMESEQ], t]], 
          not[member[x, PRIMES]]], t -> x] // Reverse

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

Converse Theorem.

SubstTest[implies, and[equal[u, v], member[v, w]], 
        member[u, w], {u -> APPLY[inverse[PRIMESEQ], x], 
          v -> image[inverse[PRIMESEQ], x], w -> V}] // 
      Reverse

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

Main Theorem.  A recursion relation for inverse[PRIMESEQ].

equiv[equal[APPLY[inverse[PRIMESEQ], x], image[inverse[PRIMESEQ], x]], 
      member[x, PRIMES]]

equal[APPLY[inverse[PRIMESEQ], x_], image[inverse[PRIMESEQ], x_]] := 
      member[x, PRIMES]