Express exactly two logically

Question

Let C(x, y) : "x and y have chatted over the Internet"

where the domain for the variables x and y consists of all students in your class.

a ) There are two students in your class who have not chatted with each other over the Internet.

My answer: $\exists x \exists y[(x \not =y) \land \lnot C(x, y)]$

I googled it and mine found correct.

b ) There are exactly two students in your class who have not chatted with each other over the Internet.

My answer: $\exists x \exists y[(x \not =y) \land \lnot C(x, y) \land \forall a \forall b(\lnot C(a, b) \iff ((a = x \land b = y)\lor(a = y \land b = x)))]$

Am I correct for question b?

Answer 1

I was going to comment on the ambiguity from the lack of braces but now that you've edited, I believe it is correct. I would remove the equivalence and just leave it as an implication as it is redundant and makes it a bit harder to read.

$\exists x \exists y[(x \not =y) \land \lnot C(x, y) \land \forall a \forall b(\lnot C(a, b) \implies ((a = x \land b = y)\lor(a = y \land b = x)))]$

EDIT: thinking further I feel like I want to add this as maybe somebody is (not) chatting with himself over the internet, but we don't want this to bother us.

$\exists x \exists y[(x \not =y) \land \lnot C(x, y) \land \forall a \forall b\{ [a\neq b \land \lnot C(a, b)] \implies ((a = x \land b = y)\lor(a = y \land b = x))\}]$

Answer 2

Your answer is correct. In fact, given that you use a biconditional, you can leave out the $\lnot C(x, y)$:

$\exists x \exists y[(x \not =y) \land \forall a \forall b(\lnot C(a, b) \iff ((a = x \land b = y)\lor(a = y \land b = x)))]$

(do you see why this works?)

Please do make sure that you can use $a$ and $b$ as variables in your system: some systems regard those as individual constants.