Please forgive the fact that what follows these remarks is in ASCII format. I am an amateur; my work shall never be published; and, there is simply no personal benefit to be gained by converting the text into anything else.
To the best that I can ascertain, one cannot even approach question 1 from the standpoint of the first-order paradigm. Whatever the set universe might be, its formulation must satisfy the first-order presupposition of identity criteria without assuming that criteria. This is the case because it must be sufficient to serve as the interpretation of the universal quantifier.
Harry Deutsch discusses the problem of using the first-order paradigm for such purposes
in the link:
http://plato.stanford.edu/entries/identity-relative/#1
Later, when critiquing Geach's arguments, he states exactly the problem that a formulation of the set universe presents. The notion of indiscernibility for the theory must be made to coincide with the notion of identity for the paradigm of first-order logic. According to Deutsch, arguments for language relativity improperly assume that first-order identity defines indiscernibility for a theory.
This analysis is in the section:
http://plato.stanford.edu/entries/identity-relative/#5
To understand the difference, one must discriminate between the referential purport of singular terms and the fact that a system of objects is simultaneously a system of relations between objects. Relative to the purport of singular terms, there are four necessary relations: the full relation, the empty relation, the identity relation, and
the diversity relation.
But, again, this is precisely what cannot be assumed when formulating a theory that includes reference to the set universe. Such reference must be formulated with respect to
some non-reflexive relations.
The sentences which follow attempt such a formulation. I could try to explain them in a variety of ways, but it is unlikely that my explanations would carry the day. By any account they are non-standard.
I have discussed them once before at the link,
Why hasn't mereology succeeded as an alternative to set theory?
That may help somewhat.
The only additional remark I could add is that the primitive relations of this theory are introduced using circular syntax. In "Model Theory", Hodges makes the observation that such definitions are recursive definitions to which model theory has no application. So, with that in mind, interpret them as you see fit.
For what this is worth, established mathematics has no interest in these sentences. And, I am not competent enough to analyze them properly. What I do know, however, is that introducing a term for the set universe is not a simple matter.
We take the consequences of the
following as the basic theory.
It's signature is given by
( (M, |M|), (c, 2), (e, 2) )
with models interpreted coherently
according to
M=V()
in the extended signature
( (M, |M|), (c, 2), (e, 2), (EQ, 2), (=, 2), (V, 0), (null, 0), (set, 1), (S, 1), (P, 1) )
Definition:
AxAy(xcy <-> (Az(ycz -> xcz) /\ Ez(xcz /\ -ycz)))
Provable:
AxAy(xcy -> -ycx)
Provable:
AxAyAz((xcy /\ ycz) -> xcz)
Provable:
Ax(-xcx)
Definition:
AxAy(xey <-> (Az(ycz -> xez) /\ Ez(xez /\ -ycz)))
Definition:
AxAy(xEQy <-> (Az(xcz <-> ycz) /\ Az(zcx <-> zcy) /\ Az(xez <-> yez) /\ Az(zex <-> zey)))
Definition:
AxAy(x=y <-> Az(xez <-> yez))
Assumption:
AxAy(Az(xcz <-> ycz) -> Az(xez <-> yez))
Assumption:
AxAy(Az(zex -> zey) -> Az(ycz -> xcz))
Assumption:
AxEyAz(zey <-> zcx)
Provable:
AxAy(xcy -> Az(zex -> zey))
Provable:
AxAy(Az(ycz -> xcz) -> Az(zex -> zey))
Provable:
AxAy(xcy <-> (Az(zex -> zey) /\ Ez(zey /\ -zex)))
Provable:
AxAy(Az(zex -> zey) -> Az(zcx -> zcy))
Provable:
AxAy(Az(xez -> yez) -> Az(xcz -> ycz))
Provable:
AxAy(xEQy <-> Az(xcz <-> ycz)
Provable:
AxAy(xEQy <-> Az(zex <-> zey))
Provable:
AxAy(xEQy <-> Az(xez <-> yez))
Provable:
AxAy(xEQy <-> x=y)
Assumption:
AxAy((Az(ycz -> xez) /\ Ez(xez /\ -ycz)) -> Az((xez /\ -ycz) -> (Ew(xew /\ wcy) / Aw(zcw -> ycw))))
Assumption:
AxAy((Ez(xcz) /\ Ez(ycz)) -> EwAz(zew -> (z=x / z=y)))
Definition:
Ax(x=V() <-> Ay(-(ycx <-> y=x)))
Assumption:
ExAy(-(ycx <-> y=x))
Assumption:
Ax(Ey(xcy) -> Ey(xey))
Definition:
Ax(set(x) <-> Ey(xcy))
Definition:
Ax(x=null() <-> Ay(-(xcy <-> x=y)))
Assumption:
ExAy(-(xcy <-> x=y))
Assumption:
Ax(Ey(ycx) -> Ey(yex /\ -Ez(zex /\ zey)))
Assumption:
AxEy(Az(zey <-> Ew(wex /\ zew)) /\ (Ez(xcz) -> Ez(ycz)))
Assumption:
AxEy(Az(zey <-> Aw(wex -> zew)) /\ (Ez(zcx) -> Ez(ycz)))
Definition:
AxAy(x=P(y) <-> (Ez(ycz) /\ Az(zex <-> (zcy / z=y))))
Assumption:
Ax(Ey(xcy) -> Ey(Az(zey <-> (zcx / z=x)) /\ Ez(ycz)))
Definition:
AxAy(x=S(y) <-> (Ez(ycz) /\ Az(zex <-> (zey / z=y))))
Assumption:
Ax(Ey(xcy) -> Ey(Az(zey <-> (zex / z=x)) /\ Ez(ycz)))
Assumption:
Ex(Ey(xcy) /\ null()cx /\ Ay(ycx -> Ez(zcx /\ ycz)))
Let the restricted quantifier
Ap[pEQp]
be interpreted as
Ap[pEQp] (phi(p)) <-> Ap(pEQp -> phi(p))
Then for each n and each well-formed formula phi(y, p_0, ..., p_n),
assume
=================
Ap_n[p_nEQp_n]...Ap_0[p_0EQp_0]
AxAy(
Ew(ycw) ->
(Ez((Ew(zcw) /\ (yez <-> (yex /\ phi(y, p_0, ..., p_n))))) <-> Ew(xcw))
)
=================
and assume
=================
Ap_n[p_nEQp_n]...Ap_0[p_0EQp_0]
(
AxAyAz(
(
((Ew(xcw) /\ Ew(ycw)) /\ (phi(x,y, p_0, ..., p_n)) /\
((Ew(xcw) /\ Ew(zcw)) /\ (phi(x,z, p_0, ..., p_n))
) -> (y=z)
)
->
AxAy(
Ew(ycw) ->
(Ez((Ew(zcw) /\ (yez <-> Ew(wex /\ phi(z,w, p_0, ..., p_n))))) <-> Ew(xcw))
)
)
=================