0

I'm working on a bigger proof using natural deduction and I'm struggling with a final step, which is showing $Fd$ follows by natural deduction from $Gd$, $∃x¬Gx$ ($d$ is a random constant, $G,F$ are unary predicates). No matter what rule I try, it doesn't seem to work. Would greatly appreciate some help.

Othman El Hammouchi
  • 734
  • 4
  • 12
  • 1
    No wonder you're struggling; the sequent isn't provable. Are you sure ou copied the assignment correctly and it' snot $\neg \exists x Gx$ rather than $\exists x \neg Gx$? – Natalie Clarius Dec 06 '20 at 18:26
  • No, it was correctly copied. Sequents are relevant to deriving, not natural deduction, right? I need to use natural deduction and its rules. – Othman El Hammouchi Dec 06 '20 at 18:44
  • 1
    By "sequent" I meant the pair of premises and conclusion. You can't derive it in ND. If it's the last part in some other proof you're doing, you seem to be on the wrong track and need to reconsider what you did earlier on. – Natalie Clarius Dec 06 '20 at 18:56
  • Well maybe you could help me get on the right track please? The full exercise is to derive $∃xFx$ from $∃x¬Gx$ and $Ɐx(Fx v Gx)$. My idea was derive an instantiation $Fd$ from the premises using AND-elimination and continue from there, but evidently that's a fruitless path. – Othman El Hammouchi Dec 06 '20 at 19:59
  • 1
    The $x$ of which $F$ holds will be that $x$ of which $G$ is false. The main idea is to do an $\exists$-elimination on $\exists x \neg Gx$ to give that something a name (e.g. $d$) and derive $Fd$ using the fact that $Fx \lor Gx$ also holds of that $d$. – Natalie Clarius Dec 06 '20 at 21:34
  • Worked like a charm. Thanks a lot! – Othman El Hammouchi Dec 07 '20 at 00:52

0 Answers0