FOM: Does Shapiro's ZFC2 need a small cardinal axiom?

[Roger Bishop Jones]

The traditional axiomatisation of ZFC is obtained by adding
replacement to ZC.
I am concerned here with interaction between two "improvements"
to this axiom system.

The naive axiomatisation is redundant in that the empty set, pair
and separation schemas are derivable from the usual formulation
of replacement.

The first innovation is therefore to drop these redundant axioms.
For the sake of relating the discussion to Shapiro we'll keep the
pair axiom.

Innovation 1: drop the empty set axiom and separation schema

For the second innovation we move to a second order formulation
of ZFC.
In this context the usual formulation of replacement involving a
many-one relation can be replaced by one using a function variable.
This eliminates the need to prove the many-one condition.

Innovation 2: adopt a functional formulation of replacement

Either of these two innovations by itself is unproblematic and
leaves the theory unchanged (I guess we have to assume here
that we did the whole thing in second order logic).

However, if we do them both (which Shapiro does in ZFC2)
the empty set becomes elusive.

Though the normal formulation of replacement entails the
existence of the empty set, the functional version does not.
Without the empty set the full separation schema cannot be
derived from functional replacement.

One ought perhaps to be able to get the empty set from
the axiom of foundation.
Every set either is the empty set or is disjoint from one
of its members in which case the empty set is their
intersection.

Unfortunately, intersection is defined using separation,
and functional replacement without an empty set suffices
only to define the intersection of non-disjoint sets.

Does anyone know how to prove the existence of an
empty set in Shapiro's ZFC2?
(as defined in "Foundations without Foundationalism" 6.1 & 4.2)

Roger Jones