0
$\begingroup$

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?

$\endgroup$
3
  • $\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$
    – Mark Bennet
    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$
    – Andreas Blass
    Nov 17, 2022 at 16:42

0

Reset to default

You must log in to answer this question.