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$?

  • 2
    $\begingroup$ Nice question. For those who use the two-sorted approach to these theories, you are asking whether GBC proves the second-order $\in$-recursion scheme. $\endgroup$ Mar 29 at 14:45
  • $\begingroup$ @JoelDavidHamkins, Yes, it is about the second order $\in$ -recursion, since I think it would follow from the foundation scheme. $\endgroup$ Mar 29 at 14:59
  • $\begingroup$ Why not? If there is a set $X$ such that $\Phi(X)$, then take the one of least rank. Otherwise there are only classes $X$ such that $\Phi(X)$, so none of them can possess another. $\endgroup$ Mar 29 at 15:46
  • 2
    $\begingroup$ @MonroeEskew you can't necessarily take the set of least rank, if the formula is second-order, since you don't have second-order separation in NBG. $\endgroup$ Mar 29 at 16:30
  • 1
    $\begingroup$ That is, you'd want to take the least-rank instance of the failure of $\Phi(X)$, but you can't form the set of failing instances in which to do this, since you lack second-order separation. $\endgroup$ Mar 29 at 17:18

2 Answers 2


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.

  • $\begingroup$ Yes, I should have been saying induction rather than recursion in all my remarks. $\endgroup$ Mar 29 at 18:37
  • 1
    $\begingroup$ BTW, the proof that $V_\alpha$ is a model of ZFC in your argument is a little more subtle than what you state (as I know you know because we've discussed it), since one needs to argue that the nonstandard instances of ZFC are declared true by the satisfaction class. But one can get that by instances of reflection applied with the class as parameter, just as you mention. $\endgroup$ Mar 29 at 19:21
  • 1
    $\begingroup$ Right, there is a subtlety there about nonstandard models. Thanks for raising it! $\endgroup$ Mar 29 at 19:40
  • $\begingroup$ @KamerynWilliams, the foundation scheme given here would prove second order $\in$-recursion, right? So, this means this theory is equi-consistent with MK. $\endgroup$ Mar 29 at 19:50
  • $\begingroup$ @ZuhairAl-Johar Maybe I'm misreading your formula, but I don't see it. Could you sketch your argument? $\endgroup$ Mar 29 at 20:08

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.