example proof using predicate calculus with equality

Question

I am trying to understand example 4 of section 21 of First Order Mathematical Logic by Angelo Margaris:

1. 0 + 0 = 0 + 0 (=)
2. 0 + y = y + 0
3. y' + 0 = y + 0'
4. y + 0' = (y + 0)'
5. y + 0' = (0 + y)'
6. 0 + y' = (0 + y)'
7. 0 + y' = y' + 0 (=, 6, 5, 3)

The only things introduced so far in this section have been the equality axioms and the following two theorems:

T1. $\forall x \forall y (x = y \to y = x)$

T2. $\forall x \forall y \forall z (x = y \land y = z \to x = z)$

It does not seem to me that steps 2-6 can be arrived at from these alone. Are they all assumptions? If they are all assumptions then why are steps 1, 2 and 4 stated?

What does the prime notation denote? Why is step 7 different from step 2?

Answer 1

Margaris is a great book, but does require some patience getting to know his particular nomenclature. In addition, as Example 4 of Section 21 illustrates, he is sometimes not as clear as he could have been.

The purpose of this example is solely to show how three of the results introduced in the preceding two pages are used in an exemplary proof. These results are:

• Equality Axiom (E1): $\forall x(x=x)$;
• Theorem 1: $\vdash\forall x\forall y(x=y\rightarrow y=x)$;
• Theorem 2: $\vdash\forall x\forall y\forall z(x=y\wedge y=z\rightarrow x=z)$

(E1) is used in step (1) of the proof. Theorems 1 and 2 are used in step (7). These applications are properly explained in the paragraph following the example on page 106. Why no reasons are given for steps (2)-(6) is because the results required have yet to be introduced in the book. Indeed, Example 4 is exactly those first 8 (of 17) steps given as the proof for Theorem 4 of Section 24 (pages 129-130). Section 24 defines the first-order theory of natural numbers.

The set of proper symbols of $N$ is $\{\ =\ ,\ '\ ,\ +\ ,\ \cdot \,\ 0\ \}$, where $'$ is the first 1-place operation symbol, $+$ and $\cdot$ are the first two 2-place operation symbols, and $0$ is the first constant symbol. $r'$ is called the successor of $r$.

When you get to Section 24 and Theorem 4 therein, you will find that the justifications for steps (2)-(6) are based on the specific axioms of the natural numbers, an initial theorem of the number system, as well as some substitution theorems that actually immediately follow Example 4 in the book.

I wish this answer could be more interesting to those who do not have the Margaris text, but unfortunately the answer is a consequence of the book's pedantics and not really of a mathematical nature. But for partial completeness, see below for Theorem 4 and first 8 (of 17) steps of its proof covering the base induction step (from which the example above is taken).

Theorem 4 (Section 24/Margaris/First Order Number Theory): $\vdash \forall x\forall y(x+y=y+x)$

Proof: Induction on $x$. $P(x)$ is $x+y=y+x$. First we prove $0+y=y+0$ by induction on $y$.

1. $0+0=0+0\qquad$ Equality Axiom $\forall x(x=x)$

   2. $0+y=y+0\qquad\quad$ induction hypothesis
   3. $y'+0=y+0'\qquad\ \ \ $ Number Theorem $\forall x\forall y(x'+y=x+y')$.
   4. $y+0'=(y+0)'\qquad$ Number Axiom $\forall x\forall y(x+y'=(x+y)')$.
   5. $y+0'=(0+y)'\qquad$ substitution of (2) and (4).
   6. $0+y'=(0+y)'\qquad$ Number Axiom $\forall x\forall y(x+y'=(x+y)')$.
   7. $0+y'=y'+0\qquad\ \ \ $ Theorems 1/2 from above.

$8$. $\forall y(0+y=y+0\rightarrow0+y'=y'+0)\qquad$ deduction from (2) to (7) and generalization