[FOM] re: What do you lose if you ditch Powerset?

[A.P. Hazen]

    Here's the OBVIOUS answer to Timothy Chow's question (with further 
questions).
    Under appropriate codings, the hereditarily finite sets are "the 
same thing" as the natural numbers: ZF without INFINITY is (modulo 
painful coding and decoding) about the same thing as First Order PA. 
(MY question: is there a reference for details on this?  And for 
variants: ZFC without INF, Z without INF?  Are these really "the same 
thing" when you make that notion precise as, say, mutual 
interpretability?  These are things that ought to be well-known, but 
I don't know of a published source.)
    Much weaker systems suffice to prove the existence of each 
individual Hereditarily Finite Set: the Tarski-Szmielew system 
axiomatized by Extensionality, Nullset and Addamember ("for all x and 
y there is a z having as members  y and all the members of x"), for 
instance.  SECOND-ORDER versions of any system in the neighborhood 
will be similar in strength to Second Order PA.  Hao Wang studied 
some of these systems around 1950: the relevant papers were 
incorporated into his "A Survey of Mathematical Logic" (which, to 
spread bibliographical joy, was reprinted as "Logic, Computers and 
Sets").
    INFINITY gets you denumerable sets (and REPLACEMENT then gets you 
lots more denumerable sets), so SECOND Order PA.  I believe it is a 
well-known "folklore" result that ZF without POWERSET is 
proof-theoretically equivalent to 2nd-Order PA ("Analysis")-- is, in 
other words "the same thing" if coding and decoding don't bother you. 
Steve Simpson's book on PA2 ("Systems of Second Order Arithmetic") 
will list interesting things that ARE provable in this.
    Chow's question, however, refers to "making sense of" theorems, so 
maybe proof-theoretic equivalence isn't all one could ask for.
     And Giovanni Sambin has already posted a more interesting answer.
--
Allen Hazen
Philosophy Department
University of Melbourne