When was Bounded Zermelo set theory first formulated? Bounded Zermelo set theory, and many variants named for MacLane in some way, are used in equiconsistency proofs for Simple Theory of Types plus infinity, and for the Elementary Theory of the Category of Sets starting in 1969 (see Finite order arithmetic and ETCS).  But did anyone formulate it before that?  
Of course Bounded Zermelo could easily have been stated before that, and the analogy with Primitive Recursive Arithmetic could have suggested it.  But was it formulated earlier in fact?
 A: The Princeton thesis of John Kemeny, written in 1949,  was devoted to the relation between Zermelo set theory and type theory.  For example, early in the thesis, there is a proof of the consistency of the simple theory of types relative to the consistency of a small fragment (nowadays known as KF) of Bounded Zermelo set theory. The comprehension scheme in KF is limited to stratifiable instances of bounded comprehension. KF was explicitly introduced and studied by Kaye and Forster in their 1991 paper in JSL entitled "End-extensions Preserving Power Set".  
For more detail, see subsection 8.0 of Mathias' Strength of Mac Lane Set Theory (APAL, 2001); indeed Mathias further discusses Kemeny's thesis in detail towards the end of section 8 of his paper.
Based on Mathias' account, it is clear that, conceptually, Kemeny "knew about" bounded Zermelo set theory, but it is not clear to me whether he explicitly formulated any fragments of Zermelo set theory.
A: I wish there was more direct evidence.  For now, it seems likely Bounded Zermelo originated as one unnamed member of a family of theories arising from equiconsistency results.  
The article
Jensen RB "On the consistency of a slight (?) modification of Quine's NF" Synthese 19 1969 pp 25--63.
introduces  "a weak version of Zermelo set theory" which has the axioms of extensionality, pair set, sum set and power set, plus bounded separation.  He gives it no usable descriptive name but and just calls it $S$.  He gives no references but says it is "folklore" that this theory (or it plus infinity, or plus infinity and choice) is equiconsistent with simple type theory (plus the same).
