 Russell would object that the set \(\mathbf{N}^{n+1}\) is being “defined” in terms of facts about all sets \(A^{n+1}\): something is a type \(n + 1\) natural number just in case it belongs to all type \(n + 1\) inductive sets. But one of the type \(n + 1\) sets in terms of which it is being “defined” is \(\mathbf{N}^{n+1}\) itself. (Independently of predicativist scruples, one does need an Axiom of Infinity to ensure that all natural numbers exist; this is frequently added to TST, as is the Axiom of Choice).