Finding a satisfiable closed wf that is not true if the domain has fewer than three elements (I can't add the homework tag) 
For my logic class, I have found the following wf: 
$$
\mathcal{B} \mbox{ is } \forall x \exists y \mbox{  } A(x) \land \lnot A(y)
$$
This function is satisfiable (take the integers as domain and $A(x)$ is $x$ is even), but in an interpretation $M$ with a domain with only one member it is false. 
Now I want to find another satisfiable closed wf, such that in an interpretation where  the domain has two members or less, it is false. 
Inspired by the last expression, I came up with:
$$
\mathcal{C} \mbox{ is } \forall x \forall y \exists z \mbox{ }A(x,z) \land A(y,z) \land \lnot A(x,y) \land \lnot A(y,x)
$$
It seems to me that in a domain with one or two members, this $\mathcal{C}$ is not true. But I wonder if it satisfiable, for instance if $D$ are the natural numbers and $A(x,y)$ denotes $x \geq y$ , with the sequence $s = (2, 2, 0)$, then $\mathcal{C}$ is true, so $s$ satisfies $\mathcal{C}$, hence $\mathcal{C}$ is satisfiable. 
Is this thinking correct?
And how can I see if a function is false for a domain with zero memebers (the empty set)? 
 A: If you have $=$ as a primitive logical concept, then you can use
$$ \forall x\forall y\exists z(z \ne x \land z\ne y) $$
to assert that the domain has at least three elements. This has the advantage that you don't need to speak about satisfiability, but is simply a matter of truth in the structure.
In contrast, your solutions depend on the structure cooperating in assigning the meaning you need to $A$ -- if you get a structure that doesn't contain an appropriate $A$, you would need to extend the structure with one in order to use your idea to test it. That is probably not what your exercise is asking for.
Hmm, I suppose it could be asking for an $=$-less formula that is (a) not satisfied by any too small structure, but (b) satisfied by some (but not necessarily all) structures with three or more objects. In that case you could use the same idea as above, but add your own axiom that forces a predicate of your own choosing to behave "sufficiently much" like equality, as in
$$ \forall x(A(x,x)) \land \forall x\forall y\exists z(\neg A(z,x)\land \neg A(z,y)) $$

As first-order logic is usually defined, structures with zero members are not allowed at all (since they create problems for the most natural proof rules for quantifiers, for no good reason), so you can know that if you're in ordinary first order-logic, then there's at least one element.
In other words, the formula $\exists x(x=x)$ is logically valid.
A: The first sentence is a contradiction, hence satisfiable nowhere:
The sentence $\forall x\exists y(A(x)\land\lnot A(y))$ immediately implies that $\forall x A(x)$, so you conclude $A(y)\land \lnot A(y)$. In particular in your model you need to show that for every number $n$ there exists a number $m$ such that $A(n)$ and $\lnot A(m)$. If $A(x)$ is interpreted as "$x$ is even" then the sentence fails for $n=1$. 
The formula (which is not closed) $\exists y(A(x)\land\lnot A(y))$ is satisfiable in the model that you describe, that is, there exists some element $n$ in your model such that $M\models \exists y(A(n)\land\lnot A(y))$.
As for the formulas you are looking for, as Henning Makholm noted, it's a good idea to use equality as a relation in your language.
