What does the theory of the empty set look like? I know next to nothing about logic, but I was wondering what first order axioms would give rise to the theory of the empty set (that is to a theory whose only model is the empty set)? The problem I have: It seems that first order logic doesn’t allow axioms like “$¬∃x$” because this is an ill-formed statement (as it lacks a predicate). Does one define an own predicate $E$ to denote existence and the axiom would be “$¬∃xEx$”?
Addendum. If we assume predicate logic with equality, is it done by stating “$¬∃x(x=x)$” together with the axiom of reflexivity of equality? Or more generally, is it done by making “$∀xPx$” and “$∀x¬Px$” axioms for some predicate symbol $P$?
 A: You may use $=$ as we (unless you are doing very special logic) assume $=$ to exist. Now create the sentence $\forall x (x\neq x)$. In any model which contain at least one element this sentence is not true. Thus if $\forall x (x\neq x)$ is an axiom in our theory the only possible model is the empty model. The empty model will satisfy this since each element in it is not equal to it self, as no elements are in it (for each $x\in \emptyset$ then $x$ will satisfy anything).
Note however that depending on the language, the empty model may not actually be a model. More specifically if you have at least one constant in the langauge, then you must have at least one element in the universe of the model to interpret this constant as. For instance if you work with Groups you have the language $\{\cdot,^{-1}, 1\}$ where $1$ is a constant. This is because each group needs to have an identity element which $1$ is interpreted as, and thus the empty model may never be a group.
A: There are two questions: what "should" the theory look like, and what "does" it look like under a given logic.
First, as long as we still require terms to denote objects, there cannot be any closed terms in the language, if we want to consider an empty model. So all sentences must begin with an outermost quantifier.
Under the natural understanding of quantifiers, if there are no elements to quantify over, then universal quantifiers are vacuous and the existential quantifiers all fail. Thus every universally-quantified sentence should be true in the empty model, and every existentially-quantified sentence should be false. In particular, if we have equality in the language, then both $(\forall x)[x = x]$ and $(\forall x)[x \not = x]$ should be true in an empty model.
The challenge with this is that most presentations of first-order logic are designed in a way that assumes models are nonempty. Thus what "does" happen, if we consider empty models without considering the logic, is that the theory than an empty model "should" have is inconsistent. 
For example, from $(\forall x)[x = x]$ and $(\forall x)[x \not = x]$ we can prove every sentence, in ordinary first-order logic.  The proof sketch is:


*

*From $(\forall x)[x = x]$, use universal instantiation to obtain $c = c$ for a new variable $c$.

*Now, instantiate $(\forall x)[x \not = x]$ with $c$ to obtain $c \not = c$

*We now have $c = c$ and $c \not = c$, a contradiction. From this, we can conclude any other formula by ex falso quodlibet.


Therefore, it is necessary to change the underlying inference rules in order to handle empty models. In particular, all existential assumptions regarding universal quantifiers have to be removed.  
This does have costs. For example, we may no longer be able to put sentences in prenex normal form. Normally, the options for the prenex normal form of
$$
(\exists x)[x = x] \land (\forall y)[y = y]
$$
would be
$$
(\exists x)\big ( [x = x] \land (\forall y)[y = y] \big)
$$
and
$$
(\forall y)\big ( (\exists x)[x = x] \land [y = y] \big )
$$
These are equivalent in ordinary first-order logic, but not in the empty structure. 
