# How to prove an extension of ZFC is conservative

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?

-
Neil, Why don't you list the specific axioms you have in mind? The answer will depend on your axioms. –  Andres Caicedo Apr 14 '11 at 20:21
@Andres: There are 14 of them, and they depend on 11 predicates. I couldn't in good conscience ask anyone here to read through all that. :) And because there are so many, it would save me a lot of trouble if I could prove it just on their lexical structure. In my searches about this, I've seen terms like "downward absoluteness" that suggest I can do that. Thanks for your help so far, by the way. –  Neil Toronto Apr 14 '11 at 21:33

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).

-
Darned good point. With the axioms, I'm doing something that is usually done by specifying a family of judgments, and taking a least fixed point to uniquely define the relation. I forgot that last part, so I'll update the question with it. –  Neil Toronto Apr 14 '11 at 21:13
Correction: I'm doing something that is usually done by specifying a family of inference rules. –  Neil Toronto Apr 14 '11 at 22:04
$R$ occurs only positively in $Q$, so it's good. (Thanks for that.) Interesting point about the axiom schemas; yes, I'll need them extended. Now, what if, instead of a fixpoint axiom, I added a weaker axiom, such as that $R$ is deterministic? E.g. $\forall x,y,z . R(x,y) \wedge R(x,z) \implies y=z$? –  Neil Toronto Apr 15 '11 at 16:14
Also, can you check my intuition? Suppose I want to construct a unique function $f : D \rightarrow D$, with $D$ countable and consisting of finite sets, from a non-well-founded recursive definition. (This comes up in computer science all the time.) I need sets to exist that are larger than any $f$ operates on: $f$'s domain, a bounding set for a fixed point or $\Nat$ to construct increasing $f_n$, etc. Similarly, if I want to construct a unique relation like $R$ on all sets, I'll probably need bigger sets, analogous to those necessary to define $f$. Is that right? –  Neil Toronto Apr 15 '11 at 17:27
If you add "$R$ is deterministic" instead of fixpoint axioms, then again you get conservativity trivially because you can interpret $R$ as always false. Therefore, I again suspect that you really want something else along with determinism, perhaps some part of the fixpoint requirements? –  Andreas Blass Apr 15 '11 at 19:06