3

$\sf ZFC + Classes$ is a bi-sorted theory with lower cases standing for sets and upper cases for Classes; axioms include all $\sf ZFC - Extensionality$ axioms written in lower case, and the following axioms on top of bi-sorted ID-theory $^\dagger$:

Sorting: $\forall x \exists Y: x=Y$

Membership: $\forall X \ ( \exists Y( X \in Y) \leftrightarrow \exists z( z=X))$

Extensionality: $\forall X \forall Y (\forall z (z \in X \leftrightarrow z \in Y) \to X=Y)$

Comprehension: if $\phi(y)$ is a formula not using symbol $``X"$, and in which $y$ occur, with parameters (free variables other than $y$) among $\vec{A}$, then: $$\forall \vec{A} \, (\exists X \, \forall y \, (y \in X \leftrightarrow \phi(y)))$$

Define: $X=\{y \mid \phi\} \iff \forall y \, (y \in X \leftrightarrow \phi)$

Define: $\operatorname {set}(X) \iff \exists y: y=X$

Define: $\operatorname {proper class} (X) \iff \neg \operatorname {set}(X)$

Now $\sf ZFC + Classes$ is a conservative extension of $\sf ZFC$. However, it differs from $\sf NBG$ in that the class comprehension schema is impredicative, i.e., like $\sf MK$, it allows quantification over class variables. Also, it differs in that it doesn't prove global choice.

Is $\sf ZFC + Classes$ finitely axiomatizable?

$^\dagger$ bi-sorted ID theory is the extension of the logical axioms of bi-sorted $\sf FOL$ with the following axioms:

Reflexivity. $\forall x: x = x \\ \forall X: X=X$

Substitution for functions. For all variables $x,X,y,Y$ and any function symbol $f$:$$x = y \to f(..., x, ...) = f(..., y, ...) \\ x = Y \to f(..., x, ...) = f(..., Y, ...) \\ X = Y \to f(..., X, ...) = f(..., Y, ...)$$ Substitution for formulas. For any variables $x,X,y,Y$ and any formulas $\phi(x), \phi(X)$, if $\phi(x | y), \phi(x|Y) $ are formulas obtained by replacing any number of free occurrences of $x$ in $\phi(x)$ with $y,Y$ respectively, such that these remain free occurrences of $y,Y$ respectively; and if $\phi(X|y), \phi(X|Y)$ are obtained by replacing any number of free occurrences of $X$ in $\phi(X)$ with $y,Y$ respectively, such that these remain free occurrences of $y,Y$ respectively, then $$x = y \to (\phi(x) \to \phi(x|y)) \\x = Y \to (\phi(x) \to \phi(x|Y)) \\X = y \to (\phi(X) \to \phi(X|y))\\ X = Y \to (\phi(X) \to \phi(X|Y))$$.

Zuhair Al-Johar
  • 9,152
  • 3
    MK is an extension of ZFC + Classes by finitely many axioms. Since MK is not finitely axiomatizable (see e.g. https://mathoverflow.net/a/87249), ZFC + Classes is not finitely axiomatizable either. – Emil Jeřábek Dec 25 '22 at 08:23
  • @EmilJeřábek, Nice! Same argument applies if we weaken Comprehension to that of NBG, i.e. forbid quantification over class variables, which I'd label as ZFC + definable classes. It'll be finitely axiomatizable since also NBG would be an extension of it by finitely many axioms. – Zuhair Al-Johar Dec 25 '22 at 10:13
  • Finite axiomatizability is preserved upwards by adding finitely many axioms, but not preserved downwards. So the finite axiomatizability of NBG does not imply finite axiomatizability of ZFC + definable classes. In fact, I think this theory is liekly not finitely axiomatizable. – Emil Jeřábek Dec 25 '22 at 10:25
  • Indeed, if $T$ is any subtheory of ZFC that includes extensionality, then $T$ + Classes is conservative over $T$, and therefore $T+S$ is conservative over $T$ for any subtheory $S$ of Classes (such as “definable classes”). It follows that ZFC + $S$ is not finitely axiomatizable. – Emil Jeřábek Dec 25 '22 at 10:44
  • @EmilJeřábek, take ZFC + definable classes, remove Separation and Replacement and add the single axiom stating that the range of every set-ordinal definable function from a set is a set, also replace comprehension by finitely many instances of it. The resulting theory is finitely axiomatized. I'm not really sure if this is technically possible nor if it would be equivalent to ZFC + definable classes. – Zuhair Al-Johar Dec 25 '22 at 16:39
  • I don't understand why ZFC+Classes is conservative over ZFC, given that your class comprehension allows quantification over classes. – Joel David Hamkins Dec 26 '22 at 23:11
  • @JoelDavidHamkins, Yes, but replacement and separation are quite restricted to what ZFC say, there is no use of class variables here. I'll send you the proof of conservativity of ZFC + Classes over ZFC. – Zuhair Al-Johar Dec 27 '22 at 00:54
  • I see, you don't include class parameters in replacement and even separation. What a strange theory. Why should we care about it? – Joel David Hamkins Dec 27 '22 at 01:08
  • @JoelDavidHamkins, About this conservatively extending ZFC, see: https://math.stackexchange.com/a/4289425/489784 – Zuhair Al-Johar Dec 27 '22 at 01:42
  • @JoelDavidHamkins, I see this theory as constituting an earlier step in introduction of classes to ZFC than both MK and NBG, this is sometimes safer as far as trying to generally use classes over first order theories, for example the inconsistency of the original version of ML which tried to mimick MK could have been avoided if introducing classes to NF paralleled ZFC+Classes. Also ZFC+Classes doesn't prove size facts over classes, which I think it is an advantage, it makes it more flexible with extending it. – Zuhair Al-Johar Dec 27 '22 at 01:50

0 Answers0