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

הקדמה

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

מספור גדל

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

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

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

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

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

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

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

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

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

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

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

באופן כללי הניסוח מסורבל מעט יותר, כאמור: אם $latex g_{1}\dots g_{n}$ כולן פונקציות רקורסיביות ב-$latex m$ משתנים, ו-$latex f$ היא פונקציה ב-$latex n$ משתנים, אז אפשר להגדיר כך פונקציה $latex h$ מ-$latex m$:$latex 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)$.

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

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

$latex 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)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

מה עוד נשאר?

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

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

שימו לב למה שקרה כאן כרגע – היינו חייבים להתבסס על עקביות התורה. אם היא לא הייתה עקבית, הרי שכן היה ניתן להוכיח את פסוק גדל שלנו, ולכן הטענה שהוא טוען הייתה שגויה. מכאן שלא מדויק לומר שהפסוק $latex G$ הוא "נכון" – יותר מדויק לומר שאם המערכת שלנו עקבית, אז הפסוק נכון. ההבחנה הזו קריטית, מכיוון שלפעמים מנסים לטעון ש"אנחנו יותר חכמים מהמערכת הלוגית" כי אנחנו יודעים ש-$latex G$ נכון בזמן שהיא לא יודעת זאת כי היא לא מסוגלת להוכיח זאת. דא עקא, אנחנו לא באמת יודעים ש-$latex G$ נכון; "לדעת" ש-$latex G$ נכון היה אומר שאנחנו יודעים שהמערכת שלנו היא עקבית, אבל אנחנו לא יודעים זאת!

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

