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)
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
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).
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