I have been having trouble proving the formulas given in the exercises in the section on equality in First Order Mathematical Logic by Angelo Margaris.
The axioms of equality are given as:
E1. $\forall x (x = x)$
E2. $\forall x_{1} \cdots \forall x_{n} \forall y_{1} \cdots \forall y_{n} ((x_{1} = y_{1} \land \cdots \land x_{n} = y_{n}) \to (G(x_{1}, \ldots, x_{n}) \iff G(y_{1}, \ldots, y_{n})))$ (one axiom for each predicate symbol $G$)
E3. $\forall x_{1} \cdots \forall x_{n} \forall y_{1} \cdots \forall y_{n} ((x_{1} = y_{1} \land \cdots \land x_{n} = y_{n}) \to (F(x_{1}, \ldots, x_{n}) = F(y_{1}, \ldots, y_{n})))$ (one axiom for each operation symbol $F$)
The first exercise is to prove that if $P(u)$ is similar to $P(v)$, then $\vdash \forall u (P(u) \iff \exists v (v = u \land P(v)))$.
$P(u)$ is similar to $P(v)$ if and only if $v$ is not free in $P(u)$ and $u$ is not free in $P(v)$, and $P(u)$ admits $v$ for $u$ and $P(v)$ admits $u$ for $v$, and $P(v/u)$ is $P(v)$ and $P(u/v)$ is $P(u)$.
Is there a general strategy that may help or any other hints that someone could point me to?
I have been first trying to prove $\vdash P(u) \iff \exists v (v = u \land P(v))$. Is this possible?
EDIT
From Mauro's hint I so far have:
\begin{array}{l l l} 1. & \forall x (x = x) & \text{E1} \\ 2. & u = u & \text{T17.1, $\Delta$ is $\varnothing$, $v$ is $x$, $P$ is $x = x$, $t$ is $u$} \\ 3. & \quad P(u) & \text{as} \\ 4. & \quad u = u \land P(u) & \text{SC, 2, 3} \\ 5. & \quad \exists v (v = u \land P(v)) & \text{T17.4, $\Delta$ is $\{P(u)\}$, $v$ is $v$, $P$ is $v = u \land P(v)$, $t$ is $u$} \\ 6. & P(u) \to \exists v (v = u \land P(v)) & \text{DT, 1-5} \\ \end{array}
EDIT
If $v = u \to (P(v) \iff P(u))$ holds when $P(u)$ is similar to $P(v)$ (does it?) then perhaps:
\begin{array}{l l l} 1. & v = u \to (P(v) \iff P(u)) & ? \\ 2. & \quad \exists v (v = u \land P(v)) & \text{as} \\ 3. & \quad \quad v = u \land P(v) & \text{C$v$} \\ 4. & \quad \quad v = u & \text{SC, 3} \\ 5. & \quad \quad P(v) & \text{SC, 3} \\ 6. & \quad \quad P(v) \iff P(u) & \text{MP, 1, 4} \\ 7. & \quad \quad P(v) \to P(u) & \text{SC, 6} \\ 8. & \quad \quad P(u) & \text{MP, 7, 5} \\ 9. & \quad P(u) & \text{C, 3} \\ 10. & \exists v (v = u \land P(v)) \to P(u) & \text{DT, 1-9} \\ \end{array}
Steps 3-9 use T17.12 letting $\Delta$ be $\{\exists v (v = u \land P(v))\}$, $v$ be $v$, $P$ be $v = u \land P(v)$, and $Q$ be $P(u)$. $v$ is not free in $\Delta$. $v$ is not free in $Q$ by the definition of similar. Is this correct?
EDIT
I found the following alternative to E2 at Wikipedia:
For any variables $x$ and $y$ and any formula $\varphi(x)$, if $\varphi'$ is obtained by replacing any number of free occurrences of $x$ in $\varphi$ with $y$, such that these remain free occurrences of $y$, then $x = y \to (\varphi \to \varphi')$.
See E3 at https://en.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms
If I use this instead of step 1 in my previous edit then perhaps:
\begin{array}{l l l} 1. & v = u \to (P(v) \to P(u)) & \text{alt E2, $P(u)$ and $P(v)$ are similar, hence $P(u)$ is $P(u/v)$} \\ 2. & \quad \exists v (v = u \land P(v)) & \text{as} \\ 3. & \quad \quad v = u \land P(v) & \text{C$v$} \\ 4. & \quad \quad v = u & \text{SC, 3} \\ 5. & \quad \quad P(v) & \text{SC, 3} \\ 6. & \quad \quad P(v) \to P(u) & \text{MP, 1, 4} \\ 7. & \quad \quad P(u) & \text{MP, 6, 5} \\ 8. & \quad P(u) & \text{C, 3} \\ 9. & \exists v (v = u \land P(v)) \to P(u) & \text{DT, 1-8} \\ \end{array}
Steps 3-8 use T17.12 letting $\Delta$ be $\{\exists v (v = u \land P(v))\}$, $v$ be $v$, $P$ be $v = u \land P(v)$, and $Q$ be $P(u)$. $v$ is not free in $\Delta$. $v$ is not free in $Q$ by the definition of similar. Is this correct?
I think then that the next step is to prove that this version of E2 follows from the version in my book (at the top of my question).
Hint
See Th.17.4 [page 75]: If $\Delta \vdash P(t/v)$, then $\Delta \vdash \exists v P(v)$, provided that...
Assume $\{ P(u) \}$ as $\Delta$ and with equality axiom E1 we have $\vdash u=u$.
Thus:
Then apply Th.4 to get: $\exists v \ (v=u \land P(v/u))$.
For the other "direction", we can start from $\exists v \ (v=u \land P(v))$ and use the existential elimination rule [page 40] to get: $t=u \land P(t/v)$.
Then by equality axiom E2 we get: $P(u)$.