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
$\begingroup$

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

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

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

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.