Classical set theory and the existence of at least one set

Question

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).