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
Best Answer
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.