Finite subsets and the Definable Power Set Operation I'm starting to read chapter VI of Kunen's "Set Theory: An I ntroduction to Independence Proofs". Lemma 1.2 says that for each formula $\phi(v_0, ..., v_{n-1}, x)$ with all free variables shown, $\forall A \forall v_0, ..., v_{n-1}\in A[\{x \in A: \phi^A(v_0, v_1, ..., v_{n-1}, x)\} \in \mathscr D(A)]$, where $\mathscr D$ denotes the definable power set operation.
On Lemma 1.3(c), Kunen proves that every finite subset of $A$ is in $\mathscr D (A)$. After that, he states that "those readers who think that (c) is a trivial consequence of Lemma 1.2 should refer to Exercises 19 and 20." Well, I had that feeling, so I went there to take a look.
Exercise (20) states: What is wrong with the following "proof" of 1.3(c)?
Let $X=\{a_0, ..., a_{n-1}\}$. Then by 1.2, $X=\{x \in A: \phi^A(a_0, ..., a_{n-1}, x)\}\in\mathscr D(A)$, where $\phi$ is $x=a_0 \vee ... \vee x=a_{n-1}$.
Well, I can't figure out why. Can someone give me some help?
 A: Lemma 1.2 (and the purported proof in exercise 20) quantify over $n$ at the metalevel -- properly speaking for each $n$ (and each $\phi$)there's a different theorem of ZF with its own proof.
1.3(c) claims the single formula $\forall X\subset A\bigl(|X|<\omega\to X\in\mathscr D(A)\bigr)$ as a theorem of ZF. In order to prove that, you cannot let your proof depend on what the actual size of $X$ is.
Intuitively, consider that a proper proof of 1.3(c) must work even for a model of ZF with non-standard integers, such that an $X$ that (within the model) satisfies $|X|<\omega$ may not be something that you recognize as finite when looking at the model from the outside.
A: To supplement Henning Makholm's answer, here is a discussion of a simplified situation in which the same issue appears.
First fix a formula $\psi(v)$ and consider analogously to Lemma 1.2 a theory $\mathsf{T}$ consisting of statements $\psi[n]$ for each meta-natural-number $n$.  By this I mean it consists of the statements $\psi[0]$, $\psi[S(0)]$, $\psi[S(S(0))],\ldots$ where $S$ denotes the successor operation and the ellipses means that for each meta-natural-number $n$ there is a statement with that many instances of the "$S$" symbol.
Next consider analogously to Lemma 1.3(c) the single statement $\theta$ which says "$\forall n \in \mathbb{N}\,\psi(n)$".
In general, we do not have $\mathsf{ZFC} + \mathsf{T} \vdash \theta$.  If we did, then by the finitary nature of proofs, $\theta$ would follow from some finite subset of $\mathsf{T}$, that is, from $\psi[0]$, $\psi[S(0)],\ldots$ $\psi[S(\cdots S(0)\cdots )]$ up to some particular meta-natural-number of applications of the successor function, and there is no reason to believe that this should be the case.
For example, if $\mathsf{ZFC}$ is consistent and $\psi(v)$ says "$v$ does not code a proof of a contradiction from $\mathsf{ZFC}$" then
in reality $\psi[0]$, $\psi[S(0)]$, $\psi[S(S(0))],\ldots$ all hold and so we have $\mathsf{ZFC} \vdash \mathsf{T}$.  On the other hand the statement $\theta$ defined as "$\forall n \in \mathbb{N}\,\psi(n)$" expresses the consistency of $\mathsf{ZFC}$ and so $\mathsf{ZFC} \not\vdash \theta$ by the second incompleteness theorem.
