Introduced in [[Lévy - A hierarchy of formulas in set theory]], the Lévy hierarchy is a hierarchy of formulas in the language of set theory (LST - $\{\in \}$). # Definition Let $\Phi$ be an LST-formula. Define recursively: - $\Phi$ is $\Sigma_0$ (or $\left.\Pi_0\right)$ iff it contains no unbounded quantifiers. - $\Phi$ is $\Sigma_{n+1}$ iff it is of the form $\exists \vec{x} \Psi(\vec{x})$ where $\Psi(\vec{x})$ is $\Pi_{n}$ - $\Phi$ is $\Pi_{n+1}$ iff it is of the form $\forall \vec{x} \Psi(\vec{x})$ where $\Psi(\vec{x})$ is $\Sigma_{n}$. For a theory $T$ (usually a subtheory of $\mathrm{ZF}$) , we say that a formula $\Phi$ is $\Sigma_n^{T}$ iff there is a $\Sigma_n$ formula $\Psi$ such that $ T \vdash \Phi \leftrightarrow \Psi $ Similarly $\Pi_n^{T}$. A formula $\Phi$ is said to be $\Delta_n^{T}$ iff it is both $\Sigma_n^{T}$ and $\Pi_n^{T}$. >[!note] Remark >In many contemporary texts mention of $T$ is omitted, and is simply assumed to be $\mathrm{ZF(C)}$. >Then a common characteristic is the following >- $\Phi$ is $\Sigma_{n}$ ($n \geq 1$) if it is equivalent to a formula > $\exists\vec{x_{n}}\forall\vec{x_{n-1}}\dots Q\vec{x_{1}} \Psi$ > with alternating blocks of quantifiers ($Q\in\{\exists,\forall\}$) and $\Psi$ does not contain unbounded quantifiers. >- $\Phi$ is $\Pi_{n}$ ($n \geq 1$) if it is equivalent to a formula > $\forall\vec{x_{n}}\exists \vec{x_{n-1}}\dots Q\vec{x_{1}} \Psi$ > with alternating blocks of quantifiers ($Q\in\{\exists,\forall\}$) and $\Psi$ does not contain unbounded quantifiers >[!example] >- "$R$ is a wellfounded relation" is $\Delta_{1}^{\mathrm{ZFC}^{-}}$. >- Axiom of Extensionality is $\Pi_{1}$ >- Axiom of Foundation is $\Pi_{1}$ >- Axiom of Infinity is $\Sigma_{1}$ The *quantifier rank* (or simply *rank*) of a formula $\varphi$ of the basic language, to be denoted with ${\rho}(\varphi)$, is defined recursively as follows. 1) If $\varphi$ is atomic then $\rho(\varphi)=0$; 2) if $\varphi$ is $\psi \mid \chi$ ($\mid$ is the Sheffer stroke) then $\rho(\varphi)=\max\{\rho(\psi),\rho(\chi)\}$ 3) if $\varphi$ is $\exists v\left(v \in w \wedge \psi\right)$ and $v \ne w$ then $\rho(\varphi)=\rho(\psi)$; 4) and if $\varphi$ is $\exists v\ \psi$, where $\psi$ is not $v \in w \wedge \chi$ for some $v\ne w$ and some $\chi$, then $\rho(\varphi)=\rho(\psi)+1$. We denote $\Lambda_n=\{\varphi \mid \rho(\varphi) = n\}$. And as before define $\Lambda_{n}^{T}$. >[!note] Remark >Although $\Lambda_{n}$ consists of formulas of rank exactly $n$, $\Lambda_{n}^{T}$ consists of formulas of rank *at most* $n$ as we can add dummy quantifiers. # Facts ![[Absoluteness#^18da90]] # Boldface hierarchy The boldface hierarchy generalizes the Lévy hierarchy to formulas with higher order variables. We say that formula is in prenex form if all the quantifiers in the formula appear at the beginning of the formula in a string, those of highest order first and so on. A prenex formula is called a $\boldsymbol{\Pi}_m^n\left(\boldsymbol{\Sigma}_m^n\right)$ where $m \geqslant 1$ if the highest order quantifiers appears are $(n+1)$ th order, if the first quantifiers is a universal (existential) $(n+1)$ th order quantifier, and if there are $(m-1)$ alternations of $(n+1)$ th order quantifiers (i.e., there are $(m-1)(n+1)$ th order quantifiers immediately followed by a quantifier of the opposite kind). >[!note] Remark >In some texts, and in handwriting, these are denoted by an "undertilde"