Return to Answer

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.

We can turn this argument into a proof that the second-order $\in$-recursion 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.

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.

If ZFC is consistent, then NBG does not prove the second-order $\in$-recursion 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$-recursion.

We can turn this argument into a proof that the second-order $\in$-recursion scheme implies that there is a truth predicate for first-order truth. There is such a predicate for $\Sigma_0$ truth, and from any such $\Sigma_n$ truth predicate we can define a $\Sigma_{n+1}$-truth predicate. These are unique when they exist and cohere into a full truth predicate for first-order truth.

This implies $\text{Con}(\text{ZFC})$ and much more, since indeed it implies that the universe $V$ is the union of an elementary chain of $V_\alpha$s, each of which will be a transitive model of ZFC.

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.

We can turn this argument into a proof that the second-order $\in$-recursion 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.

If ZFC is consistent, then NBG does not prove the second-order $\in$-recursion 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 a class to be a $\Sigma_n$-truth predicate is a first-order expressible property about that class, since one need only assert that it fulfills the Tarski recursion. 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$-recursion.

We can turn this argument into a proof that the second-order $\in$-recursion scheme implies that there is a truth predicate for first-order truth. There is such a predicate for $\Sigma_0$ truth, and from any such $\Sigma_n$ truth predicate we can define a $\Sigma_{n+1}$-truth predicate. These are unique when they exist and cohere into a full truth predicate for first-order truth.

This implies $\text{Con}(\text{ZFC})$ and much more, since indeed it implies that the universe $V$ is the union of an elementary chain of $V_\alpha$s, each of which will be a transitive model of ZFC.

If ZFC is consistent, then NBG does not prove the second-order $\in$-recursion 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$-recursion.

We can turn this argument into a proof that the second-order $\in$-recursion scheme implies that there is a truth predicate for first-order truth. There is such a predicate for $\Sigma_0$ truth, and from any such $\Sigma_n$ truth predicate we can define a $\Sigma_{n+1}$-truth predicate. These are unique when they exist and cohere into a full truth predicate for first-order truth.

This implies $\text{Con}(\text{ZFC})$ and much more, since indeed it implies that the universe $V$ is the union of an elementary chain of $V_\alpha$s, each of which will be a transitive model of ZFC.