inductively defined propositions in set theory

Stream: new members

[Patrick Thomas]

I don't think I encountered inductively defined propositions in mathematics until I started playing around with Lean and type theory. Is there an equivalent formulation in set theory to an inductively defined proposition? If so, what would it be? What would the equivalent formulation in set theory be to a proof by cases on an inductively defined proposition? What would the justification for such a proof in set theory be? Does it follow somehow from the well ordering of the natural numbers?

[Huỳnh Trần Khanh]

this thread might be of help https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/zfc.20inductive.20predicates

[Patrick Thomas]

Thank you.