Confusion with Equivalence and Replacement theorems

Question

Proposition: If $\psi$ is a subformula of $\phi$ and $\phi'$ results from replacing $0$ or more occurrences of $\psi$ in $\phi$ by a wf $\rho$ and each free variable of $\psi$ or $\rho$ that it's also a bound variable of $\phi$ occurs in the list $y_1,y_2,...,y_k,$ then

$$a)\vdash [\forall y_1...\forall y_k(\psi\leftrightarrow\rho)]\to(\phi\leftrightarrow\phi')$$ $$b) \vdash\psi\leftrightarrow\rho\implies\vdash\phi\leftrightarrow\phi'$$ $$c)\vdash\psi\leftrightarrow\rho,\vdash\phi\implies\vdash\phi'$$

I don't understand a) and I tried to understand it with a particular example but I got more confused, and the only example that appears in the book is this $$a) \forall x(A_1(x)\leftrightarrow A_2(x))\implies(\exists xA_1(x)\leftrightarrow \exists A_2(x))$$ for which I still don't see the relation with the theorem a).

Could someone explain to me how I could understand these theorems? Maybe with another kind of examples. I need to understand the proposition to solve my homework.

---

The example that I construct is this

Suppose $\phi=[\forall x(P(x)\to Q(x))]\to R(y).$ Then a subformula of $\phi$ is $\psi=\{[\forall x(P(x)\to Q(x))]\to R(y),\forall x(P(x)\to Q(x)),P(x)\to Q(x),P(x),Q(x),R(y)\}$. Now I suppose that $\psi$ have 1 ocurrence in $\phi ,$ $\phi'=\rho$. But from here I can't assume $\rho\leftrightarrow\psi$ because $\rho$ is a wf and $\psi$ is a set.

Answer 1

The set $\psi$ (in your example), is the set of all subformula of $\phi$, i.e, a subformula is a wf this is not a set.

Now, if $\phi$ is as your example and $\rho\equiv R(y)\wedge R(y)$, then $$ \vdash\forall y(R(y)\leftrightarrow\rho) $$ So, by $(a)$, you can conclude (and deduction theorem) $$ \vdash(∀x(P(x)→Q(x))→R(y))\leftrightarrow(∀x(P(x)→Q(x))→\rho). $$

Answer 2

You have to manufcature some simple but meaningful example like e.g.

$\forall x ( x \ge 0) \to (1 \ge 0)$

as $\phi$.

We know (we can prove it) that $\forall x$ is equivalent to $\lnot \exists x \lnot$.

Thus, we have $\forall x ( x \ge 0)$ as $\psi$ and $\lnot \exists x \lnot (x \ge 0)$ as $\rho$.

The condition $\psi \leftrightarrow \rho$ is satisfied, and the part b) of the theorem allows us to conclude that:

$(\forall x ( x \ge 0) \to (1 \ge 0)) \leftrightarrow (\lnot \exists x \lnot ( x \ge 0) \to (1 \ge 0))$.

For part a), consider as $\psi: \forall x ( x \ge y)$ and as $\phi : \forall x ( x \ge y) \to (1 \ge y)$.

We have: $\forall y [ \forall x ( x \ge y) \leftrightarrow \lnot \exists x \lnot (x \ge y)]$, and then apply the theorem again.

---

The gist of the theorem is: we may replace provably equivalent formulas into a "context" formula without "changing the meaning".