Is the following a theorem of $\sf ZF(C)$?


**Countable reflection:** If $\phi$ is a sentence in which $W$ is not free, then:


$\phi \to \exists W: |W|= \omega \land \operatorname {Transitive}(W) \land \phi^W$


Where $\phi^W$ is the sentence obtained by merely bounding all quantifiers in $\phi$ by $ \in W$.


That is: every true sentence is reflected upon a countable transitive set.


So all true sentences are reflected upon some elements of $V\_{\omega\_1}$ (or $V\_{\omega\_2}$ in case of $\sf ZF$).



Does ZF(C) prove countable reflection?
As Monroe Eskew points out in his comment to the question, the positive answer is well-known for ZFC, thanks to the ZF reflection theorem and the Löwenheim-Skolem Theorem (in the form: every model in a countable language has a countable elementary submodel). See, e.g., part (iii) of Theorem 12.14 in Jech's canonical textbook *Set theory, third millenial edition.*


Note that ZFC can be weakened in the above to ZF+ DC (DC = dependent choice) since it is well-known that in the presence of ZF, DC implies (and indeed is equivalent to, see, e.g., [Asaf Karagila's note](https://karagila.org/wp-content/uploads/2012/10/Lowenheim-Skolem-and-Choice.pdf)) the statement that every structure in a countable language has a countable elementary submodel.



> 
> The point of this answer is to point out that even DC can be eliminated from the proof of countable reflection.
> 
> 
> 


**Theorem.** ZF *proves every instance of countable reflection.*


Proof: In light of the fact that the Mostowski collapses can be carried out in ZF, and the constructible universe L satsifies ZFC (and therefore L satisfies "every model in a countable language has a countable elementary submodel), the proof is complete once we note:


$(\*)$ For any set-theoretical sentence $\phi$, if $\phi$ has a transitive model, then the sentence "$\phi$ has a transtive model" holds in the constructible universe L.


The above statement, as far as I know, was first noted in a (famous) paper of Barwise and Fisher entitled "The Shoenfield Absoluteness Lemma" (Israel J. Math. 8 1970, pp.329-339) in which a fine-tuning of the Shoenfield Absoluteness Lemma is presented (in particular, it is shown that the Lemma can be proved without invoking DC).


More specifically, $(\*)$ follows from Theorem 1b (page 336) of the Barwise-Fisher paper, which states that if $\phi$ has a transitive model $A$ with $\rho(A)=\alpha$ (where $\rho$ is the usual ordinal-valued rank function on sets), then there is a transitive model of $\phi$ in the $\kappa^{+}(\alpha)$-th level $L\_{\kappa^{+}(\alpha)}$ of the constructible universe $L$, where $\kappa^{+}(\alpha)$ is the next admissible ordinal after the least admissible ordinal above $\alpha$.


