1

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:

enter image description here

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/

Frank Hubeny
  • 1,527
Waliy Ismail
  • 21

3 Answers3

1

[

$\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

aman
  • 1,294
1

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

enter image description here

Dan Christensen
  • 14,529
1

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

enter image description here

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:

enter image description here

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/

Frank Hubeny
  • 1,527
  • so for attempt that I made is completely wrong? or is there another way to improvise it? – Waliy Ismail Apr 07 '19 at 06:28
  • @WaliyIsmail I think the mistake was in using that particular assumption on line 2 rather than an assumption that could be discharged.later. When making an assumption think of how you might be able to discharge it later. The assumption on line 2 assumed the consequent of the conditional you wanted to show true. That consequent would have to be derived from the antecedent (line 1) somehow. So I don't think this approach would work. – Frank Hubeny Apr 07 '19 at 13:25
  • okay got it, thanks! – Waliy Ismail Apr 07 '19 at 17:55