How to prove an extension of ZFC is conservative

Question

I asked this question on math.stackexchange.com and got some great comments from Andres Caicedo, but no answers. His comments pointed me toward class forcing, but that's way out of my field. I'm basically an infant in advanced set theory and model theory - I'm a computer scientist that loves logic and set theory - but it seems to me that there should be an easier way.

The original problem starts this way: I would like to define a unary, recursive function $F$ on a proper class. But the recursion is necessarily not well-founded, so I can't.

Instead, I've introduced a new primitive binary relation $R$, and stated a family of defining axioms. All but one would correspond with rules defining $F$, if I could define $F$, and these can be written in the form

$$\forall x_1, x_2, \dots, x_n. Q(x_1,x_2,\dots,x_n) \implies R(x_1,x_2)$$

where $Q$ is an axiom-specific condition that usually refers to $R$. I'm not sure how to formulate the last axiom at the class level. It's that $R$ is the intersection of all relations that satisfy the previous axioms.

Here's my original problem: I'm unsure whether this extension of ZFC is conservative. Does it prove the existence of any new sets?

Andres suggested class forcing. The strategy would be: if $R$ is defined without parameters and is a partial order (I can easily make it so), I could possibly prove it is tame; it therefore preserves ZFC; QED. But proving tameness is beyond my abilities right now, and I have a hard time justifying the time I would spend learning how. I haven't a clue whether $R$ is tame, anyway.

The axioms have a simple, regular form that it seems I should be able to exploit to more easily prove the extension is conservative. In particular, all but the last one have these properties:

1. None of them conclude or assert that a set exists.
2. Every $Q(x_1,x_2,\dots,x_n)$ is a $\Delta_0$ sentence.
3. Therefore, every axiom is a $\Pi_1$ sentence.

Using these properties, can I prove the extension is conservative?

Answer 1

If all the axioms are indeed of the indicated form, then they'd be satisfied if you interpret $R$ as the universally true relation. Of course, that makes your axioms conservative. But I conjecture that what it really shows is that you have, at least implicitly, some additional axioms in mind that are not of the indicated form and cannot be satisfied by interpreting $R$ as always true.

EDIT, after the question was clarified: So your intent is to add to ZFC a new relation symbol $R$ intended to denote the smallest (possibly class-sized) relation satisfying the indicated implications. (You probably also want to assume that $R$ occurs only positively in the $Q$ formulas; otherwise there's no guarantee that those implications will be satisfied by the intersection of all the $R$'s that satisfy them, or that there will be a smallest solution.)

My immediate reaction is that this sort of inductive definition would enable you to define a truth predicate (or more precisely a satisfaction predicate) for the language of ZFC and thereby prove the consistency of ZFC. If that's correct, then of course you have a non-conservative extension of ZFC.

Another EDIT to correct the preceding paragraph: I still think this sort of inductive definition will provide a truth definition for the language of ZFC, but in order to use this to prove the consistency of ZFC you'd need to extend the replacement (or at least separation) schema of ZFC to apply to formulas containing the newly introduced relation. Some people regard this as automatic --- when you extend the language, you automatically extend axiom schemas to allow the new symbols. Furthermore, I think you'll probably want this extension, because without it you won't be able to do much with your new, inductively defined relations. Nevertheless, it's worth noting that this extension of an axiom schema is a genuine extension in the sense of producing new axioms. I would expect that, if you don't extend any axiom schema to allow the new relation symbols, then you would have a conservative extension, simply because any model of the original theory can be extended to interpret the new relation symbols as the appropriate least fixed points (as calculated in the given model).