Алгоритм Тарского – Куратовского

редактировать

Алгоритм

Алгоритм Тарского – Куратовского для арифметической иерархии состоит из следующих шагов:

Преобразование формулы в предварительную нормальную форму. (Это недетерминированная часть алгоритма, поскольку для данной формулы может быть несколько допустимых предваряющих нормальных форм.)
Если формула не содержит кванторов, она находится в $Σ 0 0 {\ displaystyle \ Sigma _ {0} ^ {0}}$ $\ Sigma ^ 0_0$ и $Π 0 0 {\ displaystyle \ Pi _ {0} ^ {0}}$ $\ Pi ^ 0_0$ .
В противном случае подсчитайте количество чередований кванторов; назовите это k.
Если первый квантификатор ∃, формула находится в $Σ k + 1 0 {\ displaystyle \ Sigma _ {k + 1} ^ {0} }$ ${ \ displaystyle \ Sigma _ {k + 1} ^ {0}}$ .
Если первым квантификатором является ∀, формула находится в $Π k + 1 0 {\ displaystyle \ Pi _ {k + 1} ^ {0}}$ ${\ displaystyle \ Pi _ {k + 1} ^ {0}}$ .

Роджерс, Х. Теория рекурсивных функций и эффективная вычислимость, MIT Press. ISBN 0-262-68052-1 ; ISBN 0-07-053522-1