Let $\phi$ be a formula and $a$ be a set. The relativization $\phi^a$ of $\phi$ to $a$ is defined as the formula obtained by replacing all [unbounded?] quantifiers $Qx$ in $\phi$ by $Qx {\in} a$. I sometimes see the definition that replaces all quantifiers, bounded or unbounded. However, I sometimes see the definition that replaces only unbounded quantifiers. For example:
- Reference 1 (p. 60):
$C^z$ is obtained from $C$ by replacing all unbounded quantifiers $\exists x$ in $C$ by $\exists x \in z$.
- Reference 2 (p. 833):
For every $\mathrm{L}_\Omega$ formula $A$ we write $A^\sigma$ to denote the $\mathrm{L}_\Omega$ formula which is obtained by replacing all unbounded quantifiers $(Q \xi)$ in $A$ by $(Q \xi < \sigma)$.
- Reference 3 (p. 29-30):
Here $\Phi^M$ is the formula obtained from $\Phi$ by replacing all unbounded quantifiers of the forms $\forall x, \exists x$ by quantifiers $\forall x \in M, \exists x \in M$. [...] \begin{align} (\forall x \Phi)_M &= \begin{cases} \forall x \Phi_M & \text{$\Phi$ is of the form $x \in a \to \Psi$} \\ \forall x {\in} M \Phi_M & \text{otherwise} \end{cases} \\ (\exists x \Phi)_M &= \begin{cases} \exists x \Phi_M & \text{$\Phi$ is of the form $x \in a \land \Psi$} \\ \exists x {\in} M \Phi_M & \text{otherwise} \end{cases} \end{align}
- Reference 4 (p. 10):
If $A$ is a transitive set and $\phi$ is a formula with parameters in $A$ we denote by $\phi^A$ the formula which arises from $\phi$ by replacing all unbounded quantifiers $\forall u$ and $\exists v$ in $\phi$ by $\forall u \in A$ and $\exists v \in A$, respectively.
- Reference 5 (p. 33):
Further, we write $A^\sigma$ to denote the $\mathcal{L}_\Omega$ formula which is obtained from $A$ by replacing all unbounded stage quantifiers in $Q \tau$ in $A$ by bounded stage quantifiers $(Q\tau \prec \sigma)$.
Which of the two definitions is correct? Is one more prominent or common than the other? Is there a standard notation and/or terminology for each that distinguishes the two?
References:
- The art of ordinal analysis. Michael Rathjen. 2006.
- Some theories with positive induction of ordinal strength $\phi \omega 0$. Gerhard Jäger, Thomas Strahm. The Journal of Symbolic Logic. Volume 61. Issue 3. September 1996. Pages 818-842.
- Large sets in constructive set theory. Albert Zieger. The University of Leeds School of Mathematics. December 2014.
- Proof theory of constructive systems: inductive types and univalence. Michael Rathjen. 5 January 2018.
- On Feferman’s operational set theory OST. Gerhard Jäger. Annals of Pure and Applied Logic. Volume 150. Issues 1-3. December 2007. Pages 19-39.