Ex(Hx & Ax), Ax(Ax -> Ey(Dy & Txy)), AxAy((Dy & Txy) -> Wx) |- Ex(Hx & Wx)
In the third premise we need to have both quantifiers up front, and we use a universal quantifier for the courses since the concept is that any single instance is enough to trigger the condition.
Ex(Hx & Ax)
Ax(Ax -> Ey(Dy & Txy))
AxAy((Dx & Txy) -> Wx)
~Ex(Hx & Wx)
Ax(Hx -> ~Wx)
Ha
Aa
Aa -> Ey(Dy & Tay)
Ha -> ~Wa
/
\
~Ha ~Wa
x
/ \
~Aa Ey(Dy & Tay)
x Db &
Tab
(Db & Tab) -> Wa
/ \
~(Db & Tab) Wa
x
x
2. No honor students are lazy. Anyone not lazy takes difficult courses. It's necessary for someone taking difficult courses to work hard. Therefore, there are students who are working hard.
Ax((Hx & Sx) -> ~Lx), Ax(~Lx -> Ey(Dy & Txy)), AxAy((Dy & Txy) -> Wx) |- Ex(Sx & Wx)
Because of the different statements in the first premise and in the conclusion, we need to symbolize in a more complete manner for "honor students."
Ax((Hx & Sx) -> ~Lx)
Ax(~Lx -> Ey(Dy & Txy))
AxAy((Dy & Txy) -> Wx)
~Ex(Sx & Wx)
Ax(Sx -> ~Wx)
Sa -> ~Wa
(Ha & Sa) -> ~La
~La -> Ey(Dy & Tay)
/ \
~Sa ~Wa
/
\
~(Ha & Sa) ~La
/
\
~Ha ~Sa
We do not need to go further to see that there
are branches that will not close, so we know that the second argument is
not valid. The key problem is that we never know that there actually
are honor students.
3. Only honor students take difficult courses. None of the courses that the men are taking are difficult. Therefore, only women are honor students.
AxAy((Dy & Txy) -> Hx), AxAy((Mx & Txy) -> ~Dy), Ax(~Mx -> Wx) |- Ax(Hx -> Wx)
We need to add something in the symbolization to show that any "x" not a man would be a woman (remember, polar bears are not men), and this we do in the third premise. But even with this addition we can see that we will not be able to arrive at a valid argument, since we have no way of knowing that there are any women taking difficult courses.
4. Anyone not an honor student takes all easy courses. Alice is taking courses that are not easy. Therefore, Alice is an honor student.
Ax(~Hx -> Ay(Txy -> Ey)), Ey(~Ey & Tay) |- Ha
Ax(~Hx -> Ay(Txy -> Ey))
Ey(~Ey & Tay)
~Ha
~Eb
Tab
~Ha -> Ay(Tay -> Ey)
/
\
Ha
Tab -> Eb
x
/ \
~Tab Eb
x x