3
$\begingroup$

$\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))$$.

$\endgroup$
10
  • 3
    $\begingroup$ MK is an extension of ZFC + Classes by finitely many axioms. Since MK is not finitely axiomatizable (see e.g. mathoverflow.net/a/87249), ZFC + Classes is not finitely axiomatizable either. $\endgroup$ Dec 25, 2022 at 8:23
  • $\begingroup$ @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. $\endgroup$ Dec 25, 2022 at 10:13
  • $\begingroup$ 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. $\endgroup$ Dec 25, 2022 at 10:25
  • $\begingroup$ 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. $\endgroup$ Dec 25, 2022 at 10:44
  • $\begingroup$ @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. $\endgroup$ Dec 25, 2022 at 16:39

0

Your Answer

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

Browse other questions tagged or ask your own question.