Tarski–Kuratowski algorithm

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In computability theory and mathematical logic the Tarski–Kuratowski algorithm is a non-deterministic algorithm which provides an upper bound for the complexity of formulas in the arithmetical hierarchy and analytical hierarchy.

The algorithm is named after Alfred Tarski and Kazimierz Kuratowski.

Algorithm[edit]

The Tarski–Kuratowski algorithm for the arithmetical hierarchy consists of the following steps:

  1. Convert the formula to prenex normal form.
  2. If the formula is quantifier-free, it is in and .
  3. Otherwise, count the number of alternations of quantifiers; call this k.
  4. If the first quantifier is , the formula is in .
  5. If the first quantifier is , the formula is in .

References[edit]