Logic & Proof Ch. 8 Homework Question

Stream: general

[Dominic Farolino]

Hi, for a homework assignment, one of the questions I have to do is #2 in section 8.6 of the Logic and Proof book. The question is: "Give a natural deduction proof of ∀x B(x) from hypotheses ∀x (A(x) ∨ B(x)), and ∀y ¬A(y). My thoughts were to proof B(x) by contradiction, because by doing so, I get to assume ¬ B(x), and from ¬ B(x) and my other assumption ∀y ¬A(y), I can derive, through De Morgan's laws ¬ (A(x) ∨ B(x))`, which should be enough to get the contradiction. Could someone check my proof in the attached picture and perhaps provide feedback? I'd really appreciate it! IMG-1413.JPG

[Dominic Farolino]

I think it is close, but it feels a little off since I have not cancelled all of my hypotheses

[Dominic Farolino]

Or I guess the two given hypotheses don't need cancelled, since they were simply given?

[Dominic Farolino]

(deleted)

[Dominic Farolino]

Actually I think it can be done simpler: IMG-1414.JPG

[Andrew Ashworth]

Why not do it in Lean? Then it'll check your proof for you!

[Dominic Farolino]

I haven't read chapter 9 yet!