As a student of mathematics I used to accept the argument that the existence of the empty set followed from the axiom schema of comprehension, so long as we could prove the existence of at least one set: if a is any set, then we can derive the existence of {x:a | bot }. I would then argue using the axiom of infinity that the existence of at least one set was established.

Having drifted towards logic and computer science it now seems to me that the existence of at least one set can be derived simply from the deductive system being used, without additional set theoretic axiom.

This is slightly disappointing to me, as I would have liked the existence of at least one set to be a consequence of set theoretic axioms, not a logical consequence of a deductive system. Of course, there are many reasonable deductive system of first order logic we could consider, and it may be that I am looking at the wrong one, which motivates my question.

I am hoping that someone will confirm that the existence of at least one set is indeed a logical consequence (not a set theoretic consequence), or explain the flaws in the forthcoming reasoning, or point to a deductive system where the statement does not hold.

In order to spell out the deductive system I have in mind, let us consider the language where primitive propositions are of the form x in y (where x and ylie in a suitably large set of variables) and bot, and we have an implication -> as well as quantification Ax for every variable x. This language can be represented by the Haskell type:

data Expr v  = In v v
             | Bot 
             | Imply (Expr v) (Expr v)
             | Forall v (Expr v)

or for those who prefer coq:

Inductive Expr (v:Type) : Type :=
| In    : v -> v -> Expr v
| Bot   : Expr v
| Imply : Expr v -> Expr v -> Expr v
| Forall: v -> Expr v -> Expr v

There is nothing else in the language (no constant, no equality). Although ordinary mathematics usually involves a far richer language, the hope is that everything can be desugared in terms of this core language.

Now the deductive system I have in mind is a Hilbert style system with 5 axiom schema and 2 rules of inference (modus ponens and generalization).

(i)     p -> (q -> p)
(ii)    [p -> (q -> r)] -> [(p -> q) -> (p -> r)]
(iii)   [(p -> bot) -> bot] -> p                   (classical mathematics)
(iv)    [Ax.(p -> q)] -> (p -> Ax.q)   (x not free in p)
(v)     Ax.p -> p[y/x]                 (y free for x in p)

Given our rules of inference, we can formally represent our proofs as derivation trees, or specifically as the Haskell inductive data type:

data Proof v  = Axiom (Expr v)
              | Hypothesis (Expr v)
              | ModusPonens (Proof v) (Proof v)
              | Generalize v (Proof v)

and we crucially have a map eval :: Proof v -> Expr v which acts as a sort of type checker, returning the proposition (the type) actually being proved by the proof (the expression). Now of course, not every proof is valid (for example the proof Axiom p is not a valid axiom invocation unless p is indeed an axiom) in which case the eval function can simply return bot -> bot which is a convenient way to state that an invalid proof does not prove anything. When implementing the function eval (which amounts to spelling out our deductive system), we shall need isAxiom :: Expr v -> Bool as well as Hyp :: Proof v -> [Expr v] (which returns the list of hypothesis involved in a proof). The function Hyp is useful to decide whether the proof Generalize x P is valid, by checking that x is not free in any of the propositions of Hyp P. A proof P = ModusPonens P1 P2 is not valid unless eval P2 is of the form eval P1 -> p in which case eval P = p.

Having described our proofs, we can define the sequent G |- p as equivalent to the existence of a proof P such that eval P = p and Hyp P <= G (where the <= is set inclusion and lists are viewed as sets)

Ok so at this stage we have a reasonable outline of a reasonable deductive system for first order logic and set theory. Now, if p is a proposition without any free variable then Ax.p and p are provably equivalent for any variable x (Ax.p -> p is an axiom, while p -> Ax.p is not hard to prove), and if we consider the existence statement Ex.(bot -> bot) as syntactic sugar for ~Ax.~(bot->bot) where ~p is syntactic sugar for p -> bot, then the existence of at least one set is equivalent to [Ax.((bot -> bot) -> bot)] -> bot which is equivalent to ((bot -> bot) -> bot)-> bot which is itself provable. So the existence of at least one set is a logical consequence, not a set theoretic one.

Going back to the comprehension axiom schema, we have:

Aa.Eb.Ax[x in b <-> bot]     (*)

