Show $\vdash P(a) \to \forall x(P(x) \lor \lnot(x=a))$ using natural deduction

Question

Can somebody help me with this question? The question is to show

$$\vdash P(a) \to \forall x(P(x) \lor \lnot(x=a))$$

using natural deduction.

Here is my attempt:

I think I am going half-way through the question but I can't reach the conclusion.

My proof is right until line 8, but when I want to use the "implication introduction rule" my proof goes wrong.

Edit: I am using the online proof checker from https://proofs.openlogicproject.org/

Answer 1

The following proof uses the proof checker used by the OP and Adam's hint on Philosophy SE:

The part that may offer some confusion is the equality elimination (=E) on line 9. What it does is substitutes $a$ for $b$ in $\lnot Pb$ on line 6 to get $\lnot Pa$ on line 9.

Consider the attempt made by the OP:

The reason there is an issue with line 9 is because the subproof is between lines 2 and 8, not between lines 1 and 8. Starting with the assumption on line 2 one is not able to discharge that assumption with any available rule. One has to discharge the assumption on line 2 and then one can introduce the conditional.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

Answer 2

[

$\quad$P(a)$\quad${Entering a fantasy}

$\quad$[

$\quad\quad$$x=a$$\quad${Entering a fantasy}

$\quad\quad$P(a)$\quad${Bringing inside fantasy}

$\quad\quad$P(x)$\quad${Substitution with $x=a$}

$\quad$]

$\quad$$x=a$ implies P(x)$\quad${Fantasy rule}

$\quad$!! $x=a$ implies P(x)$\quad${Adding double negative}

$\quad$! $x=a$ or P(x)$\quad${Switcheroo rule}

]

P(a) implies !$x=a$ or P(x)$\quad${Fantasy rule}

P(a) implies ALLx: !$x=a$ or P(x)$\quad${x is a free variable}

QED

By the way I have used '!' for "not"

I have used [] to enter and exit fantasies.

All the logical terminology is from the book Godel Escher Bach

Answer 3

Using the DC Proof 2.0 proof checker ('|' is the OR-operator)