משפטי אי השלמות של גדל - מה הם כן אומרים?

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

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

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

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

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

את המשמעות של תורות מספקים המודלים שלהן. מודל (בנפנוף ידיים פרוע) הוא קבוצה של אובייקטים מתמטיים שמותאמים לסמלים שבשפה ונותנים להם פרשנות אפשרית אחת (בדוגמה של הפוסט הקודם הבאתי את תורת החבורות, שבה הסימן \( \cdot \) שמסמן את פעולת החבורה יכול לקבל פרשנות של “חיבור מספרים שלמים” ופרשנות אחרת של “כפל מטריצות”). מכיוון שמודל הוא יצור “אמיתי”, אפשר לשאול את עצמנו האם טענות שמנוסחות בשפה הפורמלית אכן מתקיימות בפרשנות שמציע המודל (בפוסט הקודם הדוגמה הייתה הטענה הפורמלית \( \forall x,y\left(x\cdot y=y\cdot x\right) \) שהייתה נכונה בפרשנות של “מספרים שלמים” אך לא נכונה בפרשנות של “מטריצות”). כדי שמשהו יהיה מודל עבור תורה מסויימת צריך, מן הסתם, שהאקסיומות של התורה יהיו נכונות עבורו.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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