What does it mean to say that a sentence in a predicate logic is "$\Pi_2$"? So I've come across this classification of sentences in a predicate language a couple of times. A "$\Sigma_1$" sentences is of the form "$\exists x \phi x$" for a quantifier-free $\phi$. A $\Pi_1$ sentences is one of the form $\forall x \phi x$. (I think this is right.) So my question is, in general what form does a $\Pi_n$ sentence have, and why is it a useful characterisation of sentences in a logic? A short introduction to the use of such a characterisation would be helpful. (hence the reference request tag)
 A: Let $\varphi$ be a sentence in prenex normal form (all quantifiers at the front).  Then indeed the sentence is called $\prod_2$ if it has form $\forall x_1\cdots \forall x_k  \exists y_1\cdots \exists y_l \psi$ where $\psi$ is quantifier-free.  For some purposes, there are finer classifications, where in addition we count the actual numbers of each type of quantifier. 
The general definition is by induction. A formula is $\Pi_0$, and also $\Sigma_0$, if it is quantifier-free. A formula is $\Pi_{n+1}$ if it has shape $\forall x_1\cdots\forall x_k\psi$, where $\psi$ is $\Sigma_n$. A formula is $\Sigma_{n+1}$  if it has shape $\exists x_1\cdots\exists x_k\psi$, where $\psi$
is $\Pi_n$. A sentence is $\Pi_n$ (respectively, $\Sigma_n$) if it is $\Pi_n$ (respectively, $\Sigma_n$) when viewed as a formula. 
I do not know how far back names such as $\pi_2$ go.  The standard name for such sentences used to be "sentences of the form $\forall\exists$."  The use of $\Sigma$ and $\Pi$ for quantifiers dates back to the nineteenth century, but did not catch on. I think that the first use of notations of the type $\Pi_n$ and $\Sigma_n$ was for roughly analogous notions in analysis, specifically descriptive set theory. 
The first classification of sentences by using the number of alternations of quantifiers arose in connection with the decision problem, and is associated with the school of Hilbert.  It was realized quite early on that finding a decision procedure for the predicate calculus might be difficult.  So, in typical mathematical fashion, mathematicians looked for subproblems that they could solve.  
A natural approach is to put restrictions on the types of formulas considered. One reasonable measure of complexity is the number of alternations of quantifiers. Some progress was already achieved by Skolem around 1920.  Much more work was done by students of Hilbert in the late 1920's.  Some of this work appears in the book by Hilbert and Ackermann. The enterprise ultimately had to fail, since the predicate calculus is undecidable already when there is a single binary predicate symbol.
Although the predicate calculus was proved undecidable in the 1930's, work on subclasses of sentences did not end then. An important later result was the one by Wang, that the $\forall\exists\forall$ case is undecidable.  There has also been a fair bit of more recent work, for example by Goldfarb and Gurevich.  Similar themes are continuing to be explored in Theoretical Computer Science. 
There are classifications in other areas of mathematics that use very similar ideas, and indeed notation. Two examples should be mentioned.   There are the hierarchies of Descriptive Set Theory, starting with the Borel hierarchy, that counts the number of alternations between countable unions and complements, starting from open sets.  There are also hierarchies that go well beyond Borel sets, such as the projective hierarchy. These hierarchies were studied from quite early on in the history of point set topology, and have been given renewed importance by set-theoretic independence results. 
There is also the arithmetical hierarchy, that starts with the recursive sets. At the next levels are the recursively enumerable sets (existential quantification) and the co-r.e. sets (universal quantification), and so on forever.  It can also be described in terms of alternations of quantifiers, starting from formulas of arithmetic that only use bounded quantification. There has been a certain amount of interplay and cross-fertilization between work on descriptive set theory and work on the arithmetical hierarchy.  
