# Logic in the metatheory

In Goldstern and Judah's The Incompleteness Phenomenon we are asked to prove that any model of the first two Peano Axioms: $$\forall x [Sx\neq0]$$ $$\forall x\forall y[Sx=Sy\implies x=y]$$ must be infinite. S is a unary function intended as successor. If the model is finite there must be $m$ and $n$ with $S^m0=S^n0$ where the superscript represents iteration. Then $|n-m|$ applications of the second axiom lead to a contradiction with the first.

We are clearly arguing in the metatheory, as our axioms have no ideas of infinite sets. Is there a clear definition of what axioms and logic are allowed here? Can you suggest a book on the subject?

-
Model theory is part of set theory, so use your favourite set axioms, eg. ZF or ZFC. –  Robin Chapman Dec 8 '10 at 14:16
I don't think many pure model theorists would agree that what they do is set theory. –  Carl Mummert Dec 8 '10 at 15:01

There are two ways to handle this.

The most common way is simply to assume some form of set theory in the metatheory, e.g. ZFC. Then you can use all the normal semantic and model-theoretic methods that you are used to. The advantages of this method are that it matches the way that mathematicians actually think about things, and that it allows us to use all the theorems we're used to.

Another option is to reinterpret claims made in the metatheory as syntactic claims. For example, the claim "the model must be infinite" can be reinterpreted to mean that the theory itself (!) proves each of the sentences $$\lnot (\exists c_0) (\forall x) (x = c_0)$$ $$\lnot (\exists c_0, c_1) (\forall x) (x = c_0 \lor x = c_1)$$ $$\lnot (\exists c_0, c_1, c_2) (\forall x) (x = c_0 \lor x = c_1 \lor c = c_2)$$ and more generally, for each $k > 0$, $$\lnot (\exists c_0, \ldots, c_k ) (\forall x) (x = c_0 \lor \cdots \lor c = c_k)$$

The fact that each of these sentences is provable in the theory can be verified using a very weak metatheory. There's a simple and uniform way, for any fixed $k$, to generate a proof from your two axioms for that particular $k$.

This reinterpretation process is well known to logicians, and it can be applied very generally. The main limitation is whether the property in question can be stated in the language of the theory itself (possibly as an infinite set of sentences, as with the example above).

Gödel's completeness theorem says that if a sentence in the language of a theory is true (semantically) in every model of the theory, then that sentence is provable (syntactically) within the theory itself. So we could, if we wanted, ignore the "true" part in those cases and focus just on the "provable" part. The cost of doing that is that it arguably misses the point, since we usually think semantically about models, and that it does not apply to properties of models that cannot be expressed within the language of the theory itself.

Because this reinterpretation process is usually very routine, it's rare for logicians to bother to mention it, even though we're well aware it could be done. We just write in the normal model-theoretic (set theoretic) way unless there is a particular reason that we need to focus on the syntactic interpretation.

-
Thanks. I can see how to prove each of the statements you cite in the base theory. However, the metatheory doesn't seem to come with a set of axioms (unless, as Robin Chapman suggested, you just say it is ZFC), so it is hard to know what you have to work with in a proof. –  Ross Millikan Dec 13 '10 at 14:21

You are doing it indirectly, the direct way to do this is by defining a one to one function from $N$ to the members of the model.

So let $M$ be a model of the first two axioms. (To able to to talk about the model you need a theory that can talk about sets to some extent or a theory that can interpret that amount of set theory.)

The next thing is defining the function inductively in the obvious way and then use induction and the fact that $M$ satisfies the first and second axiom to prove that the function is one to one.

-