Lets take the intersection of the theory of $L_{\omega_1^{CK}}$ and $\sf ZF + [V=L]$, this is equivalent to the theory of constructability from below + limit stages.

Can this theory prove the following definability $\omega$-rule?

$\textbf{Definability: }$ if $\phi_1,\phi_2, \phi_3,...$ are all formulas in which only symbol "$y$" occurs free, and "$y$" never occur bound, and that doesn't use the symbol "$x$", and $\psi$ is a formula in which only symbol "$x$" occurs free, and "$x$" never occur bound; then:

$\underline {[i=1,2,3,...; \\ \forall x \, (x=\{y \mid \phi_i\} \to \psi)]} \\ \forall x: \psi$

In English: if a parameter free formula holds for all parameter free definable sets, then it holds for all sets.

In other words, are all models of this theory pointwise definable models?

The context is generally related to having an extremely concrete kind of sets, and so it is in continuation to the context of this posting; and also to the hyperarithmetical hierarchy


1 Answer 1


There are two issues with your question.

First, your statement "in other words" is not correct, since there are theories whose models have the property that whenever a statement holds of every parameter-free definable element, then it holds of every element, but not all models are pointwise definable.

Theorem. In any model of ZFC+V=HOD, if a property $\psi$ holds of every parameter-free definable element, then it holds of every element.

Proof. This theory has a parameter-free definable well ordering of the universe. So if there is a counterexample to any statement $\psi$, then there is a definable counterexample, since there will be one that is least with respect to the well ordering. $\Box$

But not every model of ZFC+V=HOD is pointwise definable, since this is a first-order theory which, if consistent, has uncountable models, which cannot be pointwise definable.

What your inference rule is expressing is not that the models should be pointwise definable, but rather, that the definable elements form an elementary substructure of the universe. This is true whenever there is a definable global well-ordering or more generally whenever there are definable Skolem functions, since the class of definable elements will be closed under the Skolem functions and therefore constitute an elementary substructure.

What is more, I claim that your deduction rule is simply equivalent in models of ZFC (and also weaker theories) to the axiom V=HOD. The reason is that if a model has V=HOD, then it has a parameter-free definable well-ordering and hence definable Skolem functions, which makes the definable elements an elementary substructure. Conversely, if your rule is valid for a particular theory extending ZFC, then the models of that theory will have their definable elements forming an elementary substructure (by the Tarski-Vaught test). So the definitions will still work inside the substructure, where everything is definable, and so that will be a model of V=HOD, since you don't even need the ordinal parameters. So the original model also has V=HOD. In conclusion, your deduction rule is equivalent over ZFC to the set-theoretic axiom V=HOD.

This brings us to the second point. There can be no first-order theory with infinite models but only pointwise definable models. The upward Löwenheim-Skolem theorem shows that every consistent theory with infinite models has models of arbitrarily large cardinality. Once the model is larger than the number of definitions, it cannot be pointwise definable.

  • 1
    $\begingroup$ Your theory includes V=L, which implies that there is a definable well-ordering, and so yes, the theory proves the rule, because for every statement, if it has a counterexample, it has a definable counterexample. $\endgroup$ Jun 3 at 11:46
  • 1
    $\begingroup$ That really changed my mind about matters. So ZF + V=HOD actually proves that all sets are parameter free definable, since it has a definable well ordering over the universe. Before, I used to think that this cannot be captured. Thanks $\endgroup$ Jun 3 at 12:04
  • 3
    $\begingroup$ @ZuhairAl-Johar Contrary to your last comment, Joel already explained that ZF + V=HOD does not prove that all sets are parameter-free definable. $\endgroup$ Jun 3 at 13:28
  • 3
    $\begingroup$ That's right, it proves the inference rule you mention, but it doesn't prove that every object is definable. Those are not the same, for the reasons I explain in the first half of my answer. $\endgroup$ Jun 3 at 14:51
  • 1
    $\begingroup$ @JoelDavidHamkins, Yes, for my part and for this case I do admit technical failure in capturing the intentions behind developing this method, yet it is not a failure on the intuitive side. Also, you have proved a nice result by equating this deduction rule with the single set theoretic axiom V=HOD, which at least to me is a very nice technical result, though short of my intended goals. Thanks a lot! $\endgroup$ Jun 5 at 11:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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