You would see this syntax in a typical mathematical logic class. It ANDs (&) together each statement before and after the ->. Here, we might say -- Ha: a is Hu

You would see this syntax in a typical mathematical logic class. It ANDs (&) together each statement before and after the ->. Here, we might say -- Ha: a is Human, Ma: a is Mortal. Then the first example says: "((For all x, if x is Human, then x is Mortal) AND (s is Human)) IMPLIES (s is Mortal)". We could write it on one line like this: (x,Hx->Mx) & Hs -> Ms, which gives the same result (necessarily true). To show that ~(Hs->Ms) is not logically equivalent to Hs->~Ms, you would write: ~(Hs->Ms) <=> Hs->~Ms. If you want, you can break it into three lines instead. The web app says this is contingent, which indicates it is neither always true nor always false. (Though technically this is a false statement, since they are not logically equivalent.) An example that is always false would be: Hs <=> ~Hs (i.e. from it we derive a contradiction). Compare that to the logically consistent statement: ~(Hs->Ms) <=> Hs & ~Ms. ("(It is NOT the case that (s being Human IMPLIES s is Mortal)) IF AND ONLY IF (s is Human) AND (s is NOT Mortal).") In other words: the only time Hs does not imply Ms is (of course) when Hs is true and Ms is false!