24 תגובות בנושא “משפט אי השלמות הראשון של גדל – איך (בערך) מוכיחים אותו?”

  1. אני מניח שלא ניתן לנסח את פרדוקס השקרן ע"י הסכמה של גדל. האם נתקלת פעם בהתייחסות לרעיון?

  2. האמנם "משפט גדל" הוא משפט? אם הוא אכן משפט אזי הוא ניתן להוכחה, ואכן, זה מה שגדל טוען. האם הוא מתבסס על מערכת של מספר סופי של אקסיומות? כלומר מצאנו טענה הבנויה במערכת של מספר סופי של אקסיומות שטוענת שכל מערכת הבנויה על מספר סופי של אקסיומות איננה שלמה?….
    האם ניתן להפריך את משפט גדל. יתכן שמשפט גדל בלתי "כריע" ! וההוכחה מבוססת על "כשל מעגל הקסמים" שבו עסק ראסל – שבו אם פונקציה היא פרמטר של עצמה היא נכנסת ללולאה בלתי כריעה, כמו בעית העצירה של תוכנית מחשב, או כל פרדוקס אחר כמו פרדוקס השקרן או פרדוקס הספר, או הבעיה שהטרידה את קאנטור: האם "הכל" הוא הקבוצה.
    לפי גדל, כל תכנית מחשב ניתנת לביטוי ע"י "מספר גדל", כולל משפט גדל שבו תכנית ההוכחה מופעלת על עצמה כפרמטר באופן רקורסיבי.
    נכון, כל מה שכתבתי כאן הוא "סלט"…. אבל עדיין מטרידה אותי השאלה האם האם ניתן לקרוא "משפט" לטענה שמערערת על כל הפרובלמטיות של הוכחת משפטים.

  3. "מצאנו טענה הבנויה במערכת של מספר סופי של אקסיומות שטוענת שכל מערכת הבנויה על מספר סופי של אקסיומות איננה שלמה?…."

    אין עם זה שום בעיה. זה שמערכת אינה שלמה לא אומר שלא ניתן להוכיח בה דברים (מה גם שמשפט גדל לא אומר כלום על *כל* מערכת אלא רק על מערכות מסויימות – קרא את הפוסט שלי שמסביר זאת).

    את הרלוונטיות של שאר מה שאמרת לטיעון הזה (או משהו אחר שניסית לומר) לא הבנתי.

  4. וואו זה ממש מסובך אבל ממש אהבתי את הרעיון של הקידוד במספרים ראשוניים – זה מבריק!
    (דרך אגב, כבוד – הוא היה יהודי )

  5. תודה על המאמר. נהנתי לקרוא אותו.

    הפריע לי רק מה שכתוב בפסקה הלפני אחרונה: "מכאן שלא מדויק לומר שהפסוק G הוא "נכון" – יותר מדויק לומר שאם המערכת שלנו עקבית, אז הפסוק נכון."
    איך יכול להיות שהפסוק G הוא נכון, אם לפי משפט השלמות (שאותו גם כן הוכיח גדל) כל פסוק שהוא נכון (כלומר נכון בכל מודל שמספק את התורה) ניתן להוכחה?
    ואם אנחנו מתנים את נכונות G בעקביות המערכת, האם זה אומר שישנם מודלים שעבורם המערכת היא עקבית וישנם מודלים שעבורם היא אינה עקבית?

  6. ״נכון״ כאן במובן האינטואיטיבי, של ״אי אפשר להוכיח אותי״. לא במובן שציינת כאן (כי אכן, הפסוק אינו יכול להיות נכון – בעל ערך אמת סמנטי – בכל מודל של התורה).

  7. אם כך, זה מוביל אותי לשאלה הבאה:
    לפי מה שאמרת, יש מודל שעבורו G אינה נכונה. כלומר לפי המודל הזה קיים X כך ש: (|B(X,|G.
    נתרגם את ה-X הזה להוכחה שמוכיחה את G, בסתירה למשפט גדל. איך זה מסתדר?

  8. אני לא שוחה בחומר הזה כרגע ולכן ייתכן שאני טועה, אבל בשעתו כשניסיתי להבין את הנקודה הזו, המסקנה הייתה פשוטה: במודל שעבורו B(X,G) מתקיים, ה*משמעות* של B איננה אותה משמעות כמו במודל של הטבעיים; צריך לזכור שגדל מלכתחילה בונה את B כמעין תוכנית מחשב שבודקת הוכחה לטענה, והתוכנית הזו נכתבת תוך ההנחה שהיא פועלת על מספרים טבעיים.

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

  9. הפוסט מעולה, אבל יש לי הערה קצת קטנונית:

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

    הפונקציות שהגדרת(שבנויות מפונ' ה0, פונ' העוקב, פונ' ההיטל ומספר סופי של הרכבות ורקורסיות) נקראות פונקציות פרמיטיביות רקורסיביות כפי שציינת.

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

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

    אם תרצה אני יכול להעלות את קובץ הPDF של המרצה שלנו לחישוביות שמכיל את ההוכחה לגבי פונ' אקרמן.

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

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

  10. לשם הבהרה(ואולי תקציר למי שהתעצל):
    בין שתי סוגי הפונק' שהצגת קיים עוד סוג של פונ' שהן יותר חזקות מהרקורסיביות פרמיטיביות(אלו שרוב הפוסט סובב סביבן) אבל שלמות, הפונ' הנ"ל נוצרות ע"י הוספת כלל המינימיזציה ממש(ולא מינימיזציה) שהיא פונ' שלמה, מינימיזציה ממש היא פונ' שמוצאת את האיבר המינימלי שידוע לנו שקיים אבל לא ידוע לנו על חסם עבורו, ולכן לא ניתן לבנות לה פונ' רקורסיבית פרמיטיבית, אך היא שלמה.

    פונקציית אקרמן(וכמובן עוד אינסוף פונקציות אחרות כגון A(m,n)+1, A(m,n)+2, וכו') היא פונקציה רקורסיבית ושלמה אבל אינה רקורסיבית פרמיטיבית.

    מעבר לזה הפוסט מאלף.

  11. זו לא הייתה הכוונה שלי, זה היה רק חלק מהתגובה, הבעיה הייתה עם המשפט:

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

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

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

    מה שקורה כאן דומה לבניית בסיס המגדל על ראש המגדל.
    או שמא עליי להניח את "נכונות" ועקביות השפה המתמטית המורכבת יותר (כמו זו שגדל משתמש בה) ולהגדיר בעזרתה את המערכת הטהורה בלי לשאול שאלות?

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

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

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

    הערה קטנה, בהגדרה של פעולת הרקורסיה, בנוסחה שרשמת שמגדירה את h(0,…) ו-h(n+1,…) השוויון האמצעי לפי מה שהבנתי אמור להיות פסיק או משהו דומה.

    תודה רבה!

  15. במשפט הזה:
    אז φ(|φ|) הוא פסוק שמתקבל מלקיחת φ והצבת המספר |y| בכל מקום שבו כתוב y ב-φ.

    מופיע |y| במקום |φ|.

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

  17. יש שתי נקודות שאשמח אם תוכל להסביר לי, שתיהן נוגעות ליכולות שנראה לי שגדל "הוסיף" למתמטיקה, שלא היו לה :
    1. ההתאמה בין מספר לסדרת תווים באלף-בית של השפה שהוא תוקף. יש כאן עליה למטא, שלא ברור מדוע היא מותרת. למשל, העלה בדעתך פונקציה המקבלת ספרות, ומחזירה 0 אם יש בצורת הספרה קו מעוגל, ו- 1 אם יש בה רק קוים ישרים.
    2. הפונקציה B מצריכה תו בשפה עבור יחס, שלא היה קיים בה : ' הוכחה של '. בלי היחס הזה, אי אפשר להגדיר אותה.

    משהוספת יכולת רפלקסיה, ואת היחס ' הוכחה של ', אפשר לכתוב את פרדוקס השקרן.

כתיבת תגובה

האימייל לא יוצג באתר. שדות החובה מסומנים *