## Is it important to distinguish between meta-theory and theory?

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?

-

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$).

-

As you already mention in the body of your question, there are also philosophical reasons for doing so. See, for example, Kunen's "The Foundations of Mathematics" Chapter 3 (esp. Sec. 3.2 Keeping them Honest).

I'll try to quickly outline it here, freely using Kunen's own ideas and words (but if you find any mistake here, it'll be my fault).

As to what is the metatheory we cannot say exactly. Basically it is ordinary finitistic reasoning about finite objects, or in other words, "how we think about the world". You need finitistic reasoning even to understand finitistic reasoning (you can get nothing from nothing). So this is why one usually regards it as what is "really true".

The formalist point of view needs, in order to be philosophically justified, to develop logic twice:

Working in the metatheory, one develops formal logic, proving finitistic theorems about one's notion of formal proof to make sense of it, particularly Soundness saying that if $\Sigma$ proves $\phi$ then $\phi$ is true in all finite models of $\Sigma$.

Then, one goes on to develop ZFC, and within ZFC, one develops all of standard mathematics, including (not finitistic) model theory. To develop model theory, one must again develop formal logic. One uses at this stage the same reasoning, but now both the languages and the structures for them have arbitrary cardinalities, and the reasoning is formalized within ZFC.

But if you are a platonist and think that the ZFC axioms are obviously true, I don't think there is much need for such a distinction.

-

I will try to answer two questions:

1: "But how does set theory "know" which $n$ is meant?"

Within ZFC, we have a standard construction of the natural numbers. So for each natural number $n$ in the metatheory, and any model $M$ of ZFC, we can identify a set in $M$, say $n^M$, which plays the role of $n$ within $M$. Every model of Peano arithmetic starts with a copy of the standard natural numbers, possibly followed by some nonstandard "numbers". It's the other direction that's problematic: if $p$ is a nonstandard number in $M$, then clearly there is no standard $q$ such that $q^M = p$.

2: "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))\}$" (in ZFC).

Call that set $B$. The definition of $B$ uses the fact that $n$ is a standard number. It looks like this: $$s \in B \leftrightarrow (\exists t_0, \ldots, t_{n-1})[ t_0 = s(\dot{0}) \land t_1 = s(\dot{1}) \land \cdots \land t_{n-1} = s(\dot{n-1}) \land \phi(t_0, \ldots, t_{n-1})]$$

To make this easier to follow, I put a dot over the numbers in that formula that actually represent fixed set parameters in the formula (like $\dot{0}$). In a particular model $M$, you would replace $\dot{0}$ with $0^M$, etc.

The subscripts are not actually part of the formula; I could call those variables $a, b, c, d, \ldots$ instead. Each of the dotted parameters is found using my response to the first question. You could further expand the definition of $B$ by replacing each subformula of the form $t = s(\dot{m})$ with its own definition in ZFC.

The fact that $n$ is a standard number is what allows us to write a formula that actually has $n$ different variables.

-
how do you define $n^M$ formally? (without using meta induction) – Martin Brandenburg Sep 28 2010 at 16:25
Write $n$ with curly brackets and the symbol $\emptyset$. (Using the set theoretic convention $\\{0,\dots,n-1\\}$.) From this notation of $n$ cook up a formula $\phi_n(x)$ that says that $x$ has $n$ distinct elements, the $\in$-first being the empty set and so on. The formula $\phi_n(x)$ is constructed by meta recursion, I agree. But for each $n$ you come up with one formula $\phi_n$ that defines $n$. Now let $n^M$ be the unique $x\in M$ satisfying $\phi_n(x)$. Things get simpler once you have a successor function in your language, like in Peano Arithmetic. – Stefan Geschke Sep 28 2010 at 16:44
Assuming that I want to identify $n^M$ with the $n+1$-st von Neumann ordinal, I would use metainduction. I pick the empty set in $M$ to be $0^M$. Assuming I have defined $k^M$, I use the fact that $M$ is a model of ZFC to know there is a unique set in $M$ of the form $k^M \cup \{k^M\}$; I call this set $(k+1)^M$. Could you explain your concern with metainduction? I think it's a perfectly formal way to define the function $k\mapsto k^M$ in the metatheory – Carl Mummert Sep 28 2010 at 16:57
Thank you. It seems that metainduction is acceptable and cannot be avoided, right? Perhaps I should return to this subject when I study logical calculus more seriously. – Martin Brandenburg Sep 28 2010 at 17:21
(cont'd) I mean, take unique readability of formulas. That's a TRUE statement about formulas, right? It's not simply a formal theorem in some system, it's TRUE. And what other way to prove something about an inductively defined class (the formulas) than by (meta)induction? – Pietro KC Sep 29 2010 at 5:24