משפט אי השלמות הראשון של גדל - איך (בערך) מוכיחים אותו?

הקדמה

הרעיון המפורסם ביותר בהוכחת משפט אי השלמות הראשון של גדל (איני חושב שאוכיח כאן את השני, לפחות לא כעת) הוא הרעיון של לכסון - שיטה ששימשה כבר את גאורג קנטור בהוכחה שלו לכך שעוצמת הממשיים אינה שווה לעוצמת הטבעיים. כמעט בכל תיאור של משפט גדל מזכירים את הדמיון שלו לפרדוקס השקרן (הפרדוקס שבו איש כרתים אומר “כל אנשי כרתים משקרים תמיד”, ולכן לא ברור אם הוא אומר את האמת או משקר), ולעתים אף מגדילים לעשות ומסבירים עד כמה גאוני היה מצד גדל לחשוב על להשתמש בו - אך כאמור, קנטור כבר עשה זאת זמן מה קודם לכן. לדעתי, הגאונות האמיתית של גדל היא ברעיון, שכיום נראה אולי פשוט וברור לחלוטין - בפרט לבקיאים במדעי המחשב - להשתמש בנוסחאות שלכאורה מדברות רק על מספרים טבעיים כדי לתאר מערכות הוכחה, ולא סתם מערכות הוכחה אלא את אלו שבתוכן הנוסחאות הללו “חיות”. ברעיון הזה אפשר להתחיל את תיאור ההוכחה של גדל.

מספור גדל

