Logic and set theory using only uniquely defined items In Prenex form, a set theoretic sentence can be written $\forall \exists \forall \exists ...\forall \exists \psi$ where $\psi$ has no quantifiers. Now, consider all formulas of the more restrictive form $\forall \exists! \forall \exists! (...)$ (recall that $\exists!$ means "there is a unique"). I call those "constructive" because $\forall x \exists ! y \phi(x,y)$ can be viewed as expressing the
existence of a "function" $f$ such that $y=f(x)$ is the only solution to $\phi(x,y)$.
Several axioms or axiom schemes of ZFC are naturally "constructive" in this sense, such as replacement, power set, union, while others like foundation and choice are not.
Is it known whether the non-constructive axioms can be replaced with constructive ones,
while keeping a theory that's equiconsistent with ZFC ?
  A related question : if a theory knows the truth value of any constructive sentence, must it necessarily be complete ?
 A: It's not obvious most axioms of ZFC are constructive in this sense, e.g. the replacement schema has many sentences involving $\phi$ with non-constructive existential quantifiers. The only axioms that seem to have obvious constructive statements are pairing and extensionality. Still, I think it's plausible that ZFC+V=L can be axiomatized using only constructive sentences. I'll sketch out a possible approach:
Start with extensionality and pairing. Define $``x \neq \emptyset"$ by $\exists! b \forall a(a \not \in b \wedge b \neq x)$ (taken from Dap's answer).
Define $x \not \subset y$ by $\exists! z(\forall a (a \in z \leftrightarrow (a \in x \wedge a \not \in y))\wedge z \neq \emptyset).$
Define $\alpha \in Ord$ by $\forall \beta \in \alpha (\forall \gamma \in \beta (\gamma \in \alpha)) \wedge \forall S(S \not \subset \alpha \vee S=\emptyset \vee \exists!\beta \in S(\forall \gamma \in S(\beta = \gamma \vee \beta \in \gamma))).$
I think the basic theory of ordinals (and functions on them) should be constructively axiomatizable. We should be able to state $V=L$ using the auxillary Jensen hierarchy $S_{\alpha}$ (which is rather convoluted to define, see Schindler's text book). In particular, we should be able to constructively define the notion of an "$S$-sequence," i.e. a transfinite sequence of the form $\langle (S_{\alpha}, <_{\alpha}): \alpha<\beta \rangle,$ where $<_{\alpha}$ is the canonical well-order on each $S_{\alpha}.$ We need to construct the well-order simultaneously because the definition of successive $S_{\alpha}$'s uses the notion of union, and I think we need to use the well-order to constructively define the union of a set.
Now we can state $V=L$ as the statement that for each $x,$ there is a unique $S$-sequence whose final $S_{\alpha}$ is the first to have $x$ as an element. Now we can constructively state the other axioms of ZFC by noting $\exists \phi(x)$ is equivalent to there existing a unique $<_L$-minimal $x$ satisfying $\phi.$
Addendum: Here's a possible counterexample to the suggestion that a theory deciding all constructive sentences is necessarily complete. Define a poset $(P,<)=(\mathbb{Z} \cup \{\infty, \infty'\},<),$ where $<|_{\mathbb{Z}}$ is the standard order and $\infty$ and $\infty'$ are both maximal elements. 
Consider two models in the language of a single binary predicate $<,$ namely $(M_1,<), (M_2,<),$ where $M_1=\mathbb{N} \times P$ and $M_2=M_1 \cup (\{-1\} \times \mathbb{Z}).$ In each, we define $(a,b)<(c,d)$ iff $a=c$ and $b<d.$ I strongly suspect $(M_1,<)$ and $(M_2,<)$ have the same constructive truths, but are clearly not elementary equivalent.
