תורת החישוביות/משפט הרקורסיה: הבדלים בין גרסאות בדף

# בעזרת <math>\langle M \rangle</math> המכונה מגדירה את הטענה (המחרוזת) S

#: S": "המכונה <math>M</math> לא עוצרת על הקלט הריק"

#המכונה מונה את כל המחרוזות x (ההוכחות x), אחת אחרי השניה. עבור כל מחרוזת:

* <math>F\vdash S</math>: כלומר יש הוכחה <math>x^*</math> ב־F לטענה S. אחרי זמן סופי M תמצא את ההוכחה, ותעצור. אבל אם הטענה S נכונה (הרי, מצאנו עבורה הוכחה!) הרי ש־M אינה עוצרת. מאידך יש לנו הוכחה שהיא כן עוצרת: סדרת הקונפיגורציות שמוצאת את <math>x^*</math> היא '''הוכחה''' ש־M כן עוצרת. במילים אחרות יש לנו שתי הוכחות: אחת של הטענה ש־M לא עוצרת, והשניה של הטענה ש־M כן עוצרת. הוכחנו טענה ושלילתה -<math>\leftarrow</math> '''F לא עקבית!''' בסתירה להנחה.

* <math>F\vdash \neg S</math>: כלומר יש הוכחה לכך ש־M לא עוצרת. מכיוון שהנחנו ש־F עקבית, לא ייתכן שקיימת הוכחה לכך ש־M כן עוצרת, כלומר, '''לא קיימת הוכחה ל־S'''. מכיוון שכך, המכונה M לעולם לא תעצור (כי לא קיים x שיגרום לא לעצור), אבל זו הרי סתירה לכך ש<math>\neg S</math> היא טענת-אמת (שהרי, הוכחנו אותה!).