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?– Mauro ALLEGRANZAJul 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.– Mauro ALLEGRANZAJul 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.– causativeJul 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-twoJul 30, 2021 at 11:34
-
1@user21820 thanks, I'll check these out 👍– part-twoJul 31, 2021 at 0:55