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 Tarski–Kuratowski algorithm for the arithmetical hierarchy:
- Convert the formula to prenex normal form.
- 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 .
- Rogers, H. The Theory of Recursive Functions and Effective Computability, MIT Press. ISBN 0-262-68052-1; ISBN 0-07-053522-1
|This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.|