basic constructions:
strong axioms
further
In logic, model theory, and set theory, the Lévy hierarchy is a stratification of formulas, definable sets, and (definable) classes according to the complexity of the unbounded quantifiers.
We define classes of formulas $\Sigma_n$, $\Pi_n$, and $\Delta_n$ by induction on $n$.
A formula is $\Sigma_0$ iff it is $\Pi_0$ iff it is $\Delta_0$, by definition if it is equivalent to a formula all of whose quantifiers are bounded, i.e. of the form $\forall x\in A$ or $\exists x\in A$.
A formula is $\Sigma_{n+1}$ if it is equivalent to one of the form $\exists \vec{x}. \phi$, where $\vec{x}$ is a list of variables and $\phi$ is $\Pi_n$.
A formula is $\Pi_{n+1}$ if it is equivalent to one of the form $\forall \vec{x}. \phi$, where $\vec{x}$ is a list of variables and $\phi$ is $\Sigma_n$.
A formula is $\Delta_n$ if it is both $\Sigma_n$ and $\Pi_n$.
A class is given one of these labels if it can be defined by a formula which has that label.
The notation “$\Sigma$” and “$\Pi$” can be explained by the fact that the existential quantifier is related to a dependent sum, while the universal quantifier is related to the dependent product.
These definitions are most useful in classical mathematics, in which every formula is equivalent to one all of whose unbounded quantifiers are in the front, that is, a formula in prenex normal form?, so that every formula belongs to some $\Sigma_n$ or $\Pi_n$.