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 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 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 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 at 11:34
  • 1
    @user21820 thanks, I'll check these out 👍
    – part-two
    Jul 31 at 0:55

Your Answer

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

Browse other questions tagged or ask your own question.