2
$\begingroup$

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)

$\endgroup$
2
$\begingroup$

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

$\endgroup$
4
$\begingroup$

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)}$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.