[FOM] Predicative Powerset Construction

[steve newberry]

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.

Please comment.

R. Stephen Newberry