# In what sense can $ACA_{0}$ be said to be a conservative extension of PA?

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?

-
I think that you may be confused about the definition of ACAo. It is not obtained by adding a constant symbol to PA; it's obtained by adding a second sort of variables that range over sets of numbers, as Emil Jeřábek indicates in his answer. –  Carl Mummert Apr 23 '11 at 13:01
I do not think MO is the right place for the basic questions you have been asking, since these are not research level questions and can be easily solved by consulting in many standard textbooks. math.stackexchange.com is more appropriate. –  Andres Caicedo Apr 23 '11 at 14:32

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$.
I need to reconcile the following: (a) $[(\forall x)(x=0 \vee \neg(\forall y)\neg(x=y^{\prime}))]$ seems to interpret as true in the model $A$ of $\mathrm{ACA}_0$. (b) $[(\forall x)(x=0 \vee \neg(\forall y)\neg(x=y^{\prime}))]$ does not seem to interpret as true in the model $(B, D)$ of $\mathrm{ACA}_0$. (c) $[(\forall x)(x=0 \vee \neg(\forall y)\neg(x=y^{\prime}))]$ is provable in PA, but does not seem to be provable in $\mathrm{ACA}_0$. (d) $\mathrm{ACA}_0$ is a conservative extension of PA. –  Bhupinder Singh Anand Apr 27 '11 at 8:30
This formula is true in all models of $\mathrm{ACA}_0$, in fact, it's usually taken as an axiom. You seem to be thoroughly confused about the definition of $\mathrm{ACA}_0$. –  Emil Jeřábek Apr 28 '11 at 11:03
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.