Solving a proof with Fitch

Question

I'm working on an assignment and I'm stuck on this proof. I feel like I'm on the right track but I can't find the way to prove the goal.

B ^ D

(B^¬A) → ¬C

B → ¬A

(D^E)→ (A v C)

GOAL: ¬E

Answer 1

I started by ^elim for B and D, then I did a subproof to start eliminating the conditionals, but how could I prove ~E when ~E is not in the premises? I can't seem to find the logical way to do that.

Good start, but you do not need a subproof to eliminate the conditionals. It is an in-context inference.

Okay, now the goal is ¬E when that negation may not be directly derived. That is an indication to try an indirect proof (a proof of negation).

So assume E and seek to derive a contradiction. Let's get you started.

 1.|  B ^ D            premise
 2.|  (B^¬A) → ¬C      premise
 3.|  B → ¬A           premise
 4.|_ (D^E) → (A v C)  premise
 5.|  D                ^elim 1
 6.|  B                ^elim 2
 7.|  ¬A               →elim 3,5
 8.|  B ^ ¬A           ^intro 6,7
 9.|  ¬C               →elim 2,8 
10.|  |_ E             assumption
11.|  |  D ^ E         ^intro 5,10
12.|  |  (A v C)       →elim 4,11
  :|  |  :
  :|  |  :
   |  |  #             ¬elim
   |  ¬E               ¬intro 

Well, obviously Proof by Cases is next.

PS: Some Fitch systems do not include a falsum symbol. Their implementation of negation elimination/introduction may differ somewhat, but the basics are the same. If a contradiction is derivable when E is assumed, then we may infer ¬E.