Solving a proof with Fitch

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

• "on the right track"... What have you tried ? – Mauro ALLEGRANZA May 12 '20 at 16:52
• The conclusion is a negation; so, a possible strategy is to work by contradiction. – Mauro ALLEGRANZA May 12 '20 at 16:52
• 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. – eaglefern May 12 '20 at 17:02
• Don't put clarifications in the comments. Please edit your question. @eaglefern. – Graham Kemp May 13 '20 at 1:28

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`.

• Hi, I tried Proof by cases, but I keep getting errors – eaglefern May 13 '20 at 2:34
• It should be straightforward. A contradiction may be derived when assuming the left case (`A`) because you may reference line 7 (`¬A`). A contradiction may also be derived when assuming the right case (`C`) because you can reference line 9 (`¬C`). – Graham Kemp May 13 '20 at 3:15
• Thank you. I figured it out. – eaglefern May 13 '20 at 22:25