[FOM] ZF[n] and (n+2)-order arithmetic

[Colin McLarty]

Several people have given good advice on the relation between higher
order arithmetic, and ZF with power set restricted.  And there is
well-published material on restricting power set in proofs of
determinacy, following Harvey.  But so far no one has known a citation
for the connection with higher order arithmetic.   It may never have
been published.  Since I want to cite it elsewhere, I venture a
proof-sketch.  The relation of orders is one off from what I suggested
in my earlier query and the most natural version will omit choice for
3rd and higher order.

The theory ZF[n] is the ZF axioms except power set, and positing that
the set N of natural numbers has n iterated power sets.

STATEMENT ZF[n] is inter-interpretable with (n+2)-order arithmetic.

Sketch:  The nonobvious direction is to interpret ZF[n] in (n+2)-order
arithmetic.  Ackermann interpreted all of ZF except infinity in PA.
He interprets any number n as the 'ZF-set' of all m such that the m-th
place in the binary expansion of n is a 1.  In other words the
remainder of n on division by 2^(m+1) is at least 2^m.

This codes the hereditarily finite sets as binary numbers, and in fact
it has a definable global choice function.

Extend this to second order arithmetic by interpeting a ZF-set as a
set (in the sense of second order arithmetic) which is either a
singleton {n} or unbounded.  Interpret any singleton {n} the way
Ackermann interprets n as a hereditarily finite ZF-set,  And interpret
{n} as a ZF-element of an unbounded set P iff n is an element of P in
the second order sense.  So the singletons correspond to hereditarily
finite sets.  The unbounded sets correspond to all ZF sets of rank
omega.   This interpetation  still has a definable global choice
function.

In third order arithmetic interpret a ZF-set as any class C of sets of
numbers such that for every set P in C, P counts as a ZF-set in the
2nd-order interpretation.  This includes a ZF-powerset for the ZF-set
of all natural numbers, but no powerset for that powerset.  This
interpretation does not provably satisfy choice for ZF sets.

The step used for third order works as well for all higher orders.

So two questions:

Is this sketch correct?

Is there an existing reference to cite in writing about this matter?

thanks, Colin