I am following a proof of $\forall y(Sx + y = S(x + y))$. The base case is $Sx + 0 = S(x + 0)$, and for its proof the author says this:

"If $y = 0$, note that by PA2 ($\forall x x + 0 = x$) we have $Sx + 0 = Sx = S(x + 0)"$.

Now the first equality does indeed come as a straightforward instance of PA2, but the second equivalence – $Sx = S(x + 0)$ – does not, as far as I can see. Is the author suppressing a substitution step or something here?

  • $\begingroup$ You have $\forall x: x+0=x$ so you get the conclusion by applying $S$ to both sides of this equation. This should be validated from the axioms, but you will have to check which number in your scheme. $\endgroup$ Nov 17, 2022 at 11:39
  • $\begingroup$ In your Scheme , you may have $(x=y) \iff (S(x)=S(y))$ & $x=x+0$. I think that must be enough. $\endgroup$
    – Prem
    Nov 17, 2022 at 11:55
  • 1
    $\begingroup$ The point of the previous two comments is that, in addition to the axioms of Peano arithmetic, you also have the axioms and rules of logic, in particular the equality axioms. $\endgroup$ Nov 17, 2022 at 16:42


You must log in to answer this question.