Zulip Chat Archive

Stream: new members

Topic: inductively defined propositions in set theory

Patrick Thomas (Nov 06 2021 at 16:21):

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 (Nov 07 2021 at 02:51):

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

Patrick Thomas (Nov 07 2021 at 19:15):

Thank you.

Last updated: Dec 20 2023 at 11:08 UTC