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$?
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:
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.