Let T be a finite collection of axioms of ZF, let σ be a sentence in the language of ZF and consider the statement
τ: “any transitive countable model of T satisfies σ”.
Then ZFC⊢τ implies ZFC⊢σ, by the classical argument using Reflection, Downward Löwenheim–Skolem and Mostowki’s collapse to get a countable transitive model where finitely many sentences are absolute.
My question is: does ZF⊢τ imply ZF⊢σ? This may look trivial but, without choice, Downward Löwenheim–Skolem can’t be used as above. On the other hand, it could be argued that ZF⊢ “there is a proof of σ from T”, but this does not mean that such a proof can be found in the meta-theory.
Thank you for your help with this (possibly trivial) matter.
@EmilJeřábeksupportsMonica thanks for the observation that ZFC⊢(τ⇒PrZFC(σ)) may be false. I somewhat was considering it be to be true, so that σ could be obtained as mentioned in your first comment, but now I see this is not the way.
– dragoon Nov 14 '19 at 23:34