The n-Category Café

Most of the time when discussing propositions or giving arguments, we give those arguments in some natural language like English. For example, “If n is even, then n is divisible by 2”. However, other times we give arguments in some formal language like first-order predicate calculus. For example, “$even(n) \Rightarrow 2\vert n$”. But when we’re using a formal language, how do we know what that language means? What are the semantics of that language’s syntax?

A number of philosophers have wrangled with this question, Tarski most famously. But the end result (so far) is that, given a language L (e.g., PA or FOL), in order to talk about what sentences of L mean we must use another language M (e.g., English), which we assume we already know the meaning of. The language L that we are talking about is called the “object language”, and the language M that we are talking in (when we are talking about L) is called the “meta-language”.

PA is a formal language in which we can prove statements (e.g., about natural numbers), but of course we can also prove things in the informal ‘meta’-language of regular mathematics (e.g., about PA itself). Godel’s proof works because he is able to code statements about PA like ‘PA proves p’ or ‘PA is consistent’ in PA itself. In this sense, PA can be a meta-language for itself (but as such cannot prove its own consistency).

It is possible to prove the consistency of PA in other meta-languages (in ZFC which is strictly stronger, and in Gentzen’s system which is incomparable). But then we must know that the meta-languages are themselves consistent since otherwise they would prove both the consistency and inconsistency of PA.

(On a sidenote, I’d rather use the term theory than language.)

One should say that Gentzen’s proof works over PRA (primitive recursive arithmetic) plus quantifier-free induction up to $\epsilon_0$ (the smallest fixed point of exponentiation). This theory is incomparable in strength to PA. I think that PRA alone is weaker than PA (it doesn’t have arbitrary induction), and Wikipedia says it is considered finitist.

I understand this as being the sense: suppose we prove Con(PA). This proof itself must take place (in principle) in some theory T; since we’re using T to reason about PA, we call T the meta-theory.

Anyhow: we’ve proven Con(PA), from T. But this would be pointlessly trivial if T was inconsistent — it’s only a meaningful result if we believe T is consistent. So in terms of strengthening our confidence in PA, as a foundational system, our proof is only helpful if we believe T is more obviously secure. So we can say: “our proof of the consistency of PA presupposes the consistency of T, on the meta-level”.

Now, as I understand it, the line

proofs of the consistency of PA available all seem to presuppose the consistency of PA (on the meta-level)

is a slight overstatement, since the theory T is not always an extension of PA (Gentzen’s original proof is a case where it isn’t). At least the ones I’ve seen, though, all presuppose the consistency of something that’s no more self-evidently secure than PA — although that’s a pretty subjective criterion, of course.

Jim Dolan gave a nice interpretation of $\epsilon_0$ in this comment, as the decategorification of the free cartesian closed category on one object.

$\epsilon_0$ can also be seen as the well-ordered set of finite rooted trees. Trees are such nice combinatorial objects (I should mention $W$-types here), so it is natural to suppose this is even constructively trues.