2
$\begingroup$

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

$\endgroup$

2 Answers 2

Reset to default
2
$\begingroup$

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

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

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

$\endgroup$

You must log in to answer this question.

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