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

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.

• I think it would be nice to be able to tag Peter Smith, user:35151, but it doesn't seem like that's a feature.
– Joe
Apr 6, 2022 at 18:55
• @WillG No, you can't actually tag users who aren't already present in the thread. Apr 6, 2022 at 19:07

$$\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).

• Comments are not for extended discussion; this conversation has been moved to chat.
– Pedro
Apr 10, 2022 at 14:59
• I'm confused about the parenthetical in the bullet: Doesn't $\mathrm{PA}$ prove "Any directed union of consistent theories is consistent"?
– cody
Apr 25, 2022 at 19:00
• @cody Yes, so? (The issue is that, while $\mathsf{PA}$ proves that $\mathsf{PA}$ proves that each finite subtheory of $\mathsf{PA}$ is consistent, $\mathsf{PA}$ doesn't prove that each finite subtheory of $\mathsf{PA}$ is consistent.) Apr 25, 2022 at 19:13
• Aha! Thanks. It's a bit mind bending to remember which belief is held at which level.
– cody
Apr 25, 2022 at 19:17