Shipman's schema for ZF(C)

[Anton Freund]

> What is obvious is that foundation follows from \in-induction, even if the
> latter
> is limited to bounded formulas. As for the converse - the proof I know of
> it uses
> the existence of the transitive closure of sets, and at least the standard
> proof
> of that existence uses the axioms of infinity, replacement and union. Are
> you sure
> that full separation suffices?

You are right that my side remark about separation was not formulated in a
fully precise way. The argument that it alludes to does indeed use
transitive closure. However, the latter is available in rather weak set
theories, far below Kripke-Platek (no sets of high rank arise). In
contrast, replacement (even for formulas of relatively low complexity)
will typically increase the proof-theoretic strength dramatically. So I
still think that my remark conveys the right idea / holds over typical
base theories. But you are right that there is a small caveat that may
apply in some settings.

Best,
Anton