Shipman's schema for ZF(C)
freund at mathematik.tu-darmstadt.de
Tue Aug 31 03:15:49 EDT 2021
Just to begin with the obvious: \in-induction for arbitrary formulas
follows from foundation in the presence of full separation.
Results about \in-induction in the absence of full separation are known,
e.g., in the context of Kripke-Platek set theory:
Gerhard Jäger, A Version of Kripke-Platek Set Theory which is Conservative
over Peano Arithmetic, Mathematical Logic Quarterly 30 (1984) 3-9,
Michael Rathjen, Fragments of Kripke-Platek set theory with infinity,
in: Peter Aczel, Harold Simmons and Stanley Wainer (eds.), Proof Theory: A
selection of papers from the Leeds Proof Theory Programme 1990,
An over-simplified summary is: With very little induction, set theories
can really become quite weak. Adding full induction yields theories of
medium strength -- which are, however, nowhere near as strong as ZF.
More information about the FOM