Using only the axioms of $\mathsf{PA}$, I want to prove this fact. It came up in a previous year's exam paper, and seems more difficult than I had anticipated... The question was to sketch the idea, but I thought it was a good exercise to try and show every gory detail of the proof.
My question is whether this proof is correct (in particular the details such as the overlines, and use of only the axioms)? Moreover, if anyone knows of a shorter proof, I would be interested to see it.
Proof
First I have stated this in the language of arithmetic: $$\forall n(( \exists q(\overline{3}\times q=\overline{n})\vee \exists q(\overline{3}\times q+\overline{1}=\overline{n}))\vee \exists q(\overline{3}\times q+\overline{2}=\overline{n})).$$
My aim is to use induction:
If $\varphi$ is a unary predicate such that:
- $\varphi(0)$ is true, and
- for every natural number $n$, if $\varphi(n)$ is true, then $\varphi(S(n))$ is true,
then $\varphi(n)$ is true for every natural number $n$.
My choice of $\varphi$ is $$\varphi(n)=(\psi(n)\wedge\psi(S(n)))\wedge\psi(S(S(n))),$$ where $$\psi(n)=( \exists q(\overline{3}\times q=\overline{n})\vee \exists q(\overline{3}\times q+\overline{1}=\overline{n}))\vee \exists q(\overline{3}\times q+\overline{2}=\overline{n}).$$
The base case, $\varphi(0)$ is okay, since the choice of $0$ for $q$ will work in all three $\psi(0)$, $\psi(S(0))$ and $\psi(S(S(0)))$. Now suppose $\varphi(n)$ is true, and look at $\varphi(S(n))$. $\psi(S(n))$ and $\psi(S(S(n)))$ follow from $\varphi(n)$, so it remains only to show that $\psi(S(S(S(n))))$ holds.
Suppose that $\exists q(\overline{3}\times q+\overline{2}=\overline{n})$, then by Tarski's definition of truth in a model(?), there is a natural number $m$ (say) with $\overline{3}\times \overline{m}+\overline{2}=\overline{n}$, and now reasoning in $\mathsf{PA}$ (numbering of axioms are as listed here), \begin{align} \overline{3}\times \overline{m}+\overline{2}&=\overline{n}\\ S(S(S(\overline{n})))&=S(S(S(\overline{3}\times \overline{m}+\overline{2}))) &&\text{axiom 2(?), three times}\\ &=\overline{3}\times \overline{m}+S(S(S(\overline{2})))&&\text{axiom 4, three times}\\ &=\overline{3}\times \overline{m}+S(S(S(\overline{2}+0)))&&\text{axiom 3}\\ &=\overline{3}\times \overline{m}+(\overline{2}+S(S(S(0))))&&\text{axiom 4, three times}\\ &=\overline{3}\times \overline{m}+(\overline{2}+\overline{3})&&\text{definition of }\overline{a}\\ &=(\overline{3}\times \overline{m}+\overline{3})+\overline{2}&&\text{properties of addition }(\ast)\\ &=(\overline{3}\times \overline{m+1})+\overline{2}&&\text{axiom 6}. \end{align} Then again by Tarksi's definition of truth in a model(?), $\exists q(\overline{3}\times q+\overline{2}=S(S(S(\overline{n}))))$, and hence $\psi(S(S(S(n))))$ holds.
Similarly, from $\exists q(\overline{3}\times q+\overline{1}=\overline{n})$, we can show $\exists q(\overline{3}\times q+\overline{1}=S(S(S(\overline{n}))))$, and hence $\psi(S(S(S(n))))$ holds.
If $\exists q(\overline{3}\times q=\overline{n})$, then by Tarski's definition of truth in a model(?), there is an $m$ such that $\overline{3}\times \overline{m}=\overline{n}$, and then reasoning in $\mathsf{PA}$: \begin{align} \overline{3}\times \overline{m}&=\overline{n}\\ S(S(S(\overline{n})))&=S(S(S(\overline{3}\times \overline{m}))) &&\text{axiom 2(?), three times}\\ &=S(S(S(\overline{3}\times \overline{m}+0))) &&\text{axiom 3}\\ &=\overline{3}\times \overline{m}+S(S(S(\overline{0})))&&\text{axiom 4, three times}\\ &=\overline{3}\times \overline{m}+\overline{3}&&\text{definition of }\overline{a}\\ &=\overline{3}\times \overline{m+1}&&\text{axiom 6}. \end{align} By Tarski's definition of truth in a model(?) $\exists q(\overline{3}\times q=S(S(S(\overline{n}))))$, and again $\psi(S(S(S(n))))$ holds.
By two applications of the $\vee$-elimination rule of first order logic, from the assumption of $\varphi(n)$, we can deduce $\psi(S(S(S(n))))$, and as mentioned previously this is sufficient to show $\varphi(S(n))$.
Since for all $n$, $\varphi(n)$, in particular $\psi(n)$, which was exactly what was asked ($\forall$-introduction rule).
$(\ast)$ for this step I used that addition is associative and commutative, which holds in $\mathsf{PA}$ (Wikipedia has a proof).