Post teoremasining isboti

Post teoremasining isboti
Turing mashinalarini birinchi darajali arifmetikada rasmiylashtirish
A-ning ishlashi Turing mashinasi N kirishidagi T mantiqan rasmiylashtirilishi mumkin birinchi darajali arifmetik. Masalan, biz foydalanishimiz mumkin belgilar A_k, B_kva C_k lenta konfiguratsiyasi, moslama holati va lenta bo'ylab joylashuvi mos ravishda k qadamdan keyin. T o'tish tizimi (A) orasidagi munosabatni aniqlaydi_k, B_k, C_k) va (A_{k + 1}, B_{k + 1}, C_{k + 1}); ularning boshlang'ich qiymatlari (k = 0 uchun) mos ravishda kirish, boshlang'ich holati va noldir. Mashina, agar B soni k bo'lsa, u holda to'xtaydi_kto'xtab turgan holat.
Aniq munosabatlar Turing mashinasi tushunchasining aniq bajarilishiga bog'liq (masalan, ularning alifbosi, lenta bo'ylab harakatlanish tartibi va boshqalar).
T holatida n to'xtab qolsa₁, (A_k, B_k, C_k) va (A_{k + 1}, B_{k + 1}, C_{k + 1}) faqat yuqoridan n bilan chegaralangan k uchun qondirilishi kerak₁.
Shunday qilib, formula mavjud  yilda birinchi darajali arifmetik un bilanchegaralangan miqdorlar, shunday qilib T, n vaqtida n kirishni to'xtatadi₁ ko'pi bilan va faqat agar  mamnun.