הבה ונזכור מהי הוכחה - סדרה של טענות, כשכל טענה היא סדרה של תווים מעל אלף-בית כלשהו של סימנים. לא כל סדרת תווים היא חוקית - יש כללים שקובעים אילו סדרות הן חוקיות (לסדרות כאלו, שמהוות טענה חוקית, לפעמים קוראים “Well formed formula” ומייד מקצרים ל-wff והופכים את יתר הטקסט לבלתי קריא) ואילו לא. מה שגדל מציע הוא לקודד כל טענה באמצעות מספר באופן הבא: ראשית, לכל תו באלף-בית נצמיד מספר טבעי - כך למשל “\( \wedge \)” שמסמל “וגם” יכול לקבל את המספר 3, בעוד “\( x \)” שהוא משתנה יכול לקבל 5 (יש אינסוף משתנים, אבל זו לא בעיה - כל משתנה יקבל מספר אחר. באופן כללי, אם \( t \) הוא סימן כלשהו, אז \( g\left(t\right) \) יהיה הערך שגדל מתאים לו.

עכשיו, בהינתן פסוק, למשל \( x\wedge\neg z \), אפשר להתאים לו מספר באופן הבא: \( 2^{g\left(x\right)}\cdot3^{g\left(\wedge\right)}\cdot5^{g\left(\neg\right)}\cdot7^{g\left(z\right)} \). כלומר, המספר שמותאם לפסוק הוא מכפלה של ראשוניים, כאשר החזקה של הראשוני ה-\( k \)-י במכפלה היא הערך המספרי שהותאם לתו ה-\( k \)-י באותו פסוק. השימוש בראשוניים נובע מכך שלכל מספר יש פירוק יחיד לראשוניים, כך שלא ייתכן ששתי מכפלות שונות של ראשוניים יתנו את אותו מספר, ולכן כל פסוק מקודד באופן ייחודי.

בימינו, הרעיון הזה נמצא בשימוש בכל מחשב, כל הזמן; הדוגמה הקלאסית שלו היא קוד ASCII, שבו מקודדים 256 תווים שונים באמצעות מספרים מ-0 ועד 255. כל מחרוזת של תווים מקודדת כעת באמצעות רצף של מספרים שכאלו, וכשמחשב פותח קובץ טקסט הוא קורא את המספר הגדול מאוד שמהווה את הקידוד, ומתרגם אותו חזרה לסדרת תווים. גדל לא הכיר מחשבים ואת שיטת הקידוד ASCII, כמובן; בזמנו הם כלל לא היו קיימים. איני יודע אם הוא המציא את רעיון הקידוד באופן כללי - אני מניח שלא, ובכל זאת, הקרדיט על הרעיון של קידוד טענות פורמליות שמדברות על מספרים באמצעות מספרים, מה שמאפשר לטענות לדבר “על עצמן” - הקרדיט הזה ניתן לגדל במלואו.

באופן דומה לזה שבו מקודדים פסוקים, אפשר לקודד הוכחות שלמות - פשוט קחו את 2 בחזקת הקידוד של הפסוק הראשון בהוכחה, כפול 3 בחזקת הקידוד של הפסוק השני בהוכחה, וכן הלאה. מכיוון שכל הוכחה היא סופית, זה עובד - ושוב, למי שמכיר קידודים במחשב בימינו כל הדיון הזה נשמע קצת מיותר, ושיטת הקידוד של גדל - קצת מסורבלת.

פונקציות רקורסיביות

המושג הבא שגדל מדבר עליו הוא פונקציות רקורסיביות. בימינו, המשמעות המוכרת של “פונקציה רקורסיבית” היא של פונקציה בתוכנית מחשב שמבצעת קריאה לעצמה (איך זה אפשרי? בשביל מה זה טוב? זה עניין לפוסט אחר). גדל, כמובן, מתכוון למשהו קצת שונה - כפי שנראה, שם יותר מתאים לפונקציות הללו הוא למעשה “פונקציות ניתנות לחישוב” - למשל, לחישוב על ידי מחשב, או אלגוריתם, או מכונת טיורינג, או אדם עם נייר ועט וסבלנות, אך זהו מושג שלא היה קיים בתקופת גדל; למרות שהרעיון של בניית פונקציות באופן רקורסיבי לא היה חדש, הפורמליזם המדוייק שגדל השתמש בו, והצליח לתפוס בצורה (כמעט) מדוייקת את הרעיון של “ניתן לחישוב”, הוא (ככל שהצלחתי לברר) המצאה שלו, ואחד מהרעיונות המבריקים שבמאמר. אתאר כעת את הפורמליזם הזה.

באופן כללי, הדיון עוסק בפונקציות מהמספרים הטבעיים לטבעיים. כדי להקל על החיים, מרשים לפונקציה לקבל ולהחזיר סדרות סופיות של טבעיים, כלומר באופן כללי אנחנו מדברים על פונקציה \( f:\mathbb{N}^{n}\to\mathbb{N}^{m} \). ההגיון הוא שכל דבר שניתן לחישוב ניתן לתאר (באמצעות קידוד מתאים) כחישוב על טבעיים - ואכן, זה גם מה שגדל עושה - מתרגם פונקציות על טענות והוכחות (למשל, פונקציה שמחזירה 1 רק אם הוכחה מסויימת היא תקפה) לפונקציות על מספרים טבעיים.

מגדירים את הפונקציות הרקורסיביות באינדוקציה - מתחילים מפונקציות בסיס פשוטות מאוד, ובונים באמצעותן פונקציות מורכבות יותר. פונקציות הבסיס הן:

1. הפונקציה הקבועה אפס: \( f\left(x_{1},\dots,x_{n}\right)=0 \) (לכל\( n \) טבעי, כלומר \( f\left(x\right)=0 \), וגם \( f\left(x_{1},x_{2}\right)=0 \) וכו').
2. פונקצית העוקב: \( g\left(x\right)=x+1 \).
3. פונקצית ההטלה על הרכיב ה-\( i \): \( h_{i}\left(x_{1},\dots,x_{n}\right)=x_{i} \)

כל אלו הן פונקציות פשוטות למדי. אם אתם יודעים לתכנת, תוכלו לתכנת אותן ללא קושי רב. אם כן, בינתיים הפונקציות מתאימות היטב להגדרה של “ניתן לחישוב”. ומה הלאה?

דרך אחת לבנות פונקציות חדשות מהישנות היא הרכבה. הניסוח הפורמלי מעט מסורבל, ולכן קודם כל דוגמה למקרה פשוט: אם יש לנו שתי פונקציות רקורסיביות,\( f\left(x\right),g\left(x\right) \), אז אפשר לבנות פונקציה חדשה שמסמלת קודם כל הפעלה של \( g \) ואחרי הפעלה של \( f \). בכתיבה פורמלית,\( h\left(x\right)=f\left(g\left(x\right)\right) \). די בבירור אם\( f,g \) ניתנות לחישוב, גם \( h \) ניתנת לחישוב (קודם כל מחשבים את \( g\left(x\right) \), ואז מחשבים מה \( f \) מחזיר על התוצאה).

באופן כללי הניסוח מסורבל מעט יותר, כאמור: אם \( g_{1}\dots g_{n} \) כולן פונקציות רקורסיביות ב-\( m \) משתנים, ו-\( f \) היא פונקציה ב-\( n \) משתנים, אז אפשר להגדיר כך פונקציה \( h \) מ-\( m \):\( h\left(x_{1},\dots,x_{m}\right)=f\left(g_{1}\left(x_{1},\dots,x_{m}\right),\dots,g_{n}\left(x_{1},\dots,x_{m}\right)\right) \).

הבניה המרכזית והמעניינת ביותר, שנתנה לפונקציות את שמן, היא הרקורסיה. במשמעות ה”רגילה” של המילה, פונקציה רקורסיבית היא כזו שמוגדרת באמצעות עצמה, אך על קלט פשוט יותר. למשל, \( f\left(n\right)=f\left(n-1\right)+f\left(n-2\right) \) היא פונקציה רקורסיבית (שמגדירה את מספר פיבונאצ’י ה-\( n \)-י) כדי שיהיה טעם ברקורסיה, חייבים להיות מוגדרים לה “תנאי עצירה” - הגדרה מפורשת של ערכיה כאשר הקלט קטן דיו. עבור פיבונאצ’י, למשל, הגדרה אפשרית אחת היא \( f\left(0\right)=0,f\left(1\right)=1 \).

פורמלית, פעולת הרקורסיה מוגדרת כך. נניח שיש לנו פונקציה רקורסיבית (במובן של “ניתנת לחישוב”) \( f\left(y,z,x_{1},\dots,x_{n}\right) \) ופונקציה רקורסיבית \( g\left(x_{1},\dots,x_{n}\right) \) (זוהי הפונקציה של “תנאי ההתחלה”), אז אפשר להגדיר פונקציה רקורסיבית חדשה \( h\left(y,x_{1},\dots,x_{n}\right) \) באופן הבא:

\( h\left(0,x_{1},\dots,x_{n}\right) = g\left(x_{1},\dots,x_{n}\right) = h\left(n+1,x_{1},\dots,x_{n}\right) = f\left(n,h\left(n,x_{1},\dots,x_{n}\right),x_{1},\dots,x_{n}\right) \)

אם כן, \( h\left(n,x_{1},\dots,x_{n}\right) \) פירושו “\( h \) עבור הערך \( n \) והפרמטרים הקבועים \( x_{1},\dots,x_{n} \)”. כאשר הערך \( n=0 \), אז \( h \) פשוט מחזירה את תנאי ההתחלה, וכאשר הוא גדול יותר מחזירים את מה ש-\( f \) נותנת, שמתבסס על \( n \), על \( x_{1},\dots,x_{n} \), ועל הערך הקטן יותר של \( h \).

זהו פורמליזם קצת מתוסבך, אבל עם קצת מחשבה אפשר להבין מה קורה בו, ולראות שזה די קל לתכנת גם דבר שכזה, ולכן גם פונקציות שנבנות כך הן ניתנות לחישוב.

רק אחרי גדל, כאשר מודלים פורמליים של אלגוריתמים (למשל, מכונת טיורינג) פותחו ניתן היה להוכיח פורמלית גם את הכיוון ההפוך - שהפונקציות הרקורסיביות הן כל מה שניתן לחישוב. איני מדייק כאן עד הסוף - מה שתיארתי עד כה נקרא בימינו “פונקציות רקורסיביות פרימיטיביות”, שכן ניתן להוסיף עוד כלל בנייה אחד - כלל המינימיזציה - ולקבל מחלקה רחבה יותר של פונקציות, אך כאלו שאינן בהכרח מוגדרות לכל קלט. ארחיב על כך בפוסט נפרד, אך לעת עתה אין בכך צורך; די בכך שאומר שאפשר להוכיח שכל תוכנית מחשב שמקבלת כקלט סדרת מספרים טבעיים, עוצרת לכל קלט אפשרי ומוציאה כפלט סדרת מספרים טבעיים - כל תוכנית מחשב שכזו ניתן לתאר באמצעות פונקציה רקורסיבית. זו תוצאה די מפתיעה - הרבה יותר מפתיעה מאשר “מכונת טיורינג יכולה לחשב את כל מה שתוכנית מחשב יכולה” (מה שמעיד על כך שמכונת טיורינג היא פורמליזם טוב) - וההוכחה שלה אינה טריוויאלית.

בזמנו של גדל, כמובן, כל זה לא היה ידוע. זו הסיבה שבגללה השלב הבא בהוכחה שלו הוא כל כך טכני ומורכב. מה שגדל רוצה לעשות כעת הוא לבנות פונקציה רקורסיבית \( B\left(x,y\right) \) שמחזירה 1 אם המספר הטבעי \( x \) הוא קידוד של הוכחה עבור הטענה שמקודדת על ידי המספר\( y \) (למעשה, גדל מגדיר יחס ולא פונקציה, אך שני המושגים שקולים זה לזה ולא אתעמק בהבחנה הזו). אם אנחנו יודעים שקיימת פונקציה רקורסיבית עבור כל תוכנית מחשב, הקיום של \( B \) אינו מפתיע במיוחד - בהינתן \( x,y \), זה עניין טכני ומכני בלבד לפענח את הקידוד של \( x \) ולקבל סדרה של טענות, ואז זה עניין טכני ומכני בלבד לבדוק שכל טענה בסדרה היא או אקסיומה או נובעת מקודמותיה, ושהפסוק האחרון בסדרה הוא מה ש-\( y \) מקודד; זה בדיוק המקום שבו נדרש ממערכת ההוכחה להיות אפקטיבית, כך שבדיקה שכזו תהיה אפשרית בכלל - אם המערכת לא הייתה אפקטיבית, ככל הנראה הפונקציה\( B \) המדוברת לא הייתה רקורסיבית (כמובן, עדיין ניתן היה להגדיר את \( B \) באופן מילולי; פשוט לא היינו יכולים לעשות בה את השימוש שגדל עושה אחר כך, ומצריך ממנה להיות רקורסיבית).

לרוע מזלו של גדל, נפנוף הידיים שלעיל מן הסתם לא היה קביל עבורו. התוצאה היא שהוא בונה את \( B \) באופן מפורש ומדוייק, תוך עבודה צמודה עם ההגדרות שלעיל של כללי הבניה של פונקציות רקורסיביות. הבנייה היא הדרגתית - בכל פעם הוא בונה פונקציות רקורסיביות יותר ויותר מורכבות, שעליהן ניתן לבנות פונקציות עוד יותר מורכבות, וכן הלאה, עד שבסופו של דבר, לאחר לא פחות מ-45 צעדים (שכל אחד מהם דורש רק שורה או שניים, אמנם) הוא מגיע אל \( B \) הנכספת. כאשר מוכיחים את משפט גדל לסטודנטים ללוגיקה, זה לרוב החלק בהוכחה שכולל הרבה נפנופי ידיים או הנחות לא מוכחות - ולדעתי בצדק, כי אין בבנייה הזו שום דבר מחכים לכשעצמה. גדל פשוט תכנת באסמבלי של המתמטיקה (יותר מדוייק לומר “באסמבלי של תורת החישוביות”), לפני שהיו קיימות שפות עיליות. מבחינה טכנית זה מרשים מאוד, כמובן.

ייצוג הפונקציות הרקורסיביות

אוקיי, אז גדל הראה שאותה \( B\left(x,y\right) \) היא רקורסיבית. מה עכשיו? כעת גדל מגיע לפאנץ’ ליין של השימוש בפונקציות רקורסיביות - הוא מראה שבתורה שאותה הוא “תוקף”, אפשר לייצג את הפונקציות הללו. המשמעות המדוייק של הייצוג הזה היא מעט טכנית ולא אכנס אליה, ולכן לצורך העניין ניתן לחשוב על כך (באופן לא מדוייק לגמרי) כאילו ניתן להשתמש בפונקציות רקורסיביות בצורה חופשית בפסוקים של התורה, כאילו הן היו חלק מהשפה עצמה. גדל אמנם מראה זאת רק עבור תורה ספציפית - זו של ראסל וויטהד - אבל בהמשך הוא מראה כי די בפעולות החיבור והכפל ה”סטנדרטיות”: כדי שאפשר יהיה להגדיר את הפונקציות הרקורסיביות. זו נקודה מעניינת, ולכן אני רוצה להתעכב גם עליה.

פונקציה רקורסיבית בסיסית, כמו \( f\left(x\right)=0 \) קל לייצג, כי יש לנו סימן עבור 0 בשפה; ובדומה, גם \( f\left(x\right)=x+1 \) קל לייצוג כי יש לנו בשפה סימן עבור עוקב. גם הטלות והרכבות לא קשה לייצג - האתגר האמיתי הוא פעולת הרקורסיה (שהיא, כאמור, הפעולה עם ה”בשר” כאן). בנפנוף ידיים, מה שצריך לעשות כדי לייצג פונקציה שנבנתה ברקורסיה, הוא לבנות פסוק שאומר “קיימת סדרת ערכים, כך שהערך הראשון מתקבל מבסיס הרקורסיה, וכל ערך גדול יותר מתקבל מקודמו על ידי הפעלת פונקצית הרקורסיה, והערך האחרון הוא הפלט של הפונקציה” (קצת מזכיר הוכחה פורמלית, לא?). האתגר שבבניית פסוק שכזה הוא בדיוק בטענת ה”קיימת סדרה” - הרי בלוגיקה מסדר ראשון אין דרך לכמת קבוצות של איברים, וסדרה היא קבוצה שכזו. כל מה שניתן לעשות הוא לטעון טענות “קיים מספר”, לא “קיימת סדרת מספרים”. אז איך עוקפים את זה?

התשובה היא שכל עוד הסדרה היא סופית, אפשר לקודד אותה באמצעות מספר בודד, ואז כל מה שצריך לעשות כדי לדבר על איברים ספציפיים בסדרה הוא “לפתוח את הקידוד” ולהתייחס למקום המתאים. הרעיון הזה נשמע מאוד דומה לרעיון של קידוד גדל - ושוב, לא במקרה - ולצורך הביצוע שלו גדל שולף מהשרוול טריק מתמטי אחד או שניים ומגדיר את מה שמכונה “פונקצית ה-\( \beta \) של גדל”. הפונקציה הזו מעניינת בכך שהיא ניתנת לייצוג באמצעות פעולות חיבור וכפל בלבד (אבל שתי הפעולות הללו הן הכרחיות, ולכן בלי פעולת כפל כל ההוכחה קורסת), והיא אכן מממשת בצורה מקסימה את רעיון ה”קידוד של כל הסדרות הסופיות”. לא אתן כרגע תיאור מדוייק של הפונקציה, אך ייתכן שאקדיש לה פוסט בהמשך - רק אומר שהרעיון הבסיסי של הקידוד מתבסס על משפט עתיק יומין ויפה שכבר הזכרתי כאן - משפט השאריות הסיני.

אם כן, סיכום ביניים: גדל משתמש בפונקצית ה-\( \beta \) כדי להראות שכל הפונקציות הרקורסיביות ניתנות לייצוג בכל תורה אריתמטית. הוא כבר הראה שבכל תורה אפקטיבית, הפונקציה \( B\left(x,y\right) \) של “\( x \) היא הוכחה ל-\( y \)” היא רקורסיבית. משני אלו עולה שהיא ניתנת לייצוג בתורה שהיא אריתמטית ואפקטיבית. כעת הגענו לישורת האחרונה.

שובו של האלכסון

החלקים הטכניים של ההוכחה כבר פחות או יותר מאחורינו - כל מה שנותר הוא רעיון חדש אחד או שניים, שניתנים להבנה גם עבור מי שלא בקיא בפרטים הקטנים של מה שהלך עד כה. ראשית כל ננסה לתת את המוטביציה להגדרה החדשה. יש לנו כבר יכולת לומר “\( x \) הוא הוכחה ל-\( y \)” והיינו רוצים לבנות פסוק \( G \) שאומר “אין הוכחה עבורי”. כעת, כל נוסחה \( \varphi \) מיוצגת, כזכור, על ידי מספר - זהו מספור גדל המדובר. נסמן את המספר הזה בתור \( \left|\varphi\right| \). אם כן, מדוע לא לבנות את הפסוק הבא: \( G=\forall x\left(\neg B\left(x,\left|G\right|\right)\right) \)? כלומר, \( G \) הוא הפסוק שאומר “לא קיים \( x \) שהוא הוכחה עבורי” - זה יסיים את העניין.

לרוע המזל, ההפניה העצמית שאנו כל כך אוהבים פונה כאן כנגדנו. שימו לב איך הגדרתי את הפסוק \( G \): חלק ממנו הוא \( \left|G\right| \), שהוא מספר טבעי שמיוצג בתורה שלנו באמצעות הפעלות חוזרות ונשנות של פונקצית העוקב על 0 - כלומר, זו מחרוזת ארוכה ומסובכת. מצד שני, הערך המספרי שאותה מחרוזת מייצגת הוא משהו שכדי לחשב אותו עלינו כבר לדעת את כל הנוסחה \( G \); במילים אחרות, ההגדרה שלנו היא מעגלית - כל עוד לא כתבנו במפורש את \( G \) אין משמעות ל-\( \left|G\right| \), אבל מבלי שתהיה משמעות ל-\( \left|G\right| \) אי אפשר לכתוב את \( G \)! בקיצור, נתקענו, ואנו זקוקים לתעלול כדי לפתור את הבעיה. תעלול שכזה הוא בדיוק מה שגדל מספק; בסופו של דבר הוא יאפשר, בצורה עקיפה, להציב את \( \left|G\right| \) בתוך \( G \).

ראשית, בואו נבהיר הגדרה חשובה אחת: “פסוק” פירושו של דבר שאין בו משתנים שאינם נופלים תחת כמת כלשהו. למשל, \( \varphi=\forall x,y\left(x+y=y+x\right) \) הוא פסוק; לעומת זאת, \( \varphi^{\prime}=x+y>0 \) אינו פסוק. ההבדל מהותי: ל-\( \varphi \) יש ערך אמת מוגדר, או שהוא נכון, או שלא. לעומת זאת, ערך האמת של \( \varphi^{\prime} \) תלוי בערכים הספציפיים של\( x,y \) ש”נציב” בו.

נניח לרגע שיש לנו נוסחה \( \varphi \) שמכילה בדיוק משתנה חופשי אחד \( y \). אז \( \varphi\left(\left|\varphi\right|\right) \) הוא פסוק שמתקבל מלקיחת \( \varphi \) והצבת המספר \( \left|y\right| \) בכל מקום שבו כתוב \( y \) ב-\( \varphi \). זכרו שבשפה שלנו ניתן לתאר כל מספר טבעי, על ידי הפעלה של פונקצית העוקב מספר סופי של פעמים, ולכן \( \varphi\left(\left|\varphi\right|\right) \) הוא פסוק חוקי בשפה. הפסוק הזה מכונה “הלכסון של \( \varphi \)”, וכאמור - ערכו הוא אמת אם ורק אם כאשר מציבים את \( \left|\varphi\right| \) בתוך \( \varphi \) מקבלים אמת. אם כן, עקפנו במובן מה את הקושי של הצבת מספר גדל של נוסחה “בתוך עצמה” - אבל המחיר ששילמנו הוא בזה שמספר גדל של הפסוק \( \varphi\left(\left|\varphi\right|\right) \) שונה מזה של \( \varphi \).

דוגמה טיפשית: נניח ש-\( \varphi=\exists x\left(y>x\wedge2\cdot y<x\right) \). נניח שאחרי חישובים קשים מצאנו כי \( \left|\varphi\right|=1231 \) (מספר מפוברק, כמובן). אז \( \varphi\left(\left|\varphi\right|\right)=\exists x\left(1231>x\wedge2\cdot1231<x\right) \), וזהו פסוק שיש לו או ערך אמת, או ערך שקר. כאן אנחנו מתחילים לראות את ההתייחסות העצמית המדוברת של משפט גדל - אפשר לשאול את \( \varphi \)“מה אתה אומר על עצמך?”. אלן טיורינג ישתמש בדיוק ברעיון הזה מספר שנים לאחר מכן, ולא במקרה, אלא בהשראת הרעיון הזה של גדל.

מה בעצם משמעות המילה “לכסון” כאן? הנה אינטואיציה. חשבו על טבלה שבה לכל נוסחה במשתנה אחד \( \varphi\left(y\right) \) יש שורה, ולכל מספר טבעי שמתאים לנוסחה שכזו יש עמודה. בעמודה \( n \) בשורה של \( \varphi \) יהיה 1 אם \( \varphi\left(n\right) \) מקבל ערך אמת, ו-0 אחרת. כעת, אם נסדר את הנוסחאות \( \varphi \) על פי סדר הגודל של מספרי גדל שלהם, הרי שהערכים של \( \varphi\left(\left|\varphi\right|\right) \) יהיו בדיוק האלכסון של הטבלה.

כאמור, גם הלכסון של \( \varphi \) הוא נוסחה, ולכן יש לו מספר גדל משל עצמו. זה פותח פתח להגדרת הפונקציה הבאה: \( diag\left(n\right)=k \) אם \( k \) הוא מספר גדל של הלכסון של הנוסחה \( \varphi \) שעבורה \( \left|\varphi\right|=n \). כלומר, אם נתנו לנו \( n \) אנחנו “מפענחים” את הנוסחה \( \varphi \) שהוא מקודד, כותבים פורמלית את הנוסחה \( \varphi\left(\left|\varphi\right|\right) \) (שכאמור, שונה פיזית מהנוסחה \( \varphi\left(y\right) \) - סדרת הסמלים שמרכיבים אותה שונה, ולכן מספר גדל שלה יהיה שונה), מקודדים אותה בחזרה ומוציאים כפלט את המספר. ההסבר הזה הוא גם “אלגוריתם” לחישוב הפונקציה, ומכאן שהיא פונקציה רקורסיבית, ומכאן שהיא ניתנת לייצוג בתורה. בזאת סיימנו לדבר על הכלי החזק ביותר שבו נשתמש.

כעת נקשור את שני הרעיונות המרכזיים של גדל - הלכסון, והפונקציה \( B\left(x,y\right) \). נגדיר את הנוסחה הבאה: \( U\left(y\right)=\forall x\neg B\left(x,diag\left(y\right)\right) \). הנוסחה הזו אומרת “לא קיימת הוכחה לפסוק שמיוצג על ידי המספר\( diag\left(y\right) \)”. אנחנו כבר ממש ממש שם, נשארה רק עוד הגדרה אחת, אחרונה, שהיא הטוויסט הסופי - מה שמקבלים כאשר מלכסנים את \( U \) עצמה.

אם כן, נגדיר \( G=U\left(\left|U\right|\right) \). הנוסחה \( G \) הזו היא היעד הסופי שלנו - זה הפסוק שאינו ניתן להוכחה ועם זאת הוא נכון. ראשית, ברור שמדובר בפסוק, כי אין בו משתנים חופשיים. שנית, מה בעצם הוא אומר? הפסוק מקבל ערך אמת אם ורק אם הערך של \( U \) על \( \left|U\right| \) הוא אמת; אבל \( U \) מקבל ערך אמת על \( \left|U\right| \) אם ורק אם לא קיימת הוכחה לפסוק שמיוצג על ידי המספר \( diag\left(\left|U\right|\right) \). אבל מה זה הפסוק הזה? נזכר בהגדרה: \( diag\left(\left|U\right|\right) \) הוא מספר גדל של הלכסון של \( U \), כלומר של הפסוק \( G=U\left(\left|U\right|\right) \). כלומר, בסיכומו של דבר קיבלנו ש-\( G \) מקבל ערך אמת אם ורק אם לא קיימת הוכחה לפסוק שמיוצג על ידי \( G \) - זהו הניסוח הפחות או יותר מדוייק לתיאור האינטואיטיבי של “\( G \) אומרת שאין לה הוכחה”.

וואו. בכל פעם שבה אני מגיע לשלב הזה בהוכחה, אני צריך לעצור ולשאוף קצת אוויר. אף שהרעיון של לכסון אינו חדש, גדל בהחלט הביא אותו כאן לכדי שלמות.

מה עוד נשאר?

למרות שבנינו את \( G \), עדיין לא סיימנו. הטיעון שנתתי לעיל, של “\( G \) אומרת שאין לה הוכחה” הוא טיעון בנפנופי ידיים - טיעון “סמנטי” שמתבסס על המשמעות שאני מייחס ל-\( G \). עבור הוכחה פורמלית צריך להראות ממש שלא ניתן להוכיח את \( G \). בסימון פורמלי, \( \vdash\varphi \) אומר “ניתן להוכיח את \( \varphi \)”. אם כן, אנו רוצים להראות כי \( \not\vdash G \). נניח אם כן כי \( \vdash G \); כלומר, קיימת הוכחה של \( G \) במערכת שלנו, ולכן לאותה הוכחה קיים מספר גדל כלשהו, נניח \( m \); מכאן שמתקיים \( B\left(m,\left|G\right|\right) \), כלומר מתקיים \( B\left(m,diag\left(\left|U\right|\right)\right) \) (כל זה - על פי ההגדרות). כעת, לא ממש הסברתי עד הסוף מה זה אומר ש-\( B \)“מיוצגת” בתורה שלנו, אבל אחת מההשלכות של ה”ייצוג” הזה הוא שמתקיים \( \vdash B\left(m,diag\left(\left|U\right|\right)\right) \).

מצד שני, \( G=\forall x\neg B\left(x,diag\left(\left|U\right|\right)\right) \) על פי הבניה שלנו, ולכן \( \vdash\forall x\neg B\left(x,diag\left(\left|U\right|\right)\right) \); מכללי ההיסק הסטנדרטיים נובע ש-\( \vdash\neg B\left(m,diag\left(\left|U\right|\right)\right) \) (אם ניתן להוכיח שזה קורה לכל \( x \), ניתן להוכיח שזה קורה ספציפתי עבור \( x=m \)). לכן קיבלנו שהמערכת שלנו מוכיחה משפט ושלילתו - סתירה לכך שהיא עקבית.

שימו לב למה שקרה כאן כרגע - היינו חייבים להתבסס על עקביות התורה. אם היא לא הייתה עקבית, הרי שכן היה ניתן להוכיח את פסוק גדל שלנו, ולכן הטענה שהוא טוען הייתה שגויה. מכאן שלא מדויק לומר שהפסוק \( G \) הוא “נכון” - יותר מדויק לומר שאם המערכת שלנו עקבית, אז הפסוק נכון. ההבחנה הזו קריטית, מכיוון שלפעמים מנסים לטעון ש”אנחנו יותר חכמים מהמערכת הלוגית” כי אנחנו יודעים ש-\( G \) נכון בזמן שהיא לא יודעת זאת כי היא לא מסוגלת להוכיח זאת. דא עקא, אנחנו לא באמת יודעים ש-\( G \) נכון; “לדעת” ש-\( G \) נכון היה אומר שאנחנו יודעים שהמערכת שלנו היא עקבית, אבל אנחנו לא יודעים זאת!

אני לא רוצה לתת את הרושם הלא נכון - ה”הוכחה” שכתבתי פה היא לא יותר מאשר ערב רב של נפנופי ידיים לא מדויקים. הפרטים הטכניים של ההוכחה רבים ומורכבים יותר, וישנן נקודות עדינות רבות שלא הזכרתי או שאולי אף איני מכיר (או שם אליהן לב) בעצמי. בפרט, שימו לב שלא הוכחתי בכלל כי בתורה שלנו לא ניתן להוכיח את השלילה של \( G \)! (הסיבוך הטכני שמתקשר להוכחה הזו לא שווה את זה, במסגרת הפוסט הזה). עם זאת, אני מקווה שאת רוח ההוכחה ורעיונותיה המרכזיים עלה בידי להעביר.