[FOM] "Noetherian induction" and 2nd order Zermelo set theory

[Roger Bishop Jones]

A long time ago I got the idea that "Noetherian induction"
was the name for the following induction principle over
well-founded sets:
  forall P.  (forall x. ((forall y in x. P(y)) => P(x))) => (forall z. P(z))
Since then I have never seen anyone use the term
"Noetherian induction" and have been unable to discover my source.

Is "Neotherian induction" the correct name for the above principle?

It appears that the usual formulation of the axiom of foundation
in Zermelo set theory is not only insufficent to guarantee
well founded models in first order logic, but even in second order logic.

Gabriel Uzquiano in an article in Volume 5 of the Bulletin of
Symbolic logic shows that adding an axiom which assets that
every set is a subset of V(alpha) for some alpha ensures
well-foundedness of models.

"Noetherian induction" seems to me a more natural
way to assert well-foundedness in a second order
logic, can anyone confirm for me that an axiom asserting
the principle of Noetherian induction suffices to eliminate
non-well-founded models in second order Zermelo set theory?
(seems obvious to me, but that can't be relied upon!)

Roger Jones