$\forall x(Fx \lor \neg Fx) \rightarrow Ga \vdash \exists x Gx$

1) ∀x(Fx v ¬Fx) → Ga Premise

2)¬∃xGx Premise (Negation of conclusion)

3)∀x¬Gx Quantifier negation

4)¬Ga Universal installment

5)¬∀x(Fx v ¬Fx) Modus Tollens


I dont know how to do this derivation. My attempt might be ineffective. Some help/tips please? Thanks in advance :)

  • 1
    $\begingroup$ What specific inference rules do you have? $\endgroup$
    – Bram28
    Mar 11, 2018 at 22:59
  • $\begingroup$ Can you prove $Ga \vdash \exists xGx$? $\endgroup$
    – Git Gud
    Mar 11, 2018 at 23:02
  • $\begingroup$ I have all the rules of Sentenial Logic plus Universal Installment, Universal Generalization, Existential Generalization, Quantifier Negation , E $\endgroup$
    – Mandeyo
    Mar 11, 2018 at 23:02
  • $\begingroup$ Git Gud, i can prove the one that you said, however i am not sure how to deal with proving this. $\endgroup$
    – Mandeyo
    Mar 11, 2018 at 23:04
  • 1
    $\begingroup$ Here's a MathJax tutorial :) $\endgroup$
    – Shaun
    Mar 11, 2018 at 23:21

1 Answer 1


You're on the right track. I don't know if you have the inference rules to do this, But I would follow with:

$6. \exists x \neg (Fx \lor \neg Fx) \quad Quantifier \ Negation \ 5$

$7. \neg (Fb \lor \neg Fb) \quad Existential \ Installment \ 6$

$8. \neg Fb \land \neg \neg Fb \quad DeMorgan \ 7$

$9. \neg Fb \quad Simplification \ 8$

$10. \neg \neg Fb \quad Simplification \ 8$

$11. Fb \quad Double \ Negation \ 10$

$12. Contradiction \ 9,11$

  • $\begingroup$ You could reach a contradiction one step earlier due to 9 and 10. $\endgroup$
    – Git Gud
    Mar 11, 2018 at 23:10
  • $\begingroup$ Wait a second. I am not sure if existential installment is an actual rule? Can we really go from ∃x¬(Fx∨¬Fx) to ¬(Fb∨¬Fb) ? $\endgroup$
    – Mandeyo
    Mar 11, 2018 at 23:13
  • $\begingroup$ @AmandaO That's what I just asked: do you have a rule like that? If not, then this obviously doesn't work for your system ... so then try Git Gud's suggestion: don't do this by a proof by contradiction, but try and prove $\forall x (Fx \lor \neg Fx)$ $\endgroup$
    – Bram28
    Mar 11, 2018 at 23:16
  • $\begingroup$ @GitGud true ... though I have seen systems where you can only get contradiction between atomic statements and their negation so I tried to be safe ... though it now looks as if my assumption that there would be some kind of existential elimination was wrong ... $\endgroup$
    – Bram28
    Mar 11, 2018 at 23:18
  • $\begingroup$ @AmandaO $\exists x~\neg\text{Stuff}(x)$ means that there does exist some value, let us call it $b$, where we witness that $\neg\text{Stuff}(b)$. ... providing the token $b$ does not already occur free in the predicate $\neg\text{Stuff}(x)$. It should be among your ruleset. $\endgroup$ Mar 12, 2018 at 0:45

You must log in to answer this question.

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