Are there fragments of set theory which are axiomatized with only bounded (restricted) quantifiers used in axioms? Bounded quantifiers in set theory are represented as $(\forall x \in S)$ or $(\exists x \in S)$. But since the modifier "bounded" brings up an association with  "bounded variable", I prefer the term "restricted quantifier" used in Kit Fine. Relatively unrestricted quantification where "four broad grounds upon which the intelligibility of quantification over absolutely everything has been questioned". 
My view upon the axiomatization of a theory of multiverses is that a multiverse is a multitude of universes (like Grothendieck universes or the von Neumann universe), and restricted quantifiers are needed to quantify the variables running within each universe, while the unrestricted quantifiers are needed to quantify the variables running within this multitude.  But the last ones can be presented as quantifiers restricted by the "multitude" which can be treated as a universe (of universes). Thus, to my mind, this area of research must strongly employ restricted quantifiers. 
This is a wide area of research, but my questions refer to a more restricted area:


*

*Are there results on axiomatizing with restricted quantifiers only, in concrete set theories - ZF, NGB, NF (New Foundations), NFU (New Foundations with urelements) or other?

*Is there any correlation between decidability of a fragment of set theory and restricted quantification?


The question 2 is motivated by the link
http://en.wikipedia.org/wiki/Decidable_sublanguages_of_set_theory 
which refers to a link about a result which sounds to me strange:  
http://turing.dipmat.unict.it/~cantone/p40-97/restrQuant.ps.gz
but this last link does not work for me, so that I can check what the author meant.
 A: There are a few things to say.
First, as Goldstern notes in the comments, there are strictly
speaking no sentences in the language of set theory having only
bounded quantifiers (a sentence is a well-formed formula having no
free variables), since the bound $y$ in the outermost bounded
quantifier $\exists x\in y$ in any assertion will itself be a free
variable in the assertion. That is, you just can't even form a sentence in the language of set theory at all using only bounded quantifiers, since if there are any quantifiers, then there will be at least one free variable (and if there are no quantifiers, there will also be a free variable). Since an axiomatization of a theory is
customarily understood to consist of sentences, we therefore
will find no axiomatization purely in the language of set theory
consisting of assertions in which all quantifiers are bounded.
(This was why he mentioned having constants in the language, which
could serve as bounds and thereby enable one to form sentences
with only bounded quantifiers.)
Second, it seems to me that the interest in bounded quantifiers is
related to an interest in restricting the complexity of the
assertions appearing in an axiomatization (of ZF, GB or whatever).
But in this case, the answer is that there is no such
axiomatization. Specifically, it is an immediate consequence of
the Lévy–Montague
reflection theorem that ZF proves
the consistency of any $\Sigma_n$ fragment of ZFC, and so if ZF is
consistent, then any axiomatization of ZF must use formulas of
unbounded complexity.
So if the theory is consistent, there can be no axiomatization of
ZF or ZFC that consists of sentences having some bounded level of
complexity.
A: One sentence in your questions suggests that you want to have a "restricted quantifier over the variables in one universe". Here is one (rather silly) way to do it. 
The following is a theory ZFU which is very closely related to ZF; all axioms of ZFU use bounded quantification only. 
The language of ZFU uses equality, the binary relation $\in$, and a constant symbol $U$.  For each formula $\varphi$ in the language of ZF let $\varphi^U$ be the formula obtained by bounding all quantifiers with $U$ (i.e., replacing $\forall x$ by $\forall x\in U$, similarly for $\exists$).   Let ZFU be the set of all axioms $\varphi^U$, with $\varphi$ an axiom of ZF. (Note that the U-version of the foundation axiom implies $U\notin U$.) For clarity it might be better to also add the requirement that elements of elements of $U$ are again elements of $U$. 
The model-theoretic relation between ZF and ZFU is the following: 


*

*For any model $\mathcal M=(M,E,U)$ of ZFU,   let $V_{\mathcal M}:=\{m\in M: (m,U)\in E\}$. Then $(V,E\upharpoonright V)$ is a model of ZF. 

*Conversely, let $(V,e)$ be a model of ZF. Let $U\notin V$, and let $M$ be any superset of $V\cup \{U\}$. Let $E$ be any relation on $M$ satisfying $E\upharpoonright V=e$ and $M=\{x\in V: (x,U)\in E\}$.  Then $\mathcal M=(M,E,U)$ is a model of ZFU, and $V$ can be obtained from $\mathcal M$ as above. 


This means that in some sense ZFU is a conservative extension of ZF.