where it is understood that p <-> q is syntactic sugar for (p -> q) /\ (q -> p) while p /\ q is syntactic sugar for ~ (~p \/ ~q) and p \/ q is syntactic sugar for ~p -> q. Since Eb.Ax[x in b <-> bot] has no free variable, it is equivalent to (*) and so we have the theorem: Eb.Ax[~ x in b], i.e. we are able to prove the existence of the empty set solely from the comprehension axiom schema and nothing else (beyond logic).

  • $\begingroup$ I'm not sure if I understand your question. Is the comprehension axiom schema not a set theoretical axiom? How exactly are you assigning semantic meaning to a set without any axioms mentioning sets? Furthermore, you have a rather lengthy description of an axiom schema. I'm not sure what the relevance of an encoding into Haskell of your schema has to this question, could you elaborate on that or simply denote your schema in mathematical notation? Finally, why is proving something equivalent to existence of a set relevant? As there exists a set, anything true is equivalent to that notion! $\endgroup$
    – Discrete lizard
    Commented Mar 10, 2018 at 18:44
  • $\begingroup$ @Discretelizard Yes comprehension is set theoretic. My point is that it is not needed to show Eb.(bot->bot) (there exists a set). My Haskell digressions are only there to give more flesh to the discussion on the deductive system. The 5 axioms schema are in standard notations. Specifying modus ponens and generalization as rule of inference is enough I would think (the only subtlety is you cannot generalize with respect to a variable which is free in a proof hypothesis). if p=Ex.(bot->bot), I am not arguing that ZF|-p but that |-p , i.e. p is provable with no hypothesis (no ZF axiom). $\endgroup$ Commented Mar 10, 2018 at 19:51
  • 1
    $\begingroup$ Axiom (v) has as a special case (Ax.bot) -> bot which would not hold if no value for x existed in the model: in such case the quantification would become vacuously true, which does not imply falsehood. For this reason, in FOL we assume that models are nonempty. If the theory is a set theory, this means that there must be a set. We need separation, then, to build the empty set, as you did. $\endgroup$
    – chi
    Commented Mar 10, 2018 at 21:20
  • $\begingroup$ @chi you point out that (Ax.bot)->bot would not be true in an empty model. Hence a model theorist would exclude the empty set as model, so soundness is preserved. This may be the case, but the question remains whether 'there exists a set' is provable or not. Incidentally, in this case a model would be a set (M,r) with a binary relation r on it. However, in order to interpret a formula (with free variables) in a model, you need an variable assignment map a:V -> M, and if you define validity as being true for all (M,r) and a then M empty still works, since there exists no a:V->M $\endgroup$ Commented Mar 10, 2018 at 22:03
  • 1
    $\begingroup$ Typically $\exists x.\top$ is a theorem of FOL. This follows from chi's statement. $\exists x.P(x)$ is usually defined as $\neg\forall x.\neg P(x)$ and we can prove $\neg P\equiv (P\Rightarrow\bot)$, so $\exists x.\top$ is equivalent to $(\forall x.\bot)\Rightarrow\bot$. Semantically, FOL takes as axiomatic that the domain is non-empty, and if the domain is all sets, then there thus exists a set. But this is a completely artificial addition. Free logics, e.g., don't imply this. It turns on the question of where $y$ is coming from in Axiom (v). $\endgroup$ Commented Mar 10, 2018 at 23:10

1 Answer 1


It seems that you haven't drifted enough to computer science yet: you're still using untyped quantifiers. The crux of your argument is

Ax.p -> p is an axiom

Indeed, that's axiom (v) with a p such that x is not free in p. You can define any axiom you like, but what does this axiom mean? In the case where x is not free in p, combined with the axioms of classical logic, it means that there is at least one set. As chi notes, you can instantiate (v) with p = bot, which gives (Ax.bot) -> bot. By the classical definition of the existential quantifier, this is equivalent to ~(Ax.bot) = Ex.~bot = Ex.True.

If you take the view of a typical mathematical logician, then this axiom is perfectly fine — because mathematical logicians are not interested in empty models!

But if you take the point of view of constructive logic, your axiom is wrong. Not wrong in the sense that it makes the theory inconsistent — after all, it's valid in set theory and set theory isn't inconsistent that we know of — but wrong in the sense that it does not correspond to the proof calculation rule.

Let's write (v) in Coq syntax:

          A : T
(forall x:T. P) -> P[A/x]

Note the premise A : T. This is the axiom for forall elimination, and it requires a value of the type that's quantified over. You can only find such a value in an empty environment if the type is non-empty. In other words, this axiom will only let you prove that there exists a set if the domain of sets is not empty.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.