I want to derive the following:

∀x(Fx ↔ (¬Gx ∨ ¬Hx)). ¬∀x(Gx ∧ Hx) → ∃x(Ix ∧ ¬Gx) ∴ ∃xFx → ∃x(Ix ∧ Fx)

This is my attempt:

enter image description here

Any suggestions as to how I continue and derive this? I cannot figure out how to continue
Thank you

EDIT: These are the inference rules as well as the derivation rules and assumptions:

enter image description here

  • Could you clarify what rules of inference are you using and include the proof checker website ?
    – F. Zer
    Apr 22 '20 at 11:59
  • 1
    @F.Zer I have edited it to show above. The proof checker is called Elogic
    – applepi
    Apr 22 '20 at 12:05

I do not have Elogic software, but perhaps this gives you a rough guide about the proof. I used some of @Mauro Allegranza excellent suggestions.

You assume ∃xFx and then assume ¬∃x(Ix ∧ Fx) in order to use Indirect Proof (your system calls this rule Indirect Derivation).

enter image description here

  • Thank you. Can I ask do you know where I can find a guide to the definitions you have used? @F.Zer
    – applepi
    Apr 22 '20 at 13:59
  • You are welcome. Here proofs.openlogicproject.org is the proof checker I used in the proof. In the right side of this webpage, there is a reference of the rules used.
    – F. Zer
    Apr 22 '20 at 14:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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