Can Peano arithmetic prove the consistency of "baby arithmetic"?

Question

I am reading Peter Smith's An Introduction to Gödel's Theorems. In chapter 10, he defines "baby arithmetic" $\mathsf{BA}$ to be the zeroth-order version of Peano arithmetic ($\mathsf{PA}$) without induction. That is, $\mathsf{BA}$ is the zeroth-order theory (meaning there are no quantifiers or variables) with primitive constant symbol $\mathsf0$, unary function $\mathsf S$, binary functions $+$ and $\times$, and the following axiom schemas:

1. $\mathsf{Sn\neq0}$
2. $\mathsf{(Sn=Sm)\to(n=m)}$
3. $\mathsf{m+0=m}$
4. $\mathsf{m+Sn=S(m+n)}$
5. $\mathsf{m\times0=0}$
6. $\mathsf{m\times Sn=(m\times n)+m}$

The symbols $\mathsf{n}$ and $\mathsf{m}$ appearing in the schemas are placeholders for any term of the theory, where terms are defined via the standard recursive definition for predicate logic.

My question is, does $\mathsf{PA}\vdash\mathsf{Con(BA)}$? Note that this is a very concrete question about whether the arithmetical formula $\mathsf{Con(BA)}$ is formally derivable in $\mathsf{PA}$, not to be confused with more philosophical questions about whether $\mathsf{PA}$ itself is consistent, discussed elsewhere.

Gödel's second incompleteness theorem shows that $\mathsf{PA}$ cannot prove $\mathsf{Con(PA)}$. Meanwhile we cannot even ask whether $\mathsf{BA}$ can prove $\mathsf{Con(BA)}$ because $\mathsf{Con(BA)}$ involves quantifiers and is therefore not even in the language of $\mathsf{BA}$. But it seems plausible that $\mathsf{PA}$ could prove $\mathsf{Con(BA)}$, which would be a nice, reassuring result at the very least.

---

As a footnote, I'll say that part of my motivation for this question is indeed wondering about whether $\mathsf{PA}$ is consistent. A common argument goes something like: "If you believe $\mathsf{PA}$ formalizes valid reasoning about arithmetic, then you believe what it proves. Hence it cannot prove $\mathsf{0=1}$, because $0$ is not really equal to $1$. Hence you believe $\mathsf{PA}$ is consistent." But I think this argument would be more secure if it didn't rest on definite facts about "true arithmetic," and in particular the assumption that "$0$ is not actually equal to $1$," but instead referred only to $\mathsf{BA}$. Thus, in this light, it is important to know whether $\mathsf{BA}$ proves $\mathsf{0=1}$, i.e., whether $\mathsf{BA}$ is consistent.

I'm not putting this here to start a huge philosophical discussion/argument, just to provide motivation.

Answer 1

$\mathsf{PA}$ has a very interesting property, namely that it proves the consistency of each of its finitely axiomatizable subtheories. This is usually called the reflection principle for $\mathsf{PA}$ (and incidentally the same result holds for $\mathsf{ZFC}$). The theory $\mathsf{BA}$ is the quantifier-free part of a finitely axiomatizable theory (just throw on "$\forall x$"s everywhere) $\mathsf{BA}'$; consequently, we do in fact have $\mathsf{PA}\vdash \mathsf{Con(BA)}$.

• We have to be careful here: $\mathsf{PA}$ does not prove "Every finite subtheory of $\mathsf{PA}$ is consistent." Rather, for each finite subtheory $T$ of $\mathsf{PA}$, $\mathsf{PA}$ proves "$T$ is consistent." So we don't get a $\mathsf{PA}$-proof of $\mathsf{Con(PA)}$ itself from the reflection principle. ($\mathsf{PA}$ also proves "$\mathsf{PA}$ proves the consistency of each finite subtheory of $\mathsf{PA}$," but again this falls short of actually being a problem.)

Admittedly, this is massive overkill, but the reflection principle is a very cute trick that's worth knowing. With more care we can prove the consistency of $\mathsf{BA}$ in the very weak fragment $\mathsf{I\Sigma_1}$, or indeed much less (although when we go below $\mathsf{I\Sigma_1}$ things often get finicky so I usually don't).