Another question I'm struggling on with predicate logic:


(There exists x) ~Fx

(For all x) Ox

Desired conclusion: ~(For all x)(Ox > Fx) (if Ox, then Fx)

My thoughts are to start by assuming the opposite of the conclusion, and then using subderivations to get Ox and Fx via horseshoe introduction. Help would be appreciated here - I'm not even sure if I'm starting in the right spot.

1 Answer 1


Here is one way to approach this using the natural deduction proof editor and checker:

enter image description here

As you suggested assume the negative of what you want to prove in a subproof.

Eliminate the double negative in line 4.

Now there are two statements with universal quantifiers. Eliminate both of them using the same name "a".

Use those results to eliminate the conditional in line 7.

Introduce a universal quantifier in line 8.

In lines 9 and 10 get a contradiction by using line 1 and the conversion of quantifers rule (CQ). See Chapter 33 in forall x: Calgary Remix for more information about conversion of quantifiers.

  • Your explanations have been super beneficial - actually ended up helping me on some other problems I didn't post here. Thanks so much!
    – ephemeron
    Jun 30, 2018 at 23:58
  • There is no need for double negation elimination; just assume the universal, derive the contradiction, then introduce the negation. Jul 30, 2018 at 14:04
  • @GrahamKemp Yes, that would work. I could use the negative introduction rule to get the result. Jul 30, 2018 at 14:11

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .