Теорема Чёрча — Тьюринга

Теоре́ма Чёрча — Тью́ринга — утверждение об отсутствии алгоритма, решающего проблему разрешения. Используется при доказательстве неразрешимости арифметики натуральных чисел^[1]. Впервые была сформулирована и доказана в 1936 году Алонзо Чёрчем^[2][3] (вместе с тезисом Чёрча); в том же году, но несколько позже этот результат независимо получил Алан Тьюринг^[4][5].

Формулировка

Предикат ${\displaystyle (Ex)T(a,a,x)}$^{[уточнить]} неразрешим, то есть функция:

${\displaystyle \chi (a)={\begin{cases}0,&{\mbox{if}}(Ex)T(a,a,x)\\1,&{\mbox{else}}\end{cases}}}$

невычислима.

Данная формулировка использует понятие вычислимости по Тьюрингу.

См. также

• Теорема Геделя о неполноте
• Теорема Тарского о невыразимости истины