Jump to content

Tarski–Kuratowski algorithm

From Wikipedia, the free encyclopedia

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

[edit]

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

  1. 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.)
  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]
  • Rogers, Hartley The Theory of Recursive Functions and Effective Computability, MIT Press. ISBN 0-262-68052-1; ISBN 0-07-053522-1