Note this quote from the article. "One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “l

Note this quote from the article. "One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the paradox." This is similar to constraints of making something semi-decidable or recursively enumerable. Provable, recursively enumerable, semidecidable, and turing recognizable are all the same thing described in different ways. Some things are easier to find in type theory, other in set theory and for some Turing machines work better. The Church–Turing thesis isn't provable but is the safe assumption. IMHO termination analysis, which will never be complete, has more interesting and has some implications for ATP that aren't as easily captured in type theory. As an example related to term rewriting which will be important to ML. https://arxiv.org/abs/2307.14805 https://arxiv.org/abs/2307.14805