[FOM] Predicative Powerset Construction

steve newberry stevnewb at ix.netcom.com
Thu Feb 6 12:12:55 EST 2003

```CONSTRUCTION OF PREDICATIVE POWERSET
by  R. Stephen Newberry [February 5, 2003]

Outline of procedure:

(1) Take a countable set, any countable set; call it  S.

(2) Define a functor ' * ' which converts S  to a sequence, any
sequence whose elements are all and only the elements of  S.
(If this is considered as invoking the Countable Axiom of Choice,
so be it.) Call the sequence  *S .

(3) Define a functor ' \$', which takes as argument a countable sequence,
let's call it  X, and returns a "sequence of ordinal structure" isomorphic
with omega. Thus if  X  were <0, 1, 2, 3, . . . > then \$(X) would be
< {0}, {0, 1}, {0, 1, 2}, {0, 1, 2, 3 } . . . >; if  X  is a set rather
than a sequence,
then \$(X) = X.

(4) Define a "map function" '^Pwr' which takes as argument an infinite
sequence  X  of sets and returns an infinite sequence of powersets, one for
each component set of the given sequence; if  X  is a set rather than a
sequence of sets, then ^Pwr(X) = Pwr(X). ['Pwr' denotes standard powerset.]

(5) Defined a special union 'U, which takes an infinite sequence of
sets as argument and returns the union of that sequence of sets ;
if  X  is a set rather than a sequence of sets, then 'U(X) = X.

(6) Define the Predicative Powerset functor 'PPwr' as

PPwr(S) =df= 'U(^Pwr(\$(*S)))

E.g., if  \$(*S) were < {0}, {0, 1}, {0, 1, 2}, {0, 1, 2, 3 } . . . >; then

^Pwr(\$(*S)) would be < Pwr{0}, Pwr{0, 1}, Pwr{0,1, 2} , Pwr{0, 1, 2 },
Pwr{0, 1, 2, 3 } . . . >

and  PPwr(S) =df= 'U(^Pwr(\$(*S))) is  U(< Pwr{0}, Pwr{0, 1}, Pwr{0,1, 2} ,
Pwr{0, 1, 2 }, Pwr{0, 1, 2, 3 } . . . >),

which differs from the standard powerset Pwr(S) in only two respects:

(1): Every element of  PPwr(S) is predicatively defined; and

(2): PPwr(S) is a union of countably many countable sets, and is therefore
itself countable. Think of

PPwr(S) as being just exactly the standard powerset Pwr(S) **after** all
the IMpredicative subsets

(such as the Diagonal Function) have been removed.