I recently discovered https://proofs.openlogicproject.org/, except I'm still figuring out the appropriate rules that are needed for the system to check my proof. I thought it'd be quicker to turn to humans.

  • What is step 4? Jul 30, 2021 at 11:07
  • A different approach can be: assume the negation of the antecedent of the 2nd premise and derive a contradiction with 1st premise. Jul 30, 2021 at 11:08
  • The second premise should be written like this: (¬∃x (¬Gx ∧ Fx)) → Hac. The way it's written it looks like the whole implication is within the scope of the existential quantifier, which is not what you meant. Other than that what you wrote looks ok.
    – causative
    Jul 30, 2021 at 11:30
  • 1
    @MauroALLEGRANZA "?X" is supposed to be an indefinite subgoal, according to my professor. It's a line that always follows right after the line that states, e.g., ~A, if I want to prove A by indirect proof (IP).
    – part-two
    Jul 30, 2021 at 11:34
  • 1
    @user21820 thanks, I'll check these out 👍
    – part-two
    Jul 31, 2021 at 0:55


You must log in to answer this question.

Browse other questions tagged .