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?




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).


2 Answers 2


Yes, substitution is allowed as an axion of first-order logic, nothing wrong here.

  • 1
    $\begingroup$ +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). $\endgroup$ Nov 22, 2019 at 17:49
  • $\begingroup$ 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.") $\endgroup$ Nov 22, 2019 at 20:54
  • $\begingroup$ @roundsquare it may be possible that the author had taken it for granted! $\endgroup$
    – T.D
    Nov 22, 2019 at 20:56
  • $\begingroup$ @T.D. yeah, I guess for me modus ponens is just as obvious :( $\endgroup$ Nov 22, 2019 at 22:18

Yes. If you want axioms to cite, see the equality-defining axioms (2-5 here).


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .