# Logic Proof: Predicate Calculus

Is my proof correct? Thank you so much for your help!

Premise:

$\forall x ((Lx \rightarrow Ix) \rightarrow ((Wx \land Sx) \rightarrow \neg Lx))$

Conclusion:

$\forall x ((Wx \land Ix) \rightarrow (\forall y (Wy \rightarrow Sy) \rightarrow \neg Lx))$

My first step is to rewrite the premise (I would love if you can show me a proof without doing this because conditionals make crazy, but I want to learn how to use them without changing $\rightarrow$ to $\lor$ symbols!!!)

1) $\forall x ((\neg(\neg Lx \lor Ix) \lor \neg(Wx \land Sx)) \lor \neg Lx)$

2) $((\neg(\neg La \lor Ia) \lor \neg(Wa \land Sa) \lor \neg La))$ Universal Instantiation 1), a/x, flag a

3) $\forall x (Wx \land Ix)$ Conditional Proof Assumption

4) $\forall y (Wy \rightarrow Sy)$ Conditional Proof Assumption

5) $Wa \land Ia$ Universal Instantiation 3)

6) $Wa \rightarrow Sa$ Universal Instantiation 4)

7) $Wa$ Simplification 5)

8) $Ia$ Simplification 5)

9) $Sa$ Modus Ponens 6), 7)

10) $\neg La$ Disjunctive Syllogism 2), 7), 8), 9)

11) $\forall x ((Wx \land Ix) \rightarrow (\forall y (Wy \rightarrow Sy) \rightarrow \neg Lx))$ Universal Generalization, a/x, a/y

Q.E.D.

Here is one example of the logic book that I am using, Symbolic Logic by Virgina Klerk

Example 2 Part A

Example 2 Part B

• What book/text are you using? In particular, how is your universal generalization rule defined? – Bram28 Dec 7 '16 at 19:36
• Ah, thanks, that helps! ... what does F.S. stand for? – Bram28 Dec 7 '16 at 19:57
• F.S. means Flag Subproof – Beginner Dec 7 '16 at 20:00
• Got it, thanks! – Bram28 Dec 7 '16 at 20:08

Your proof has a few problems:

On line 11 you do two universal generalizations, and yet one of the universals ends up in the middle of the statement. You need to do the inside generalization first, then get the conditional, and then do the outside generalization.

Line 3 is also not correct, given that you need that same $x$ later in the conclusion. Put a different way: you seem to treat the conclusion as if it were a conditional, with $\forall x (Wx \land Ix)$ being its antecedent, but that is npt what the conclusion is. The conclusion is a universal with a conditional on the inside, so you need to introduce a new constant, and then prove the conditional with that constant filled in for the variable.

Finally, to deal with the conditional in the premise is not too hard. I'll show you below:

1) $\forall x ((Lx \rightarrow Ix) \rightarrow ((Wx \land Sx) \rightarrow \neg Lx))$ Premise

2) $\qquad$ flag $a$

3) $\qquad \qquad Wa \land Ia$ Cond. Proof Assumption (CPA)

4) $\qquad \qquad (La \rightarrow Ia) \rightarrow ((Wa \land Sa) \rightarrow \neg La)$ UI 1

5) $\qquad \qquad \qquad La$ ******CPA

6) $\qquad \qquad \qquad Ia$ Simp. 3

7) $\qquad \qquad La \rightarrow Ia$ CP 5-6

8) $\qquad \qquad (Wa \land Sa) \rightarrow \neg La$ MP 4,7

9) $\qquad \qquad \qquad \forall y (Wy \rightarrow Sy)$ CPA

10) $\qquad \qquad \qquad(Wa \rightarrow Sa)$ UI 9

11) $\qquad \qquad \qquad Wa$ Simp. 3

12) $\qquad \qquad \qquad Sa$ MP 10,11

13) $\qquad \qquad \qquad Wa \land Sa$ Conj. 11,12

14) $\qquad \qquad \qquad \neg La$ MP 8,13

15) $\qquad \qquad \forall y (Wy \rightarrow Sy) \rightarrow \neg La$ CP 9-14

16) $\qquad (Wa \land Ia) \rightarrow (\forall y (Wy \rightarrow Sy) \rightarrow \neg La)$ CP 3-15

17) $\forall x (Wx \land Ix) \rightarrow (\forall y (Wy \rightarrow Sy) \rightarrow \neg Lx)$ UG 2-16

• Thank you for your fast and helpful answer! I am also wondering if line 11 is right. I am reading Understanding Symbolic Logic, Fifth Edition, by Virginia Klenk – Beginner Dec 7 '16 at 19:40
• @Beginner Aye, I don't have that book. OK, can you explain to me how universal generalization is defined in that book? Or maybe give a small example the book gives that you know is a correct use of it? – Bram28 Dec 7 '16 at 19:41
• Sure. It will be my pleasure I will post an image soon. – Beginner Dec 7 '16 at 19:45
• What can I say? It looks fantantic! Thank you so much! You explain much better than my professor, and my professor is an amazing guy! – Beginner Dec 7 '16 at 20:04
• I will edit my other proof trying to use your teachings! Thank you! – Beginner Dec 7 '16 at 20:12