It doesn't directly answer your question, but you may be interested in Florio and Leach-Krouse's recent article in the Review of Symbolic Logic, "What Russell should have said to Burali-Forti".

@FrodeBjørdal if you want to see a standard development along the lines Andreas suggests, have a look at page 74 of Simpson's Subsystems of Second Order Arithmetic.

Concerning (B): this is Shoenfield's completeness theorem (Shoenfield, J. R., 1959, "On a restricted $\omega$-rule", Bulletin de L'Académie Polonaise Des Sciences: Série des sciences mathématiques, astronomiques, et physiques 7:405–407). Shoenfield's original bound was $\omega^\omega$, but this can be improved to $\omega^2$. For details see Franzén, T., 2004, "Transfinite Progressions: A Second Look at Completeness", Bulletin of Symbolic Logic 10(3):367–389.

Peano's existence theorem is nonconstructive, as it is equivalent to weak König's lemma. Details are in §IV.8 of Simpson's Subsystems of Second Order Arithmetic. From that result we can also see that Ascoli's theorem is not required, since that is equivalent to the stronger axiom of arithmetical comprehension.

@JimHefferon plenty of them, e.g. chapter 5 of Rebecca Weber's recent book Computability Theory. More classically, it's used in Hartley Rogers's 1967 book Theory of Recursive Functions and Effective Computability. Google Books should give you page references in both cases.

@usul "This a standard trick -- running all TMs in parallel -- but I don't know if it has a name." This is called dovetailing.

Let $H$ be Con(ZFC)? Or that there exists an $\omega$-model of ZFC, or a well-founded model of ZFC, or... There are a lot of them. The same answers should apply to your second question.

I know at least one person with a PhD in computability theory who now works at Google.

Thanks for such a careful explication of the subtleties, François. When formulating the question I was interpreting satisfaction in the second manner you list, but I should have been more explicit: as you rightly say, one should be careful when stating this theorem and its variants. Thankfully the lemma I am actually using does not rely on the meaning of "satisfies" in this manner (I am happy to state it in detail if that's informative).