How do I prove ∀x(A(x) -> B(x)) from ~∃x(A(x) ^ ~B(x)) using a fitch proof? [closed]

Question

What would the formal fitch proof for this be? This question came up in my practice problems and I'm really stuck on how to proceed. I'm assuming that you start with an assumption, but I can't figure out where to go from there. Any help would be appreciated thank you!

Answer 1

Always look at where you want to go. Start at the target and work back.

To prove a universal quantified conditional statement, such as is ∀x (A(x) -> B(x)), clearly we set up a universal introduction subproof and nest a conditional introduction subproof inside it.

 |_ ~∃x (A(x) ^ ~B(x))
 |  |_ [c]
 |  |  |_ A(c)
 |  |  |  :
 |  |  |  B(c)
 |  |  A(c) -> B(c)      Conditional Introduction
 |  ∀x (A(x) -> B(x))    Universal Introduction

Now, you have more to work with. We have an assumption of A(c) and the negative existential premise ~∃x (A(x) ^ ~B(x)), and from that we need you to derive B(c). Hmm...

---

Reduction to Absurdity seems indicated, does it not?

 |_ ~∃x (A(x) ^ ~B(x))
 |  |_ [c]
 |  |  |_ A(c)
 |  |  |  |_ ~B(c)
 |  |  |  |  :
 |  |  |  |  :
 |  |  |  |  #           Negation Elimination
 |  |  |  ~~B(c)         Negation Introduction
 |  |  |  B(c)           Double Negation Elimination
 |  |  A(c) -> B(c)      Conditional Introduction
 |  ∀x (A(x) -> B(x))    Universal Introduction

Filling in the remainder of the proof should be obvious.

Answer 2

Well, I'd do it like this. Though it's going to depend on what rules you have available to you. Depending on the exact system you're using you may need to unpack all the quantifiers and then re-pack them to reach the same conclusion.

1. ~∃x(A(x) ^ ~B(x)) (premise)
2. ∀x ~(A(x) ^ ~B(x)) (quantifier negation)
3. ∀x ~A(x) ∨ ~~B(x) (DeMorgan)
4. ∀x ~A(x) ∨ B(x) (double negation elimination)
5. ∀x A(x) -> B(x) (implication)