### Communities

tag:snake search within a tag
user:xxxx search by author id
score:0.5 posts with 0.5+ score
"snake oil" exact phrase
created:<1w created < 1 week ago
post_type:xxxx type of post
Q&A

# On Tarski-style universes in type theory

+2
−0

I'm looking at this note about universes in type theory.

For Tarski-style universes (page 2), as far as I understand, the "$a$" in $a:U_i$ are formal names of types, whereas the "$T_i(a)$" in $T_i(a) \ type$ are actual types. What I don't understand is the purpose of "$u_i:U_{i+1}$" and "$T_{i+1}(u_i)=U_i$". Is there any intuitive explanation on why we have these two "axioms" (or whatever)?

Further, it is said in the remark on page 3 that Tarski-style universes can be formulated in LF:

$U_i: \textbf{Type}; \ T_i: (U_i)\textbf{Type};\ u_i:U_{i+1};\ T_{i+1}(u_i)=U_i : \textbf{Type}$

But how is this related to $El(A)$ from the LF mentioned in my previous question? Is there any relationship between $El(-)$ and $T_j(-)$?

Why does this post require moderator attention?
Why should this post be closed?

+1
−0

I'm a bit confused about what you're confused about for the first part. In a Russell-style universe system, we'd have a hierarchy of universes with $\mathcal U_i : \mathcal U_{i+1}$, i.e. the $i$th universe is a type in the $(i+1)$th universe. As you state, for a Tarski-style universe system, $\mathcal U_i$ is a type of "codes" for types in the $i$th universe and $T_i(a)$ for $a : \mathcal U_i$ is the "actual" type, i.e. a thing that can be to the right of a "$:$". Thus, there should be a code $u_i$ in $\mathcal U_{i+1}$ that represents the fact that $\mathcal U_i$ is a type in the $(i+1)$th universe. That is, $u_i : \mathcal U_{i+1}$ and $T_{i+1}(u_i) = \mathcal U_i$. This is just directly how you say the Russell-style $\mathcal U_i : \mathcal U_{i+1}$ in a Tarski-style universe.

As for how $El$ relates to $T_i$, $El$ and $T_0$ are the same thing where LF has only one universe, namely $\mathsf{Type}$. So $\mathcal U_0$ correspond to $\mathsf{Type}$, $T_0$ corresponds to $El$, and $type$ corresponds to $kind$. To be clear, this is treating LF and this logic with Tarski-style universes on the same footing. If we wanted to formalize this logic in LF, then the $El$ of LF as the meta-language and the $T_0$ of the object language would be different kinds of things.

Why does this post require moderator attention? 