Is strengthening Foundation in NBG sufficient to make it prove Con(ZFC)?

Question

Can $\sf NBG$ class theory prove the foundation scheme:

Foundation schema: if $\Phi(X)$ is a formula in which "$X$" occurs free and only free, and in which "$Y$" doesn't occur, whose free variables other than "$X$" are among $\vec{P}$, and if $\Phi(X/Y)$ is the formula resulting from replacing every occurrence of "$X$" in $\Phi(X)$ by "$Y$"; then: $$\forall \vec{P} \, \bigl(\exists X \, (\Phi(X)) \to \exists X: \Phi(X) \land \forall Y \, (\Phi(X/Y) \to Y \not \in X)\bigr)$$

This would prove second order transfinite $\in$-induction I suppose.

If $\sf NBG$ cannot prove this schema, then would replacing Foundation axiom of $\sf NBG$ by this scheme makes the resulting theory prove the existence of a model of $\sf ZFC$? Would it be equi-consistent with $\sf MK$?

Answer 1

Joel answered the first question, so here's an answer to the second question.

(Minor point: I would call your schema an induction schema, not a recursion schema. These end up being different in consistency strength---see below.)

NBG + the second-order $\in$-induction schema is weaker than KM in consistency strength. Specifically, KM proves the existence of a transitive model of NBG + second-order $\in$-induction.

The key observation is, KM proves the existence of a transitive model of NBG, and a transitive model will satisfy $\in$-induction for any class of formulae.

In a little more detail: First, note that KM proves the existence of the satisfaction class for $V$ because it's $\Sigma^1_1$-definable. Using that satisfaction class $T$ we can do reflection to get $(V_\alpha, T \cap V_\alpha)$ which is, say, $\Sigma_2$-elementary in $(V, T)$. This is enough elementarity to get that $T \cap V_\alpha$ and $T$ agree on what is true, and so $V_\alpha$ is a transitive model of ZFC.

If $\mathcal X \subseteq \mathcal P(V_\alpha)$ consists of the (parametrically) definable subsets, then $(V_\alpha, \mathcal X)$ will be a model of NBG. (If you axiomatize NBG to include Global Choice, you can arrange to have this by cutting down to $L$. Or you could include a global well-order in the reflection to get one over $V_\alpha$.) And it will satisfy your second-order $\in$-induction schema. This is simply because $\in$ is well-founded, and so induction is valid over $\in$, no matter how complicated a property you want to do induction with.

You can refine this result and notice that all we needed from KM was the existence of a satisfaction class. So much weaker class theories than KM---just $\Sigma^1_1$-Comprehension, or even less---are above NBG + second-order $\in$-induction in consistency strength.

---

On the other hand, if you're talking about the second-order recursion schema, asserting that you can define classes by doing transfinite recursion along $\in$, then that will be equivalent to KM over NBG. This is surely an old observation, but the place I know to see a proof is section 3.5 of my dissertation. (There I formulated it as recursion over any well-founded class relation, not just $\in$, but it's straightforward to see that recursion along $\in$ suffices for the full strength.) Briefly: an instance of Comprehension is a recursion along $1$, and an instance of $\Sigma^1_k$-Recursion has a solution by $\Sigma^1_{k+1}$-Comprehension.

Let me remark that the same phenomenon occurs in second-order arithmetic. For example, arithmetical comprehension plus the full induction schema is weaker in strength than arithmetical recursion. In general induction is weaker than recursion.

Answer 2

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.