# Is definable power sufficient to interpret ZFC?

This post is actually related to posting titled What is the strength of definable ZFC?. However the presentation there was 'semiformal', and here I'll present a complete formal exposition of that theory.

To the language of ZFC minus Power, lets add a primitive one place predicate symbol $$definable"$$, and lets add the following Omega inference rule:

if $$\{\phi_1(y),\phi_2(y),\phi_3(y),...\}$$ is the set of ALL formulae in the language of ZFC, in just one free variable symbol $$y"$$; and if $$\psi(X,w_1,..,w_m)$$ is a formula in the language of ZFC, in which all and only symbols $$X,w_1,..,w_m"$$ occur free, then:

$$$$\text{ for each m=0,1,2,...; w_1,..,w_m } \begin{cases} \forall X\ [\forall y (y \in X \leftrightarrow \phi_1(y))\to \psi(X,w_1,..,w_m)]\\ \forall X\ [\forall y (y \in X \leftrightarrow \phi_2(y))\to \psi(X,w_1,..,w_m)]\\ \forall X\ [\forall y (y \in X \leftrightarrow \phi_3(y))\to \psi(X,w_1,..,w_m)]\\ \ . \\ \ . \\ \ . \\ \rule{10,cm}{1,pt} \\ \forall X [definable(X) \to \psi(X,w_1,..,w_m)] \\ \end{cases}$$$$

This is a schema of inference rules whose antecedent is also schema! It means for each particular substitution of $$m$$ and $$w_1,..,w_m$$: if ALL sentences $$\forall X\ [\forall y (y \in X \leftrightarrow \phi_n(y))\to \psi(X,w_1,..,w_m)]"$$, where $$n=1,2,3,...$$; were fulfilled! Then we infer the sentence below the line.

This would ensure that every set $$x$$ that fulfills the predicate "$$definable$$" is a set definable after a parameter free formula in the language of ZFC.

Proof: suppose there exists a set $$s$$ that is not parameter free definable, then take $$m=1$$ and substitute $$w_1$$ by $$s$$, and run the omega rule above for the formula $$\psi(X,w_1)$$ being the formula $$X \neq s$$, the antecedent schema would be fulfilled, and so by that omega rule, we infer that every definable set $$X$$ must satisfy $$X \neq s$$

Add the axiom scheme of definability: if $$\phi(y)$$ is a formula in the langauge of ZFC, in which only the symbol $$y"$$ occurs free, then: $$\forall X\ [\forall y (y \in X \leftrightarrow \phi(y))\to definable(X)]$$; is an axiom

From the above omega rule and the definability axiom scheme, the equivalence of the predicate $$definable$$ with definability after a parameter free formula in the language of ZFC is established!

Now to ZFC minus power, lets add the "definable power set axiom" that is:

$$\forall A \exists x \forall y \ [y \in x \leftrightarrow y \subseteq A \wedge definable(y)]$$

Question: Would that theory still interpret ZFC over the hereditarily definable realm of this theory?

• I imagine Choice would typically fail quite badly. – Eric Wofsey Feb 26 at 23:44
• @EricWofsey, can you elaborate on this point please. – Zuhair Feb 27 at 9:59
• Well, why would Choice be true? I don't know how to construct a counterexample but there is no reason to expect a definable set to have a definable choice function (or more weakly, something definable that behaves like a choice function when restricted to just the definable sets). – Eric Wofsey Feb 27 at 16:03
• @EricWofsey, but why wouldn't the same argument of your's apply to Godel's constructible universe? – Zuhair Feb 28 at 13:47