Which large cardinal this theory stops at proving its existence?

89 Views Asked by At

The language of this theory is first order predicate calculus with extra-logical primitive symbols of $``=; \in, W"$, where $``W"$ is a constant symbol.

Axioms: those for identity theory +

Extensionality: $\forall A \forall B: \forall Z (Z \in A \Leftrightarrow Z \in B) \implies A=B$

Define: $set(X) \iff \exists Y ( X \in Y)$

Class Comprehension: if $\phi$ is a formula in which Y is free, and $X$ not free, then all closures of the following are axioms: $$\exists X \forall Y (Y \in X \iff set(Y) \land \phi)$$

Define: $X=V \iff \forall Y (set(Y) \Rightarrow Y \in X)$

Define: $X=\{Y|\phi\} \iff \forall Y (Y \in X \Leftrightarrow \phi(Y))$

Foundation: $\forall X : X \neq \emptyset \implies \exists Y \in X (Y \cap X = \emptyset)$

Pairing: $\forall A,B \in V \exists X \in V: X=\{A,B\}$

Define: $H_{< W} (X) \iff \forall Y \in \text {Tr.cl}(\{X\}) (Y < W)$

Where: $Y < W \iff (\exists f: Y \hookrightarrow W \land \not \exists g: W \hookrightarrow Y)$

Where $``\hookrightarrow"$ signifies injection.

$\text {Tr.cl}(A) $ stands for "the transitive closure class of $A$", defined in the usual manner as the intersection of all transitive classes having $A$ as a subclass of.

A formula is said to be class theoretic formula if all of its terms are variables and only uses symbols $``=,\in"$ as predicate symbols.

A formula is said to be set theoretic formula if it results from the mere bounding of all of quantifiers in a class theoretic formula by the symbol $V$

Reflection: if $\phi$ is a set theoretic formula whose free variable symbols are among symbols of $Y,\vec{P}$, then: $$\forall \vec{P}\big{[} H_{< W} [\vec{P}]\land \forall Y (\phi(Y) \Rightarrow H_{< W}(Y)) \implies \\\exists X < W: X=\{Y|\phi\} \big{]} $$

This theory can interpret $\sf MK$ [Limitation of size replaced by the axiom of: any class equinumerous to a set is a set] in a straightforward manner. So it proves the consistency of ZFC via $\sf MK$. I don't think that foundation is necessary for that interpretation.

I don't see an easy way to prove every class of hereditarily strictly subnumerous to $W$ sets (i.e. the $H_{<W}$ sets) to be a set? Which is what's needed to provide a direct interpretation of Ackermann's set theory. However, this theory can of course indirectly interpret Ackermann via interpreting $\sf MK$.

How far this theory can go? What is the least large cardinal this theory cannot prove the existence of?

[Afternote] It happens that this theory (if consistent) would directly interpret Muller's theory of sets and classes, which he advocated as a foundational theory of mathematics. Also to be noted is that if we add an axiom of: $ H_{<W} \hookrightarrow W$; that is, the class of all $H_{<W}$ sets is subnumerous to $W$ [thus equinumerous with $W$], and add an axiom of any class equinumerous with a set is a set, then global choice would be enacted over $H_{<W}$, and we get to interpret directly both full $\sf MK$ and full Ackermann's since all subclasses of $H_{<W}$ would be sets. My guess is that this would add strength, though I don't know how much. We can even let $|W|=|H_{<W}|$ by changing the consequent in Reflection to $\exists X \in W: X=\{Y|\phi\}$, and this with limitation of size over $V$ would interpret also full $\sf MK$, Ackermann's, and Muller's theories in one go!