 Predicative mathematics does not permit unrestricted mathematical induction: In impredicative type theory, we can define 0 and the “successor” \(A^+\) of a set just as we did above in naive set theory (in a given type \(n)\) then define the set of natural numbers: