How to prove an extension of ZFC is conservative Working in ZFC.
I've defined a function-like binary predicate $R$ on a proper class. It has to be recursive; i.e. $R(a,b)$ must usually depend on one or more $R(c,d)$ for some $c$s and $d$s calculated from $a$ and $b$. There is, however, no well-founded recursive, unary function that agrees with $R$ (i.e. there is no $F$ such that $y = F(x)$ iff $R(x,y)$).
So I've defined it like ZFC defines $\in$: I've added a new binary predicate symbol $R$ and defined axioms for it. Every axiom conforms to the schema $\forall x_1 . \dots \forall x_n . P_1(x_1) \wedge \dots \wedge P_n(x_n) \rightarrow Q(x_1,\dots,x_n) \rightarrow R(x_1,x_2)$. I think the salient facts are 1) that no axiom concludes that a set exists, only that $R$ relates two sets; and 2) $Q(x_1,\dots,x_n)$ is a formula that usually refers to $R$.
I'd like to prove that ZFC+R proves that no more sets exist than ZFC does. How can I do this?
(Also, is "conservative extension" the right term for this?)
 A: (Slightly editing the comments into an answer.)
You terminology is right: A theory $T$ is a conservative extension of a theory $S$ iff the language of $T$ extends the language of $S$, every axiom of $S$ is provable in $T$, and every theorem of $T$ in the language of $S$ is also a theorem of $S$.
If there is a procedure that allows us to expand any model $(M,\in^M)$ of $\mathsf{ZFC}$ to a model $(M,\in^M,R^M)$ where the relevant axiom schema is satisfied with $R$ interpreted as $R^M$, then yes, the new theory is conservative over $\mathsf{ZFC}$ and does not prove the existence of any new sets. 
The typical example is to have the new axioms state that $R$ is a well-ordering of the whole universe. In $\mathsf{ZFC}$ it is not provable that there is such a class $R$ (recall that in $\mathsf{ZFC}$ all "classes" ought to be definable from parameters). However, using class forcing, one can add to any model of $\mathsf{ZFC}$ a predicate $R$ that is such a global well-ordering, and in a fashion that adds no new sets. 
(Essentially, we force with initial segments.)
The point here is not that we needed to use class forcing, that is just the means towards our actual goal. The point is this: Suppose the theory $T=\mathsf{ZFC}+$"$R$ is a well-ordering" proves a sentence $\phi$ in the language of set theory. Pick any model of $\mathsf{ZFC}$. We can extend it to a model of $T$ in the manner just described. In the extended model, $\phi$ holds. But this means that $\phi$ holds in the original model, because adding $R$ did not add any sets. By the completeness theorem, $\phi$ is provable, because it is true in all models. 
The general approach hinted at by this example is fairly malleable. A different example in the same spirit is that Gödel-Bernays set theory is conservative over $\mathsf{ZF}$. The point is that given a model of $\mathsf{ZF}$, we can extend it to a model of $\mathsf{GB}$ by taking as proper classes of the extension only the definable classes of the original model. But then, exactly the same argument as for the other example shows that we have conservation.
One can be more liberal and have more examples if one does not insist on the restrictions that the definition of conservative extension requires. For example, we could instead have $T$ interpret $S$. Among other things (details in the link), this means that from any model $M$ of $T$ we can define a model $I^M$ of $S$. That the interpretation is conservative would correspond to the requirement that every model of $S$ is $I^M$ for some $M$.
Of course, whether the example you have in mind indeed gives us a conservative extension depends on the details of the schema you have in mind. 
