什么猫

Question

Grothendieck extending Bourbaki ZF set theory to include universes, he adds the well known, UA, axiom as well as a second axiom, UB, concerning the closedness of the Hilbert tau operator used by Bourbaki. Most authors while accept UA ignore the UB, do not even mention it. Has it been proved redundant or what?

(UA): “every set is an element of a some universe,”

(UB): “if U is a universe, R{x} is a formula and there exists a y?∈?U satisfying R{y}, then τ?(R{x}) is an element of U.”

Answer 1

Part of the reason that people don't mention this axiom anymore is that first-order logic isn't commonly formalized in terms of the Hilbert choice operator $\tau$ (which is often $\varepsilon$ outside of Bourbaki) these days.

That said it's reasonable to wonder whether this axiom is conservative over the common formalization of Tarski–Grothendieck ($\def\TG{\mathsf{TG}}\TG$) set theory you see on, for instance, Wikipedia. It turns out that it is but the most direct proof of this fact is moderately involved, so I'll establish it indirectly via another result, specifically the fact that von Neumann–Bernays–G?del set theory ($\def\NBG{\mathsf{NBG}}\NBG$) set theory (with global choice) is conservative over $\def\ZFC{\mathsf{ZFC}}\ZFC$.

By a fairly general argument, this implies that $\TG + \NBG$ is actually conservative over $\TG$. To see this note that for any sentence $\varphi$ in the language of ordinary set theory provable from $\TG + \NBG$, there is by compactness a conjunction $\psi_1 \wedge \dots \wedge \psi_n$ of axioms of $\TG$ such that $\NBG \vdash \psi_1 \wedge \dots \wedge \psi_n \to \varphi$. By conservativity of $\NBG$ over $\ZFC$ for sentences in the language of set theory, this means that $\ZFC \vdash \psi_1 \wedge \dots \wedge \psi_n \to \varphi$ and so $\TG \vdash \varphi$ (since $\TG$ is an extension of $\ZFC$).

Let $T$ be the theory consisting of $\TG + \NBG$ extended with a unary function $f$ from sets together with the following statements:

• $f(\varnothing) = \varnothing$.
• For any non-empty $x$, $f(x) \in x$.
• There is a class $F$ such that $F = \{(x,f(x)) : x~\text{a set}\}$. Since $\NBG$ proves the existence of a global choice function coded as a class, $T$ is a conservative extension of $\TG + \NBG$.

Now we can interpret the $\tau$ operator using $f$ via a syntactic transformation. In Bourbaki's set theory, formulas and terms are defined in a mutually inductive way:

• For any terms $t$ and $s$, $t \in s$ is a formula. The free variables of $t \in s$ are the union of the free variables of $t$ and the free variables of $s$.
• For any formula $\varphi$, $\neg \varphi$ is a formula with the same free variables.
• For any formula $\varphi$ and $\psi$, $\varphi \wedge \psi$ and $\varphi \vee \psi$ are formulas whose free variables are the union of the free variables of $\varphi$ and the free variables of $\psi$.
• For any formula $\varphi$, $\tau_x \varphi$ is a term whose free variables are the free variables of $\varphi$ minus $x$.
• Each variable symbol $x$ is a term whose set of free variables is $\{x\}$.

In describing the syntactic transformation, I'm going to cheat a little bit by adding a certain kind of set abstraction to the language. Specifically, given a formula $\varphi(x,\bar{y})$ in the language of set theory, we'll write $\{x~\text{m.r.} : \varphi(x,\bar{y})\}$ to indicate (for a given choice of $\bar{y}$), the set of $x$ of minimal foundational rank satisfying $\varphi(x,\bar{y})$. (The function that takes $\bar{y}$ to this set is definable in $\ZFC$.) This is a term with $\bar{y}$ as its set of free variables.

Okay so now we'll define the transformation from Bourbaki-style formulas and terms to formulas and terms in $T$ as follow.

• $(\tau_x \varphi)^\dagger = f(\{x~\text{m.r.} : \varphi\})$.

The other clauses in the translation are obvious.

• $(t \in s)^\dagger = t^\dagger \in s^\dagger$.
• $(\neg \varphi)^\dagger = \neg \varphi^\dagger$, $(\varphi \wedge \psi)^\dagger = \varphi^\dagger \wedge \psi^\dagger$, and $(\varphi \vee \psi)^\dagger = \varphi^\dagger \vee \psi^\dagger$.
• $x^\dagger = x$.

Since $f$ is a global choice function, this implements the $\tau$ operator correctly. All of the axioms of the Bourbaki-style version of $\TG$ are immediate. For $\mathsf{UB}$ specifically, note that since we've defined $\tau$ in such a way that it always chooses minimal rank witnesses, it will be the case that whenever there is an $a$ satisfying $\varphi(a)$ in a universe $U$, $\tau_x\varphi(x)$ will be an element of $U$ as well. To see that this works note that the foundational rank of $\tau_x \varphi(x)$ is by construction minimal and so will be no greater than the rank of $a$. Since Grothendieck univereses are the same thing as sets of the form $V_\kappa$ for strongly inaccessible $\kappa$, this implies that $\tau_x\varphi(x)$ is an element of any Grothendieck universe that $a$ is an element of.