The TarskiâKuratowski algorithm for the arithmetical hierarchy consists of the following steps:
Convert the formula to
prenex normal form. (This is the non-deterministic part of the algorithm, as there may be more than one valid prenex normal form for the given formula.)
If the formula is quantifier-free, it is in and .
Otherwise, count the number of alternations of quantifiers; call this k.
If the first quantifier is
â, the formula is in .
If the first quantifier is
â, the formula is in .