Question

According to Wikipedia (on 23/04/2011):

"In mathematical logic, a logical theory $T_{2}$ is a (proof theoretic) conservative extension of a theory $T_{1}$ if the language of $T_{2}$ extends the language of $T_{1}$; every theorem of $T_{1}$ is a theorem of $T_{2}$; and any theorem of $T_{2}$ which is in the language of $T_{1}$ is already a theorem of $T_{1}$."

Conventional wisdom is that (op cit):

"$ACA_{0}$ (a subsystem of second-order arithmetic) is a conservative extension of first-order Peano arithmetic."

However we now note that:

We cannot extend the language of the first-order Peano Arithmetic PA to include a constant that interprets in the domain of any model of PA as a constant that is greater than any natural number.

Let $[G(x)]$ denote the PA-formula:

$[x=0 \vee \neg(\forall y)\neg(x=y^{\prime})]$

This translates, under every unrelativised interpretation of PA, as:

If $x$ denotes an element in the domain of an unrelativised interpretation of PA, then either $x$ is $0$, or $x$ is a 'successor'.

Further, in every such interpretation of PA, if $G(x)$ denotes the interpretation of $[G(x)]$:

(a) $G(0)$ is true;

(b) If $G(x)$ is true, then $G(x^{\prime})$ is true.

Hence, by Goedel's completeness theorem:

(c) PA proves $[G(0)]$;

(d) PA proves $[G(x) \rightarrow G(x^{\prime})]$.

Goedel's Completeness Theorem: In any first-order predicate calculus, the theorems are precisely the logically valid well-formed formulas (i. e. those that are true in every model of the calculus).

Further, by Generalisation:

(e) PA proves $[(\forall x)(G(x) \rightarrow G(x^{\prime}))]$;

Generalisation in PA: $[(\forall x)A]$ follows from $[A]$.

Hence, by Induction:

(f) $[(\forall x)G(x)]$ is provable in PA.

Induction Axiom Schema of PA: For any formula $[F(x)]$ of PA:

$[F(0) \rightarrow ((\forall x)(F(x) \rightarrow F(x^{\prime})) \rightarrow (\forall x)F(x))]$

In other words, except $0$, every element in the domain of any unrelativised interpretation of PA is a 'successor'. Further, $x$ can only be a 'successor' of a unique element in any such interpretation of PA.

PA and $ACA_{0}$ have no common model

Now, since Cantor's first limit ordinal $\omega$ is not the 'successor' of any ordinal in the sense required by the PA axioms, and since there are no infinitely descending sequences of ordinals in a model---if any---of set-theory, PA and any sub-system of ZF (such as the sub-system $ACA_{0}$ of the second order Peano Arithmetic $Z_{2}$) cannot have a common model, and so we seemingly cannot consistently extend PA to $ACA_{0}$ simply by the addition of the constant $[\omega]$ to the language of PA, and corresponding axioms.

So, in what sense can $ACA_{0}$ be said to be a conservative extension of PA?

Answer 1

I don’t follow your reasoning about constants at all. The language $L_{\mathrm{PA}}$ of PA is a one-sorted first-order language with signature $\{0,1,+,\cdot,\le\}$ (or similar), the language of $\mathrm{ACA}_0$ is a two-sorted first-order language whose first sort is endowed with the same function and relation symbols as $L_{\mathrm{PA}}$, and there is an additional predicate $x\in X$ taking an element $x$ of the first sort and an element $X$ of the second sort. Stated in this way, the language of $\mathrm{ACA}_0$ extends the language of PA, and the sentences of $L_{\mathrm{PA}}$ provable in $\mathrm{ACA}_0$ are exactly those which are provable in PA, hence $\mathrm{ACA}_0$ is indeed a conservative extension of PA. The model-theoretic correspondence is that on the one hand, if $A$ is a model of $\mathrm{ACA}_0$, then its first sort is a model of PA, and on the other hand, if $B$ is a model of PA, then $(B,D)$ is a model of $\mathrm{ACA}_0$, where $D$ is the collection of all definable (with parameters) subsets of $B$.

Answer 2

The argument in the question shows only that the ordering of the natural numbers in a model of PA cannot also be the ordering of the ordinals in a model of ZF. But that seems to have nothing to do with $\text{ACA}_0$ and its conservativity over PA.