Explicit Substitution in Peano Arithmetic proofs.

Question

I am creating a proof of $S0 \times SS0 = SS0$ in Peano Arithmetic, and a big part of my proof is finding equivalences and then substituting in to relevant formulae. Now I know I can do that with the following axiom schema from our axiomatic system:

$\forall u \forall v (u = v \rightarrow (\phi[u/v] \rightarrow \phi)$

But this substitution process is much more finicky if you want to lay it out explicitly (and then using modus ponens to get your desired formula), and I've ran into a wall, with two frustrating problems. I will lay out my proof so far and show you where the problems are:

1. $S0 \times SSO = S0 \times S0 + S0 \hspace{8cm}$ PA6 and $\forall E$
2. $S0 \times S0 = S0 \times 0 + S0\hspace{8.6cm}$ PA6 and $\forall E$
3. $S0 \times 0 = S0\hspace{10.6cm}$ PA5 and $\forall$E
4. $\forall x \forall y(x = y \rightarrow S0 \times S0 = x + S0 \rightarrow S0 \times S0 = y + S0\hspace{2.6cm}$ A8
5. $S0 \times 0 = S0 \rightarrow (S0 \times S0 = S0 \times 0 + S0 \rightarrow S0 \times S0 = 0 + S0)\hspace{1cm}$ $\forall E$ $\forall E$, 4
6. $S0 \times S0 = S0 \times 0 + S0 \rightarrow S0 \times S0 = 0 + S0 \hspace{4.5cm}$ MP, 5
7. $S0 \times S0 = 0 + S0 \hspace{9.5cm}$ MP 6
8. $\forall x 0 + x = x\hspace{10.5cm}$ Proved by me
9. $0 + S0 = S0\hspace{10.4cm}$ $\forall E$
10. $S0 \times S0 = S0\hspace{10cm}$ Transitivity

PROBLEM 1

Now, at this point I want to return to the original formula – $S0 \times SS0 = S0 \times S0 + S0$ – and substitute in $S0$ for $S0 \times S0$. In particular, what I seem to want is (after instantiating the axiom schema and removing the universal quantifiers):

$$S0 \times S0 = S0 \rightarrow S0 \times SS0 = S0 \times S0 + S0 \rightarrow S0 \times SS0 = S0 + S0$$

and then I make my way to my desired formula using modus ponens. The problem, though, is that if $y = S0$, then substituting for $y$ doesn't give the original formula (which I would then be able to use in modus ponens). Rather, you first get:

$$ \forall x \forall y(x = y \rightarrow x \times SS0 = x + x \rightarrow y \times SS0 = y + y)$$

And when you substitute in you apparently get:

$$ S0 \times S0 = S0 \rightarrow S0 \times S0 \times SS0 = S0 \times S0 + S0 \times S0 \rightarrow S0 \times SS0 = S0 + S0$$

So, rather than a straightforward substitution, I've now got a much more expansive formula which I have not derived. What's to be done?

PROBLEM 2

The second problem comes after. Suppose, as I hope we should be able to suppose, that I get past the first problem. Well then I should have:

$$S0 \times SS0 = S0 + S0$$,

which is good. Now to get to my final goal, I need to say that $S0 + S0 = SS0$. Again, seems like it should be simple! But if I apply the appropriate axiom – PA6 (see below for axioms) – I get:

$$S0 + S0 = S(S0 + 0)$$

Now I know that $S0 + 0 = 0$, so when I substitute, I get $$S0 + S0 = S(S0)$$, which is pretty much what I want but for those pesky brackets! Except I'm not sure the legal way to get rid of those brackets.

These then are my frustrating problems. I'll now give the axioms that I'm using:

PA1. $\forall x \hspace{0.05cm}0 \ne Sx$

PA2. $\forall x \forall y \hspace{0.05cm} (Sx = Sy \rightarrow x = y)$

PA3. $\forall x \hspace{0.05cm} x + 0 = x$

PA4. $\forall x \forall y \hspace{0.05cm} x + Sy = S(x + y)$

PA5. $\forall x \hspace{0.05cm} x \times 0 = 0$

PA6. $ \forall x \forall y \hspace{0.05cm} x \times Sy = x \times y + x$

I also have symmetry of identity and transitivity of identity, which I've proven. I've made use of transitivity of identity only, but there they are:

$\vdash \forall x \forall y \hspace{0.05cm} (x = y \rightarrow y = x)$

$\vdash \forall x \forall y \forall z \hspace{0.05cm} (x = y \wedge y = z \rightarrow x = z)$

I've also got all the standard axioms of an axiomatic proof system for first-order logic. Pardon the annotations on my derivation not lining up. If anyone has a better way of doing that please let me know in the comments too. It is driving me mad having to align manually.

Answer 1

We have the identity: $S0 \times S0 = S0$, and we want to use it into:

$S0 \times SS0 = S0 \times S0 + S0$.

We have to use the following instance of Substitution axiom:

$S0 \times S0 = S0 \to ((S0 \times SS0 = z + S0)[(S0 \times S0)/z] \to (S0 \times SS0 = z + S0)[S0/z].$

After two applications of Modus Ponens what we get is:

$S0 \times SS0 = S0 + S0.$

The second case is similar; we have $S0+0=S0$ and we want to use it with: $S0+S0=S(S0+0)$.

The formula to be used in Substitution is: $S0+S0=S(z)$.

---

The correct form of Substitution is:

$u=v → (\varphi[u/z] → \varphi[v/z])$.

The substitution operation is defined in terms of substituting a term in place of a variable into a formula.

This means that the operation amounts to e.g. $\varphi(z)[S0/z]$.

When you write $u=v→(ϕ[u/v]→ϕ)$, if $u,v$ are both variables it is ok, but in your case you have $S0 \times S0=S0$ and the two are more general terms.