Are those two theories about universes equivalent? 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?

 A: +. 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.
A: 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?
