Translate the following inference to logic notation: It is not sunny. For all x, y_2 is a carpenter if and only if y_2 will read a book. It is sunny if and only if Barbara is listening to a song. Charles is reading a book if and only if Barbara is listening to a song. Therefore Charles is not a carpenter.
~p. forall x: P(x) <-> Q(x). p <-> q. Q(a) <-> q. Therefore ~P(a).