Prove using Hilbert calculus $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$, formal proof.

Question

Prove: $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$ Using Hilbert Calculus

Format of solution: Step (my understanding)

Solution:

(1) $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow b\equiv a$ (from $Px\rightarrow x\equiv a$ on the left of $\vdash$)

(2) $\forall x(Px\rightarrow x\equiv a)\vdash b\equiv a \rightarrow (Pb\rightarrow Pa)$ (Where does this come from?)

(3) $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow (Pb\rightarrow Pa)$ (From (1) and (2) since $\rightarrow$ is transitive)

(4) $\forall x(Px\rightarrow x\equiv a)\vdash (Pb\rightarrow (Pb\rightarrow Pa))\rightarrow ((Pb\rightarrow Pb)\rightarrow (Pb\rightarrow Pa))$ (Hilbert Axiom)

(5) $\forall x(Px\rightarrow x\equiv a)\vdash (Pb\rightarrow Pb)\rightarrow (Pb\rightarrow Pa)$ (Modus Ponens)

(6) $\forall x(Px\rightarrow x\equiv a)\vdash (Pb\rightarrow Pb)$ (Hilbert Axiom)

(7) $\forall x(Px\rightarrow x\equiv a)\vdash (Pb\rightarrow Pa)$ (Modus Ponens)

I feel I understand the general argument and every step but one, I have no idea where step (2) of the solution comes from.

I would be grateful for an explanation of step (2)

Answer 1

Step two could actually be $b\equiv a \rightarrow (Pb\leftrightarrow Pa)$. If two items are equal, they have the same properties.

Answer 2

Step $2$ is an instance of Axiom $6$ of formal deduction (see Enderton's A Mathematical Introduction to Logic page $112$):

$\vdash (x=y)\to(\alpha\to\alpha ')$, where $\alpha$ is atomic and $\alpha '$ is obtained from $\alpha$ by replacing $x$ in zero or more places by $y$.

In your case (where $\equiv$ replaces $=$), the atomic formula is $Pb$ and, since $b\equiv a$, we can replace $b$ by $a$ in zero or more places in $Pb$ (actually, in one place) to yield $Pa$.

Since this is an instance of an axiom, it can be directly derived from any set of formulas, and we have:

$\forall x(Px\to x\equiv a)\vdash(b\equiv a)\to(Pb\to Pa)\quad\text{(Axiom 6)}$