I'm reading Elliott Mendelson's "Introduction to Mathematical Logic". There is a statement with a proof that $S$ (Peano Arithmetic) is a first-order theory with equality. I am not sure whether I understand the reasoning of the proof correctly.
The proof is very short, it reiterates several simpler statements about properties of $S$ and uses a proposition which says that a theory that satisfies some particular requirements, is a first order theory with equality. As I understand, the idea is that by virtue of those properties, $S$ satisfies the hypothesis of the said proposition.
My question is that I don't see why some of the properties that are reiterated are needed to satisfy the hypothesis of the proposition.
That's the quotation of the relevant part from the book:
Corollary 3.3
S is a theory with equality
Proof
By Proposition 2.25, this reduces to parts (a)-(e), (i), (k) and (o) of proposition 3.2, and (S2')
Proposition 2.25
Let $K$ be a theory in which (A6) holds and the following are true:
a. Schema (A7) holds for all atomic wfs $\mathcal{B}(x, x)$ such that no function letters or individual constants occur in $\mathcal{B}(x, x)$ and $\mathcal{B}(x, y)$ comes from $\mathcal{B}(x, x)$ by replacing exactly one occurence of $x$ by $y$.
b. $\vdash x = y \Rightarrow f^n_j(z_1, \ldots, z_n) = f^n_j (w_1, \ldots, w_n)$, where $f^n_j$ is any function letter of $K$, $z_1, \ldots, z_n$ are variables, and $f^n_j(w_1, \ldots, w_n)$ arises from $f^n_j(z_1, \ldots, z_n)$ by replacing exactly one occurrence of $x$ by $y$.
Then $K$ is a theory with equality.
Proposition 3.2
For any terms $t, s, r,$ the following wfs are theorems of $S$:
a. $t = t$
b. $t = r \Rightarrow r = t$
c. $t = r \Rightarrow (r = s \Rightarrow t = s)$
d. $r = t \Rightarrow (s = t \Rightarrow r = s)$
e. $t = r \Rightarrow (t + s = r + s)$
i. $t = r \Rightarrow (s + t = s + r)$
k. $t = r \Rightarrow (t * s = r * s)$
o. $t = r \Rightarrow (s * t = s * r)$
(S2')
For any terms $t, s, r$ of $\mathcal{L}_A$, the following wfs are theorems of $S$:
(S2') $t = r \Rightarrow t' = r'$
Where aforementioned (A6) and (A7) are:
(A6) $(\forall x_1) x_1 = x_1$
(A7) $x = y \Rightarrow (\mathcal{B}(x, x) \Rightarrow \mathcal{B}(x, y))$
As I understand,
3.2 (a) ensures (A6) via Gen 3.2 (e)-(o) and (S2') are all possible instances of the conclusion in the implication of the 2.25b given that $S$ has only three functions: $'$, $+$, $*$.
what is left over, 2.25a should also be satisfied by $S$.
As I understand, $S$ has two atomic wff:
$\mathcal{B_1}(z1, z1): z1 = z2$
$\mathcal{B_2}(z2, z2): z1 = z2$
and they should be yielding the following instances to consider in (A7):
$\mathcal{B_1}(z1, w1): w1 = z2$
$\mathcal{B_2}(z2, w1): z1 = w1$
so conditions to hold should be:
$z1 = w1 \Rightarrow (z1 = z2 \Rightarrow w1 = z2)$
$z2 = w1 \Rightarrow (z1 = z2 \Rightarrow z1 = w1)$
All of this seems obscure, I'm not sure that I understand the last part correctly. What exactly do we need to satisfy an 2.25a) in this case? How do 3.2 (b) - (c) help?
Prop.2.25 is made of two sub-cases : (a) excludes function letters and individual constants, while (b) applies to functions.
$0$ is a constant, while $',+,\times$ are functions.
Thus, to prove case (a) we need the properties regarding atomic formulas with $=$ only, i.e. 3.2 (a)-(d).
As you correctly said, from 3.2 (a) : $t=t$, using Gen we prove axiom (A6) : $\forall x (x=x)$.
3.2 (b) is necessary to rewrite (c) as : $r=t \Rightarrow (r=s \Rightarrow t=s)$.
Now, the formula is of "form" $r=t \Rightarrow (\mathcal B(r,s) \Rightarrow \mathcal B(t,s))$, where the atomic $\mathcal B(t,s)$ (that is $(t=s)$) comes from $\mathcal B(r,s)$ (i.e. $(r=s)$) by replacing exactly one occurence of $r$ by $t$.
The same for 3.2 (d) : using (b) we get : $t=r \Rightarrow (s=t \Rightarrow s=r)$, which is of "form" : $t=r \Rightarrow (\mathcal B(t,s) \Rightarrow \mathcal B(r,s))$, where the atomic $\mathcal B(t,s)$ is $(s=t)$.
In order to prove 2.25 (b) we need 3.2 (e) and (i), that take care of $+$, according to the fact that the substitution ($t=r$) applies to the left of the function symbol (i.e. $t+s=r+s$) or to the right (i.e. $s+t=s+r$).
The same for managing $\times$, that needs 3.2 (k) and (o).
Finally, (S2') takes care of the unary functipon symbol $'$ (the successor).
Note : regarding 3.2 (d) we have :
1) $t=r$ --- assumed [a]
2) $t=r ⇒ r=t$ --- 3.2. (b)
3) $r=t$ --- from 1) and 2) by MP
4) $r=t ⇒ (s=t ⇒ r=s)$ --- 3.2 (d)
5) $(s=t ⇒ r=s)$ --- from 3) and 4) by MP
6) $s=t$ --- assumed [b]
7) $r=s$ --- from 5) and 6) by MP
8) $r=s ⇒ s=r$ --- 3.2. (b)
9) $s=r$ --- from 7) and 8) by MP
10) $s=t ⇒ s=r$ --- from 6) and 9) by DT, discharging [b]