Using the Fitch application and only Intro and Elim rules (& REIT if necessary), prove that $$\forall x \forall y (P(x) \implies Q(y)) \iff (\exists x P(x) \implies \forall y Q(y))$$ is a logical truth (i.e. prove it from no premises)

I am attaching a screenshot of my work so far, please give me feedback and/or assistance so that I can fix or finish this proof. I am currently stuck and don't know if what I did is right or not because I don't know what to do next. Any feedback is appreciated. Thanks. This is my work here.

  • $\begingroup$ Welcome to CS.SE! I want to explain something about this site that might not be obvious -- part of the purpose of this site is to build up an archive of questions and answers that will be useful not only to the individual who asked, but to many others in the future. This question looks very specific to your particular situation. Generally we discourage questions that ask us to check your work or to fix problems in it (for instance, it's unlikely that anyone else will ever have exactly the same situation in the future). $\endgroup$ – D.W. May 2 at 21:52
  • $\begingroup$ I don't know the Fitch application, so I'm going to guess from what I'm seeing that it's a pretty standard natural deduction prover. The outermost thing you're trying to prove is a biconditional, so you have to prove both directions. It looks like the program is happy with the forward direction, but it requires you to prove the other direction of the biconditional before it will accept the biconditional as proven. Again, just a guess by eye-balling it. $\endgroup$ – ShyPerson May 12 at 20:00

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.