# Deriving a sentence - Predicate logic

$\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

6)...

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

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

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$

• You could reach a contradiction one step earlier due to 9 and 10. Mar 11, 2018 at 23:10
• 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) ? Mar 11, 2018 at 23:13
• @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)$ Mar 11, 2018 at 23:16
• @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 ... Mar 11, 2018 at 23:18
• @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. Mar 12, 2018 at 0:45