-1

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!

5
  • 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). – John Beverley Dec 12 '20 at 7:44
  • 2
    What have you tried ? No idea ? – Mauro ALLEGRANZA Dec 12 '20 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. – galileo Dec 12 '20 at 22:28
  • Try assuming Ex(Ax & ~Bx). Then find a contradiction. – John Beverley Dec 13 '20 at 4:35
  • would the next line be a contradiction then because lines 1 and 2 contradict one another? – galileo Dec 13 '20 at 23:51
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.

0

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)

Not the answer you're looking for? Browse other questions tagged or ask your own question.