1

Suppose we have extended $ZF$ by adding to $ZF$ an unary function symbol $arb$ (an arbitrary element of a set) and a corresponding axiom "For every non-empty set $S$, $arb(S)$ is in $S$". Will be the resulting theory a conservative extension of $ZF$?

flag
It seems to me that the answer is an obvious yes, given a proof there are only finitely many instances of $arb$ in the formulas and you can just replace each instance with the "mini-proof" that $S\neq\varnothing$ therefore we can fix some $s\in S$. This happens finitely many times so we're good without appealing to the axiom of choice. – Asaf Karagila Jan 20 at 14:05
@Asaf Surely not. Using replacement, I can (uniformly!) construct a choice function for every family of non-empty sets, so in particular this theory proves the axiom of choice! – Zhen Lin Jan 20 at 15:21
@Zhen Lin, oh yeah. It seems like you can easily get global choice from this simply take $\lbrace(x,arb(x))\mid x\neq\varnothing\rbrace$. I was thinking in terms of a "dynamic oracle" so to speak... :-) – Asaf Karagila Jan 20 at 15:37

1 Answer

8

It depends how the remaining axioms of ZF are altered (or not). For example, do we broaden the scheme of replacement to apply to formulas of set theory which contain the symbol "$arb$"? If so, then as Zhen Lin says the resulting theory proves the axiom of choice: given a collection of sets $\mathcal{A}=\lbrace A_i: i\in I\rbrace$, applying replacement to the formula "$x=arb(S)$" as $S$ ranges over the elements of $\mathcal{A}$ yields a choice function. If we don't do this - that is, if we have replacement and separation only for sentences of the language of set theory without "$arb$" - then we do in fact get a conservative extension: given any model $\mathcal{M}$ of ZF, let $arb$ pick any element from each element of $\mathcal{M}$ (I guess I'm using Choice in the ambient universe to do this, but if all we care about is not proving any new theorems, then this can be gotten rid of by Shoenfield absoluteness); the resulting extension is a model of ZF with $arb$.

link|flag
Well pointed on the delicate reasoning about the replacement schema. Why doesn't the "algorithm" I suggested in my first comment work on a syntactical level, which would then rid of the need for choice in the meta-theory? – Asaf Karagila Jan 20 at 15:48
1 
 There are only finitely many explicit instances of $arb$ in any proof; but there may be one "mass-instance" of $arb$ being applied to every member of a set of sets, via Replacement. The second step of your algorithm involves replacing each actual instance of $arb$ by a specific choice, which does work if there are only finitely many $arb$s, but fails if we have a mass instance of $arb$. (Wow, that didn't come out nearly as clearly as it sounded in my head. :p ) – Noah S Jan 20 at 16:31
Well, sure if we modify the replacement schema. But what if we keep replacement as in the original ZF? – Asaf Karagila Jan 20 at 17:09
Hm, I think what Noah is saying is that even inside one sentence, we may end up evaluating $\textrm{arb}(x)$ for infinitely many $x$. (For example, $\forall x . (\exists y \in x) \to \textrm{arb}(x) \in x$.) – Zhen Lin Jan 20 at 20:41
Zhen Lin, yes. But this is hardly enough to give a choice function. – Asaf Karagila Jan 20 at 22:12
show 11 more comments

Your Answer

Get an OpenID
or

Not the answer you're looking for? Browse other questions tagged or ask your own question.