Tarski–Kuratowski algorithm
# Tarski–Kuratowski algorithm

In computability theory and mathematical logic the Tarski–Kuratowski algorithm is a non-deterministic algorithm that produces an upper bound for the complexity of a given formula in the arithmetical hierarchy and analytical hierarchy.

The algorithm is named after Alfred Tarski and Kazimierz Kuratowski.

## Algorithm

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 $\Sigma _{0}^{0}$ and $\Pi _{0}^{0}$.
* Otherwise, count the number of alternations of quantifiers; call this k.
* If the first quantifier is ∃, the formula is in $\Sigma _{k+1}^{0}$.
* If the first quantifier is ∀, the formula is in $\Pi _{k+1}^{0}$.
