Well-founded recursion

Stream: Type theory

[Brandon Brown]

It seems like there are some constructions that have come from type theory that significantly simplify things in mathematics that are typically stated in the language of set theory. The one I've been thinking about is how well-founded relations are defined in terms of accessibility in type theory, which is a fairly simple inductive type, whereas in set theory to define the notion of a well-founded relation you have to specify that the relation is a strict total order (which comes with a list of axioms) and you have to specify it is a nonempty set and finally that there exists an element such that all other elements in the set are not less than that element. The accessibility approach seems so much simpler, and I wonder what other type theoretic constructions are simpler than their typical set theoretic counterparts.

[Kevin Buzzard]

I don't know about simplifying things but in practice (outside of set theory) well-founded recursion on anything other than nat is rather rare, and in contrast there are plenty of times in algebra where in set theory one has rings (say) $A\subseteq B\subseteq C$ and in type theory one has to juggle between subrings and algebras; the algebra_tower and bundled subrings now make this rather nice but it's still not as smooth as it is in set theory.

[Mario Carneiro]

The one I've been thinking about is how well-founded relations are defined in terms of accessibility in type theory, which is a fairly simple inductive type, whereas in set theory to define the notion of a well-founded relation you have to specify that the relation is a strict total order (which comes with a list of axioms) and you have to specify it is a nonempty set and finally that there exists an element such that all other elements in the set are not less than that element.

My view is that this apparent simplicity is mostly a consequence of the fact that inductive types are axiomatic in CIC. Defining inductive types if you don't have them built in requires transfinite induction.

Also, you don't need all that to define a well founded order. The only thing you need (which you actually omitted in your enumeration) is that every nonempty subset has a least element. From that fact you can derive transfinite induction and transfinite recursion, and all ZFC inductive types are built this way.