set existence question I'm sure this is basic but here goes.
Let $\sigma_1 (x), \sigma_2 (x), ...$ be a (computable) enumeration of the formulae in the language of set theory with one free variable.
For each $i$, let $S_i$ be the set of reals $r$ such that $\sigma_i (r)$. 
Do the axioms of set theory guarantee the existence of the set of ordered pairs of the form $\langle  i, S_i \rangle$ - that is, do the axioms of set theory guarantee the existence of the set $\lbrace \langle  1, S_1 \rangle, \langle  2, S_2 \rangle, ... \rbrace $, or does the undefinability of truth get in the way here?
 A: Let $F$ denote the function $\lbrace (i,S_i) : i < \omega \rbrace$ in whatever sense it may exist---I hope this abuse of notation will not be confusing.
The undefinability of truth does "get in the way" in the sense that it shows that there cannot be such a function $F$ that is definable.
If we let $C$ be the set of $i$ such that $\sigma_i$ is a sentence ($x$ does not appear) then from $F$ we could define $\lbrace i \in C : S_i  = \mathbb{R}\rbrace$, which is essentially a truth set and therefore cannot be definable by Tarski's theorem.
EDIT: it looks like I am using "definable" to mean "definable without parameters" and Joel is using it to mean "definable with parameters."  As Joel points out in the comments and in his answer, it is possible for a truth set, and indeed the desired function $F$, to be definable from ordinal parameters.
To answer the precise question you stated, ZFC does not prove the existence of such a function $F$.  As Andreas mentions in the comments to Bjørn's answer, there are models of ZFC in which all sets are definable. (This is not a first-order property of the model.) Any such model $M$ cannot satisfy "the desired function exists" regardless of how we try to formalize this.  One way to see this is that if there were such a function $F \in M$, then externally we could use the fact that every set in $M$ is definable in $M$ to show that $ran(F) = \mathcal{P}(\mathbb{R})^M$.  This statement about the range is absolute to $M$, contradicting Cantor's theorem in $M$.
A: As has been mentioned in the comments, there are models of ZFC in which each real number is definable without parameters (see my answer to Is analysis in fact the analysis of definable real numbers? and also my article Pointwise definable models of set theory with Reitz and Linetsky for a discussion). In a pointwise definable model, there can be no list of all the definable sets of reals, paired with their definitions, since all the definable singletons would appear on such a list and reveal that the reals are countable, contrary to ZFC.
Meanwhile, there are various ways to achieve the list of definable sets if one has a stronger background set theory, and this is much more detail about this in our article. Here are a few quick instances:


*

*If the scheme known as $V_\delta\prec V$ holds, asserting that $V_\delta$ is an elementary substructure of $V$, then we may form the list of definable sets of reals, simply by using the Tarskian definition of truth in the structure $\langle V_\delta,{\in}\rangle$. This is definable in $V$, but by the assumption of $V_\delta\prec V$, it happens to coincide with truth in $V$. The theory $V_\delta\prec V$ is equiconsistent with ZFC by a simple compactness argument.

*If one has Kelly-Morse set theory KM in $V$, then one may define a truth predicate for first-order assertions in the language of set theory, and thereby may form the desired seqeunce of definable sets. 
