# Zulip Chat Archive

## Stream: general

### Topic: Logic & Proof Ch. 8 Homework Question

#### Dominic Farolino (Feb 13 2019 at 05:46):

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 (Feb 13 2019 at 05:47):

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

#### Dominic Farolino (Feb 13 2019 at 05:51):

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

#### Dominic Farolino (Feb 13 2019 at 06:04):

(deleted)

#### Dominic Farolino (Feb 13 2019 at 06:05):

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

#### Andrew Ashworth (Feb 13 2019 at 06:50):

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

#### Dominic Farolino (Feb 13 2019 at 07:08):

I haven't read chapter 9 yet!

Last updated: Aug 03 2023 at 10:10 UTC