Sigma hierarchy of logical formulae In some papers on mathematical logic I've found references to hierarchy like $\Sigma_1^0$-sentence and so on. What does it mean? What is $\Sigma_n^m$, what is $n$ and $m$ here?
 A: You need to get your head round the idea of a bounded wff -- i.e. all the quantifiers are bounded -- so we never have an occurrence of $\forall n$, for example, but always $(\forall n < \tau)$ for some term. These are known as $\Delta_0$ or $\Sigma_0$ wffs. A bounded universal quantifier is like a finite conjunction, and a bounded existential quantifier is like a finite disjunction. So wffs with only bounded quantifiers are morally equivalent to unquantified wffs. Hence they are Jolly Nicely Behaved in various ways.
Then, [logical equivalents of] existentially quantified $\Delta_0$ wffs are $\Sigma_1$ wffs and [logical equivalents of] universally quantified $\Delta_0$ wffs are $\Pi_1$ wffs. [Think $\Sigma$ for logical Sum and $\Pi$ for logical product.] 
You might find some further help in §26 of http://www.logicmatters.net/resources/pdfs/gwt/GWT2e.pdf
A: The notation relates to a hierarchy of formulas for the theory of "arithmetic in all finite types". The superscript refers to the highest type of object being quantified; the subscript refers to the outermost quantifier of that type.
Working over the natural numbers, we say that the "type" of the natural numbers is $0$. The "type" of the set of functions from $\mathbb{N}$ to $\mathbb{N}$ is $1$. In general, once we know what the objects of type $n$ are, the objects of type $n+1$ are functions that take objects of type $n$ as input and return a natural number. For example, there is a particular functional $F$ of type $2$ defined as follows:

For all $g \colon \mathbb{N} \to \mathbb{N}$, $F(g) = 0$ if there is a $k$ such that $g(k) = 0$, and $F(g) = 1$ otherwise. 

We consider formulas built up from a language where we have different sets of variables, and different quantifiers $\exists^k$ and $\forall^k$ for each finite type $k$. This is a kind of multi-sorted logic. The base language for arithmetic includes (among other things) the addition and multiplication functions and the equality relation.
Arithmetical hierarchy
In ZFC, any such formula is equivalent to one in which all the quantifiers appear at the front of the formula, and in which the types associated with the quantifiers are nonincreasing. Given a formula in that normal form, we say that:


*

*the formula is $\Sigma^k_{n+1}$ if the outermost quantifier is $\exists^k$, and there are $n$ alternations between blocks of $\exists^k$ and $\forall^k$ at the front of the formula. 

*the formula is $\Pi^k_{n+1}$ if the outermost quantifier is $\forall^k$, and there are $n$ alternations between blocks of $\exists^k$ and $\forall^k$ at the front of the formula. 
The full definition has some additional clauses that are useful in practice. The surprising thing is that this definition is actually useful, at least when $k \in \{0,1\}$. In that context, the number of alternations of quantifier blocks turns out to tell quite a bit about the computability notations required to handle the formula semantically. For higher $k$, the relationship with computability tapers off. 
Examples


*

*A set of natural numbers is recursively enumerable if and only if it is definable by a $\Sigma^0_1$ formula.

*A set of natural numbers is decidable if and only if it is definable by a $\Sigma^0_1$ formula and also definable by a $\Pi^0_1$ formula.

*A set of natural numbers is hyperarithmetic if and only if it is definable by a $\Sigma^1_1$ formula and also definable by a $\Pi^1_1$ formula.

*There is a single $\Sigma^2_1$ formula that is true if and only if the continuum hypothesis is true. This formula does not directly state the continuum hypothesis; instead it says there is a well ordering of the reals such that every initial segment is countable. 
Side note
One noteworthy aspect of the preceding definition of types is that it does not include basic type-theoretic constructions such as product types. This is because, in the special context of arithmetic, product types can be replaced by "pure" types, which are the ones I described. Similarly, there are no quantifiers over sets, because we can represents sets by their characteristic functions.  In the context of second-order arithmetic, where we only have types $0$ and $1$, it is common to have quantifiers over sets instead of functions, which does have some subtle effect on the complexity of formulas.
