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

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!

• In outline: Suppose Ex(Ax & ~Bx) for reductio. Instantiate the existential to a constant, say, b. Instantiate the universal to b. Use modus ponens to prove Bb & ~Bb. Infer ~Ex(Ax & ~Bx). Dec 12, 2020 at 7:44
• What have you tried ? No idea ? Dec 12, 2020 at 8:40
• I honestly have no idea. My first instinct was to assume A(a) /\ B(b) but I don't think that's correct. Dec 12, 2020 at 22:28
• Try assuming Ex(Ax & ~Bx). Then find a contradiction. Dec 13, 2020 at 4:35
• would the next line be a contradiction then because lines 1 and 2 contradict one another? Dec 13, 2020 at 23:51

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.

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)