In his book on set theory, Kunen often emphasizes how important it is to distinguish between statements in the theory and the meta-theory. I have two questions:
a) When we are talking about set theory, isn't this distinction superfluous? For example when we formalize logic in set theory, there exists an enumeration of all formulas and you can make recursive definitions with them. This makes some definitions easier and somehow more natural, I think. Or is it possible that we lose something with this approach, perhaps just the philosophical strength of the statements in the meta-theory? Or is it even possible that we can "prove" wrong statements?
b) As I said, Kunen seems to make a distinction between the natural numbers in the meta-theory and the natural numbers in models of set theory. Now, for example at the beginning of chapter V, there is the following lemma:
Let $\phi(x_0,…,x_{n-1})$ be any formula whose free variables are among $x_0,…,x_{n-1}$; then
$\forall A ( \{s \in A^n : \phi^A(s(0),…,s(n-1))\} \in Df(A,n))$.
Here, $Df(A,n)$ is the set of all definable subsets of $A^n$, which was defined by a recursion involving operations such as intersection, complement etc. Thus this lemma is not a definition, although it could be one when we agree with a). Anyway, my problem is the appearence of this natural number $n$. We fix a formula with $n$ free variables in our meta-theory. But how does set theory "know" which $n$ is meant? Actually I don't even know if it is possible to give a formal definition of the set $\{s \in A^n : \phi^A(s(0),…,s(n-1))\}$. I know what this means, everyone knows it, but how can we define this without an "induction on the structure of $\phi$", which I have learned in lectures, but probably also involves a fusion of theory and meta-theory?
b') Another example is an analoguous theorem for ordinal definable sets:
For each formula $\phi(y_1,…,y_n,x)$, we have
$\forall \alpha_1 … \forall \alpha_n (\forall x : \phi(\alpha_1,…,\alpha_n,x) \leftrightarrow x=a) \rightarrow a \in OD$
In the definition of OD, we need some natural number $n$ and a definable set $R \in Df(R(\beta),n+1)$, etc. … but why do we know this natural number $n$ in the proof?
Best Answer
Just to add to Carl's answer:
If $M=(M,E)$ is a model of set theory ($M$ and $E$ sets), for instance one obtained from the completeness theorem using the assumption that ZFC is consistent, then $M$ typically is a nonstandard model, with the internal natural numbers actually being "longer" than our familiar $\mathbb N$. Now, such a model will also have nonstandard formulas. While every formula in the real world has a translation in $M$, not every object that $M$ considers to be a formula corresponds to a formula in the real world.
Now logic as a mathematical theory can be developed inside $M$, with formulas and structures being objects in $M$, and a relation definable in $M$ that tells us which structures are models of which formulas.
It could happen, by the second incompleteness theorem, that $M$ is a model of $\neg\text{Con}(\text{ZFC})$. What does this mean? This means that $M$ does not know a structure that is a model of $M$'s version of ZFC. But it also means that $M$ knows a proof of the inconsistency of ZFC. Clearly, this proof cannot be translated back into the real world, in other words, it must be a nonstandard proof (nonstandard length, using nonstandard axioms or rules).
These are just some points why we have to separate "mathematics" (in this case stuff concerning objects in $M$) and "metamathematics" (stuff going on in the real world concerning $M$).