What's the deal with empty models in first-order logic? Asaf's answer here reminded me of something that should have been bothering me ever since I learned about it, but which I had more or less forgotten about. In first-order logic, there is a convention to only work with non-empty models of a theory $T$. The reason usually given is that the sentences $(\forall x)(x = x)$ and $(\forall x)(x \neq x)$ both hold in the "empty model" of $T$, so if we want the set of sentences satisfied by a model to be consistent, we need to disallow the empty model.
This smells fishy to me. I can't imagine that a sufficiently categorical setup of first-order logic (in terms of functors $C_T \to \text{Set}$ preserving some structure, where $C_T$ is the "free model of $T$" in an appropriate sense) would have this defect, or if it did it would have it for a reason. So something is incomplete about the standard setup of first-order logic, but I don't know what it could be. 
The above looks like an example of too simple to be simple, except that I can't explain it to myself in the same way that I can explain other examples. 

Okay, if this is the answer, it is quite silly. The axioms of first-order logic in my notes include 
$$(\forall x) p \Rightarrow p[t/x]$$
which is manifestly false for the empty model and $p = \perp$ so should just be thrown out and replaced by the correct axiom
$$(\forall x) p \wedge (\exists x) \Rightarrow p[t/x].$$
Nothing changes except for the empty set, where the statement $(\forall x) \perp$ is true but $\perp$ is not, so there is no contradiction. 
