MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 6 down vote accepted

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

share|cite|improve this answer

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.

share|cite|improve this answer
how do you define $n^M$ formally? (without using meta induction) – Martin Brandenburg Sep 28 '10 at 16:25
As I said, I don't want to use meta induction because this is exactly the fusion between meta-theory and theory which Kunen seems to avoid permanently, or at least tries to(?). Besides, I don't know the rules of meta induction and why there should be something like that. I think that we have to be cautious since otherwise we can produce consistency proofs of ZF in ZF with the help of Replacement. – Martin Brandenburg Sep 28 '10 at 16:58
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 '10 at 17:21
I would venture that the necessity of metainduction goes much deeper than treating standard natural numbers internally. You use metainduction to do essentially anything nontrivial in the language, e.g. to define term, formula, proof, prove metatheorems etc. A lot of people (including myself) think, at first, that it is necessary to "rid oneself" of all mathematics when studying set theory, because that's supposed to be a foundation for mathematics. But this is not true, and elementary finitary reasoning (including induction) is indispensable if we're going to say anything at all. – Pietro KC Sep 29 '10 at 5: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 '10 at 5:24

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.

share|cite|improve this answer
One cannot reasonably get justification of ZFC from a finitistic meta-system. One can only construct the formal system of ZFC, but cannot justify any model of it, and so one cannot make the boot-strapping jump necessary to take ZFC as the new meta-system. By the way, are you a platonist? If so, what does it mean for the ZFC axioms to be obviously true? True about what? – user21820 May 29 at 15:35

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.