# Am I allowed to substitute terms when reasoning in Peano Arithmetic?

I feel a little silly asking this question, but here goes. I'm on Chapter 1 of "Forcing for Mathematicians" by Nik Weaver and doing some of the exercises.

When doing stuff in Peano Arithmetic, can I substitute in terms? For example, axioms 3 and 4 of the "non-logical axioms" (as enumerated in the book) are:

(3) $$x+0=x$$ and

(4) $$x+y^\prime=(x+y)^\prime$$

(where $$x^\prime$$ is the successor to $$x$$).

From these two axioms, am I allowed to call the following theorems?

$$(x+0)+y^\prime=((x+0)+y)^\prime$$

$$(x+0)+y^\prime=(x+y)^\prime$$

$$x+y'=((x+0)+y)$$'

It feels right that I should be able to, but I don't see any axiom that allows this (and their are other axioms that seem to handle these kinds of "obvious" things such a one related to the renaming of variables).

• +1 - and clarifying for the OP, the axioms of PA are added on top of the more fundamental rules for first-order logic in general. E.g. "From $a$ and $a\rightarrow b$, we can deduce $b$" is built into the underlying logical framework (so doesn't need to be mentioned in the development of PA specifically). See e.g. here for more information on how this "under-the-hood" system can be presented (there are many approaches which are ultimately equivalent but have various advantages and disadvantages - like programming languages). – Noah Schweber Nov 22 '19 at 17:49
• That makes sense. But isn't that true of the rule of inference? "from $\phi$ and $\phi \rightarrow \psi$ infer $\psi$"? This seems to be a straight up rule of propositional logic but it is specified on page 4 of the book which is why I wasn't confident I could use normal rules of first-order logic. (If it is relevant, the other two rules of inference specified are "from $\phi$ infer $(\forall{x})\phi$" and "from $\phi$ infer $\bar{\phi}$ where $\bar{\phi}$ is $\phi$ with the variables renamed.") – roundsquare Nov 22 '19 at 20:54