Relation between Tarski Semantics and Tarski Universes

The term Tarski Universe (in contrast to “Russell Universe”) is a direct homage to Alfred Tarski’s work on model theory and the indefinability of truth. The core connection between Tarski universes and Russell universes is the strict separation of syntax and semantics.

Tarski Semantics (Model Theory)

Tarski defined truth by separating the Object Language (the formulas being evaluated) from the Meta-Language (the mathematical framework where truth is defined).

• Syntax: A set of formulas $\varphi$.
• Semantics: An interpretation function $I$ (or satisfaction relation $\models$) mapping formulas to extensions in a model $\mathcal{M}$.
• Principle: A formula $\varphi$ is not the same object as its meaning $\parallel \varphi \parallel$.

Tarski Universes (Type Theory)

In Martin-Löf Type Theory, a Universe à la Tarski internalizes this structure:

• Syntax (Codes): An inductive type $U$ (the universe) containing “codes” or “names” for types.
  • Example: $nat\in U$ is a code, not the type of natural numbers itself.
• Semantics (Decoding): A recursive function $El:U\to \text{Type}$ (often written as $T$) that interprets codes into actual types.
  • Example: $El(nat)\equiv \mathbb{N}$.
• Relation: The judgment $u:U$ corresponds to “well-formed formula”, and $El(u)$ corresponds to the “extension” or “interpretation” of that formula.

Context: Dybjer & Setzer (1999)

Contrast: Universes à la Russell

In a Russell Universe, the distinction is collapsed: $U$ is a type of types, and if $A:U$, then $A$ is a type.

• This is convenient for formalization (Agda’s default Set is Russell-style).
• It conflates the code and the extension ($A=El(A)$).
• It obscures the model-theoretic intuition that Dybjer & Setzer require for establishing the metatheory of IR.

See also

Used in dybjer1999-inductive-recursive.