In posting "How does one define a standard model of ZFC?"
Several answers were given to this question. I would like to know if one uses the following $\omega-$rule and add it to the axioms of ZFC:
$\omega-$rule: if $\{\phi_1(y,w_1,..,w_n), \phi_2(y,w_1,..,w_n), \phi_3(y,w_1,..,w_n)....\}$ is the set of ALL formulas in the first order language of set theory, in which all and only symbols $``y,w_1,..,w_n"$ occur free, and those only occur free, and if $\psi$ is a first order formula in the language of set theory, then if we have:
$ \text{for } i=1,2,3,....; n=0,1,2,3,... \\ \forall w_1,..,w_n \forall x [\forall y (y \in x \leftrightarrow \phi_i(y,w_1,..,w_n)) \to \psi(x)] $,
Then we infer:
$\forall x \psi(x)$.
In English: if every definable set satisfy $\psi$, then all sets satisfy $\psi$.
Question: would all models of the resulting theory be standard models of ZFC?
EDIT: Below I give a negative answer specific to the context of set theory. However, this may give the impression that by replacing ZFC by something else we can change the answer. There is a fundamental obstacle preventing this, however: the Barwise compactness theorem. (Or in this case, its specific instance the Barwise-Kreisel compactness theorem.) The books by Ash/Knight and Barwise each contain good expositions of this theorem and its relatives and applications; if you're coming from a more computability-theoretic perspective, I'd start with Ash/Knight, and otherwise with Barwise.
As the name might suggest, BCT is useful for generating models of theories which "realize unintended structure" - like, in this case, having a descending sequence of ordinals. The twist is that BCT allows us to go beyond first-order logic. Here's the specific instance of BCT we care about here:
(This is the BKCT; the BCT is phrased in terms of an arbitrary countable admissible set $\mathbb{A}$ and corresponding fragments of $\mathcal{L}_{\omega_1\omega}$, with "$\Pi^1_1$" and "$\Delta^1_1$" replaced by the $\mathbb{A}$-analogues of "c.e." and "finite," respectively; BKCT is BCT in the case $\mathbb{A}=L_{\omega_1^{CK}}$.)
The point is that your $\omega$-rule (and all reasonable variations of it) is a computable infinitary sentence. Now a crucial fact from computability theory is that there are computable ill-founded linear orders without hyperarithmetic descending sequences; combined with the BKCT this shows that if $T$ is any computable infinitary first-order set theory with transitive models of height not bounded below $\omega_1^{CK}$, then $T$ has ill-founded models.
The answer - at least under reasonable assumptions - is no, since there are ill-founded pointwise definable models of set theory. Pointwise definable models obviously satisfy your new rule, so they yield counterexamples.
Here's how to argue that there are ill-founded pointwise definable models of ZFC:
Let $\alpha$ be the least ordinal such that $L_\alpha\models$ ZFC. Then $L_\alpha$ satisfies "ZFC is consistent (so has a model) but has no standard model." ZFC proves that if ZFC has a model then it has a pointwise definable model (look at the proof of Theorem 4 in Hamkins/Linetsky/Reitz, and note that it goes through in ZFC alone), so $L_\alpha$ has some $M$ it thinks is a nonstandard pointwise definable model of ZFC.
Now we simply argue that $M$ is in fact a nonstandard pointwise definable model of ZFC (that is, that being a nonstandard pointwise definable model of ZFC is absolute from $L_\alpha$ to $V$). This is a straightforward absoluteness argument (actually, invoking absoluteness here is a bit overkill, but it's fun):
Since ZFC proves the downwards Lowenheim-Skolem theorem and $L_\alpha\models$ ZFC, we may WLOG assume $M$ has domain $\omega$.
Now, for an $\{\in\}$-structure with domain $\omega$, being a pointwise definable model of ZFC is a $\Delta^1_1$ property and being nonstandard (= ill-founded) is a $\Sigma^1_1$ property, so being a nonstandard pointwise definable model of ZFC is a $\Delta^1_1\wedge\Sigma^1_1=\Sigma^1_1$ property.
And those are absolute from $L_\alpha$ to $V$, by Mostowski absoluteness. (Note that we can't use Shoenfield absoluteness here, since $V$ and $L_\alpha$ have different ordinals: $Ord^{L_\alpha}=\alpha\subsetneq Ord$.)