Editing Analytical hierarchy (section)

== The analytical hierarchy of formulas ==
The notation <math>\Sigma^1_0 = \Pi^1_0 = \Delta^1_0</math>
indicates the class of formulas in the language of [[second-order arithmetic]] with number quantifiers but no set quantifiers. This language does not contain set parameters. The Greek letters here are [[lightface]] symbols, indicating the language choice. Each corresponding [[Boldface (mathematics)|boldface]] symbol denotes the corresponding class of formulas in the extended language with a parameter for each [[Cantor space|real]]; see [[projective hierarchy]] for details.

A formula in the language of second-order arithmetic is defined to be <math>\Sigma^1_{n+1}</math> if it is [[logical equivalence|logically equivalent]] to a formula of the form <math>\exists X_1\cdots \exists X_k \psi</math> where <math>\psi</math> is <math>\Pi^1_{n}</math>. A formula is defined to be <math>\Pi^1_{n+1}</math> if it is logically equivalent to a formula of the form <math>\forall X_1\cdots \forall X_k \psi</math> where <math>\psi</math> is <math>\Sigma^1_{n}</math>. This inductive definition defines the classes <math>\Sigma^1_n</math> and <math>\Pi^1_n</math> for every natural number <math>n</math>.

[[Kuratowski]] and [[Alfred Tarski|Tarski]] showed in 1931 that every formula in the language of second-order arithmetic has a [[prenex normal form]],<ref>[[Piergiorgio Odifreddi|P. Odifreddi]], ''Classical Recursion Theory'' (1989), p.378. North-Holland, 0-444-87295-7</ref> and therefore is <math>\Sigma^1_n</math> or <math>\Pi^1_n</math> for some <math>n</math>. Because meaningless quantifiers can be added to any formula, once a formula is given the classification <math>\Sigma^1_n</math> or <math>\Pi^1_n</math> for some <math>n</math> it will be given the classifications <math>\Sigma^1_m</math> and <math>\Pi^1_m</math> for all <math>m</math> greater than <math>n</math>.