Tarski–Kuratowski algorithm

From Wikipedia, the free encyclopedia
  (Redirected from Tarski-Kuratowski algorithm)
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:

  1. Convert the formula to prenex normal form.
  2. If the formula is quantifier-free, it is in \Sigma^0_0 and \Pi^0_0.
  3. Otherwise, count the number of alternations of quantifiers; call this k.
  4. If the first quantifier is , the formula is in \Sigma^0_{k+1}.
  5. If the first quantifier is , the formula is in \Pi^0_{k+1}.

References[edit]