Theorems in MK would imply theorems in ZFC

90 Views Asked by At

Will theorems of MK, which has formulas which wff in ZFC also, be theorems in ZFC.

What about same for theroems of NBG for implying about theorems of ZFC?

And what will be accurate statement, if any, for saying about relationship between theorems of NBG and theorems of MK?

1

There are 1 best solutions below

15
On BEST ANSWER

When comparing ZFC with NBG or MK, you are asking about is (the lack of) conservativity. The following are well-known, and can be found at the relevant wikipedia page:

  • NBG is conservative over ZFC: if $\varphi$ is a sentence in the language of NBG with all quantifiers ranging over sets only which is provable from NBG, then $\varphi$ is provable in ZFC. Meanwhile, MK is not: MK proves the consistency of ZFC. (Note that this also means that there are theorems of MK which are not theorems of ZFC.)

  • Actually, the previous bullet point is technically sometimes false. We have to be careful here: usually$^*$ NBG is written in the same language as ZFC, and the set/class distinction is a definable one (a set is a class which is an element of some class). This leads to failures of conservativity: e.g. NBG proves "$\exists x\forall y(x\not\in y)$" (that is, there is a proper class) whereas obviously ZFC proves the opposite. The "right" way to formalize class theories like NBG or MK here is via sorts: have a sort for sets and a sort for classes. So e.g. NBG proves $\forall x^{set}\exists y^{set}(x\in y)$, and the same sentence - when we drop the set sort, since no sorts exist in the language of ZFC - is provable in ZFC.

  • If we work without sorts, then we need an appropriate translation from one language to another. For a sentence $\varphi$ in the language of set theory, let $\hat{\varphi}$ be the sentence gotten by inductively replacing every "$\exists x(\psi)$" and "$\forall x(\psi)$" in $\varphi$ with "$\exists x((\exists y(x\in y))\wedge\psi)$" and "$\forall x((\exists y(x\in y))\implies \psi)$" respectively where $y$ is a variable not used in $\varphi$ (this is an instance of a more general process called relativizing the quantifiers); then for all $\varphi$, we have ZFC proves $\varphi$ iff NBG proves $\hat{\varphi}$.


$^*$Historical note: actually, Bernays originally formulated NBG using sorts. Godel replaced the sorts with (equivalent) unary predicates (sorts are only meaningfully different from predicate symbols when we have infinitely many of them). The "same language" approach, as far as I know, was first used by Mendelson.