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 , , and by induction on .
A formula is iff it is iff it is , by definition if it is equivalent to a formula all of whose quantifiers are bounded, i.e. of the form or .
A formula is if it is equivalent to one of the form , where is a list of variables and is .
A formula is if it is equivalent to one of the form , where is a list of variables and is .
A formula is if it is both and .
A class is given one of these labels if it can be defined by a formula which has that label.
The notation “” and “” 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 or .
Last revised on September 25, 2012 at 05:35:38. See the history of this page for a list of all contributions to it.