**The answer to the first question is no.** If ZFC is consistent, then NBG does not prove the second-order $\in$-induction scheme.

To see this, take an $\omega$-nonstandard model of NBG, with only the parametrically definable classes. For each standard $n$, there is a class $\Sigma_n$ truth predicate for first-order $\Sigma_n$ truth, since we can easily write down a definition for it. Furthermore, for a class to be a $\Sigma_n$-truth predicate is a first-order expressible property about that class, uniform in $n$, since one need only assert that it fulfills the Tarski recursion for formulas of that complexity. Meanwhile, there can be no definable truth predicate for nonstandard $\Sigma_n$ truth, by the usual proof of Tarski's theorem.

So there can be no least $n$ for which there is a $\Sigma_n$-truth predicate, and this violates second-order $\in$-induction.

**Second-order $\in$-induction implies Con(ZFC) and much more.** We can turn the previous argument into a proof that the second-order $\in$-induction scheme implies Con(ZFC) as follows. By induction, we have observed that there is for every $n$ (including nonstandard $n$ if any) a truth predicate for first-order $\Sigma_n$ truth. Furthermore, one can show that these predicates are unique for each $n$.

If we have second-order $\in$-recursion, instead merely induction, as explained by Kameryn's answer, then we would be able to assemble the partial truth predicates into a full satisfaction class. But that is not always possible, since as Kameryn explains, having a satisfaction class implies the consistency of the second-order $\in$-induction scheme, contrary to the incompleteness theorem.

Nevertheless, we can get Con(ZFC) just from having $\Sigma_n$ truth predicates for every $n$. To see this, observe first by a standard trick that the truth predicates will include not just the standard instances of ZFC axioms, but also all nonstandard instances. One can see this by applying the replacement axiom in the language with the partial truth predicate to find a large enough $V_\alpha$ covering the desired witnesses.

Now, if our model thought there was a proof of a contradiction in ZFC, then this proof would have assertions bounded in complexity by some (possibly nonstandard) $n$, and so the axioms would all be declared true by the $\Sigma_n$ truth predicate, which is also closed under modus ponens, but never asserts any contradiction as true. So there can be no proof of a contradiction.

Having established that the model thinks Con(ZFC), we can by the same reasoning get Con(ZFC+Con(ZFC)) and so on with further iterates, just by doing the same argument again with the extra hypotheses.

4more comments