@RobinSaunders If ultrafinitists accept induction for certain predicates, though more limited than the usual infinite class of all well-formed predicates, then that would presumably pertain to only a finite collection of those predicates. Is there some way that we can hope to get to know about such a class, or will it be kept hidden within their circles?

If my view of the axioms of ZF is that, whenever I am presented with some given structure, the axioms allow me to decide whether or not the structure is a model of ZF, and all that is needed is to verify or fail to verify them. Is it then not natural that it is hard for me to grasp the meaning of these terms? After all, it is how structures in math are first presented to students. Example: a textbook presents a composition table for $S_3$ and you are required to verify from the axioms that $S_3$ is a group. In particular, nothing seems "constructed".

Let us continue this discussion in chat.

Behold my predicative definition of $\mathbb{N}$. Call a set $B$ in ZF "super-inductive" if $0\not\in B$ and $\{0\}\in B,$ and for every $x\in B$ also $x\cup \{x\}\in B.$ Let $A$ be the inductive set provided by AI. Then $B:=A\setminus \{0\}$ is super-inductive. Define $\mathbb{N}$ as the union of $\{0\}$ with the intersection set of all subsets of $B.$

(2) But we cannot state an axiom "x is an identity if xx=x" because it only captures the notion of a projection, which is not what we mean. And if we say "x is an identity if xx=x and for all y, if yy=y, then y=x", then this is also impredicative, because x is one of the possible values for y.

(1) This is true. But at the point in time at which we formulate the axioms, we may not be aware of the theorem that $\mathbb{N}$ is also among the sets being intersected. After all, the theorem is proved from the axioms, and this is one of them. In which case the statement that the definition is impredicative is itself what? Impredicative?

quite, thanks! I still have to wrap my head around how it is that the intersection of the elements of the powerset of $A$ is not a predicative thing. After all, it might turn out to be different from all those subsets. That the intersection is itself inductive must be proven afterwards. By the way, the condition $xx=x$ in a group of linear maps seems to characterize a projection, not just the identity.

I would think that definition of $\mathbb{N}$ is not usual in set-theories like ZF, since it seems to assume a set of all inductive sets, to allow defining their intersection. It sounds similarly bad as the "set of all sets".

Another instance that I wonder about is when Nelson in his 1986 pamphlet "predicative Arithmetic" states that "the principle of induction" is impredicative. How can induction fall into the scope of having an impredicative definition, given that "induction" is not a mathematical object?

The supremum and Russell's paradox seem classical examples. I wonder about the definition of the identity element in GroupTheory. It is an element e for which ex = xe = x for all x. Since in this definition there is a quantification over all elements x, including e itself, is it not also an example of an impredicative definition? In which case, is there some reason why this example would be less important, or at least less referred to, than the others?

I notice that the Wikipedia entry has been changed to saying "Roughly speaking, a definition is said to be impredicative if..." which used to begin "More precisely, ...". It is frustrating for someone who is interested in distinguishing between ways of talking about mathematics that are predicative or not. E.g. in Nelson's "Predicative Arithmetic", Princeton 1986, the introduction "The impredicativity of induction", which precise definition of impredicativity has he got in mind, does anybody know?

@Marius Kempe: How is treating "infinity" mistakenly as if it is a real number an example of "actual infinities" and not simply a mistake? You appear to think that the "infinity" $\infty$ element of the extended real numbers is in some way related to infinite sets? In that case you are quite mistaken too. If you were to grab any textbook on real and/or complex analysis, and everywhere a $\infty$ appears, you would replace it by the $1$-element set $\{\{\{\emptyset\}\}\},$ do you think that the meaning of any of the text would change?

We absolutely cannot have a more clear conception of $\mathbb{N}$ than of $10^{100}$. After all, some single element of $\mathbb{N}$ allows for an encoding of the entire bible. It probably even exists in some editor's desktop.

To question whether one can "build a true Turing Machine" (in the "real world") does not make any real sense. A TM is an abstraction of how computation works. It is like asking whether one can "build the true number 0", or "build the true imaginary number i". Of course you can build a TM from examining the way it is defined as a tuple of sets in ZF and suggesting the appropriate sets to combine.