Write in Logic: If professors are unhappy all students fail their exams

Question

I have to write the following sentence "If professors are unhappy all students fail their exams" in logic and my answer is:

∀x [Prof(x) ∧ Unhappy(x)] ⇒ [∀y stud(y) ⇒ fail_exam(x,y)]

However, the answer of my teacher is:

∀x ∀y( prof(x) ∧ unhappy(x) ∧ stud(y) ) ⇒ fail exam(x, y))

Can someone helps me?

Answer 1

They are equivalent ... although to show that, I will first insist on adding a few parentheses so as to indicate the proper scope of the quantifiers, giving us:

$\forall x ((Prof(x) \land Unhappy(x)) \rightarrow \forall y (Stud(y) \rightarrow FailExam(x,y)))$

and

$\forall x \forall y ((Prof(x) \land Unhappy(x) \land Stud(y)) \rightarrow FailExam(x,y))$

Now, to show these are equivalent, let us first note the following general 'Prenex Law', which is an equivalence that allows you to 'take out' quantifiers and broaden their scope to include ('move over') other parts of the formula:

$\psi \rightarrow \forall x \ \varphi(x) \Leftrightarrow \forall x (\psi \rightarrow \varphi(x))$

Here, the formula $\psi$ cannot include any free variables $x$

Well, we can apply this Prenex law to the second formula, and take out the $\forall y$, since the antecedent of the conditional you are moving it over does not contain any free variables $y$. Thus, we get:

$\forall x \forall y ((Prof(x) \land Unhappy(x) \land Stud(x)) \rightarrow FailExam(x,y))$

Ok, and now we can apply a second general equivalence principle that mAuro alluded to in the comments, called eXportation:

$P \rightarrow (Q \rightarrow R) \Leftrightarrow (P \land Q) \rightarrow R$

Applied to the previous formula, we thus obtain the first of your two formulas, thus showing that they are equivalent.

Answer 2

You've been answered that they are equivalent. It's also worth knowing the transformation from $(P\land Q) \rightarrow R$ to $P\rightarrow Q \rightarrow R$ is known by the name of "currying", and its inverse "uncurrying". It shows up not only in logic, but any domain that forms a Cartesian Closed Category.