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:

\begin{equation} \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} \end{equation}

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?

  • 1
    $\begingroup$ I imagine Choice would typically fail quite badly. $\endgroup$ – Eric Wofsey Feb 26 at 23:44
  • $\begingroup$ @EricWofsey, can you elaborate on this point please. $\endgroup$ – Zuhair Feb 27 at 9:59
  • $\begingroup$ 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). $\endgroup$ – Eric Wofsey Feb 27 at 16:03
  • $\begingroup$ @EricWofsey, but why wouldn't the same argument of your's apply to Godel's constructible universe? $\endgroup$ – Zuhair Feb 28 at 13:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.