Are those two theories about universes equivalent?

Question

If we define a universe as a well founded extensional transitive set that is closed under power, union, and non-bigger than, formally this is:

$\mathbf U (X) \iff \forall a \in X: \\ \forall m \in a (m \in X) \\\forall b \in X :\forall z (z \in b \leftrightarrow z \in a) \to a=b \\\forall S \subseteq X \exists m \in S: \forall n \in S (n \not \in m) \\ \exists c,d \in X : c=\mathcal P(a), d=\bigcup(a) \\\forall k \subseteq X (|k| \not > |a| \implies k \in X)$

Where: $|k| > |a| \iff \exists f: a \hookrightarrow k \land \not \exists g: k \hookrightarrow a$

Where $``\hookrightarrow"$ signify injection; and $``\mathcal P, \bigcup"$ standing for powerset and set unions defined in the usual manner.

And if we add the following axioms on top of mono-sorted first order logic with equality and membership.

1. Universes: $\forall x \exists w: \mathbf U(w) \land x \in w$

Every set belongs to some universe.

2. Separation: $\forall a \exists b: b=\{x \in a: \phi\}$, where $\phi$ doesn't use $``b"$.

Then this would prove $ZFC$ over universes higher than $V_\omega$. If we want to prove $ZF+GC$ over those universes, then we'll need to modify the size condition in the definition of universes to:

$\forall k \subseteq X (|k| \neq |X| \implies k \in X)$

Where: $|k|=|X| \iff \exists f: k \hookrightarrow X \land \exists g: X \hookrightarrow k $

Call this theory as Universes Theory, to be denoted by $\sf UT$.

To get ZFC we need to add the axiom of Largeness:

3. Largeness: $\forall x \exists w: |w| > |x| \land \forall u \in w (\mathbf U(u))$

Every set is strictly smaller than a set of universes.

I think that all sentences of $\sf TG$ set theory would be provable in this system, so this is just a reformulation of it.

However, the axiom of largeness seems to be more of a fix. I think a more principled axiom would be the following:

3. Generalization: $(\forall w: \mathbf U(w) \to \phi^w) \implies \phi$,

Where $\phi^w$ is a sentence with all of its quantifiers bounded $\in w$, and $w$ not used otherwise.

In English: what is true inside all universes is true in the whole world!

Is the generalization axiom consistent with the first two?

Are both theories ($\sf UT+Larg.; UT+Gen.$) equivalent?

Answer 1

This is a partial answer to this question.

For the second question it appears that $\sf UT + Gen$ is stronger than $\sf TG$ set theory because I think it proves the existence (among its elements) of a universe that doesn't have a set of all universes in it, more specifically a universe that is the union of inaccessibly many universes below it, this universe would satisfy all sentence of $\sf TG$ and thus would prove $\sf Con(TG)$. This very same universe would also satisfy all sentences of $\sf UT+ Larg$. However, I don't know where the consistency strength of that theory would stop, or even if its consistent either?

Answer 2

+. is inconsistent.

We note that if () and is th least ordinal not in X, then X=.

Proof:Suppose X is not a subset of . Let Y={x∈X | x∉}. There is y∈Y such that for all x∈Y, x∉y. There is a set A, such that ∈A iff is the least ordinal such that x∈ for some x∈y,. Then A is in X. Therefore UA is in X. But x⊆(UA) and thus x∈. Suppose is not a subset of X. Let B={x∈| x is not a subset of X}. Let be the least element of B. There is a set W={(t+1)|t∈B}. But UW∈X and =UW.

Let b be a function with domain ω, which enumerates those x such that "x is a sentence" holds, and "x does not hold in every universe" holds.

For every n∈ω, there is a least ordinal n such that n is a universe, Universes holds in n, and for all m∈(n+1), there is a universe X in n for which "bm does not hold in X".

Proof:Let N be the set of n∈ω such that there is a least ordinal n such that (n), Universes holds in n, and for all m∈(n+1), there is a universe X in n such that "bm does not hold in X". Universes holds and there is an X such that (X) and "b0 does not hold in X". By Generalization, there must be Y such that (Y) and Universes holds in Y and ("there is an X such that (X) and "b0 does not hold in X") holds in Y. 0 is the least such universe. Suppose that k∈N. If "b(k+1) doe not hold in X" for some universe X∈k, then (k+1)=k. Suppose ("b(k+1) doe not hold in X" and (X)) implies X∉k. Universes holds and there is an X such that (X) and "b(k+1) does not hold in X". By Generalization, there must be Y such that (Y), Universes holds in Y, and (there is an X such that (X) and "b(k+1) does not hold in X") holds in Y. (k+1) is the least such Y. Therefore N=ω.

Suppose "S is a finite set of sentences" holds. For each in S, there is a "Generalization sentence" for . Let T be the set of those "Generalization sentences". Then Con(+T)

Proof: If ∈S and " does not hold in every universe" holds, then is bm for some m. There is an n∈ω, such that if bm∈S, then m<n since "S is finite" holds. Then "UT"+T holds in n.

Since the consistency of every "finite subtheory of +." is provable in +., Con(+) is provable in +.. Therefore +. is inconsistent.