על תורה העומדת על כריעות תרנגולת

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

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

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

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

נעבור כעת לדיון על מושג הכריעות. כדי להבין אותו יש להבין ממה מורכבת בעצם תורה מתמטית: ראשית, יש לנו שפה - אוסף סימנים בעלי משמעות מוסכמת שאיתם, ורק איתם, יוצרים משפטים והוכחות (למשל, לסימן “דני” אין משמעות בתורת המספרים הפורמלית; לסימן “+” יש). שנית, יש לנו כללי היסק - כללים שמתירים לנו להסיק מאקסיומות וממשפטים שכבר הוכחו משפטים נוספים. הדוגמה הקלאסית לכלל היסק היא “מודוס פוננס” (Modus Ponens), שאומר “אם הוכחת שקיום A גורר את קיום B, והוכחת את קיום A - אז הוכחת את קיום B”. נשמע סביר (וקל להוכיח את נכונותו תחת ההגדרה הסטנדרטית שלנו של “נכונות”). שלישית, יש לנו אקסיומות לוגיות - טענות בשפה שהן נכונות תמיד (טאוטולוגיות). למשל, “אם A מתקיים אז גם ‘B גורר A’ מתקיים” (בכתיב פורמלי: \( A\to (B\to A) \) - נסו לחשוב מדוע זה נכון, מה שיכול להיות בעייתי בגלל של-“A גורר B” יש משמעות שאינה אינטואיטיבית לגמרי).

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

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

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

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

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

השאלה האם קיים אלגוריתם שכזה או לא הפכה לבעלת עניין בזכות עצמה, עוד לפני גדל, והתהדרה בשם “Entscheidungsproblem” (“בעיית הכרעה” בגרמנית). כדי להתמודד איתה היה צורך ראשית להגדיר בצורה פורמלית מהו אלגוריתם (מושג שעד כה הזכרנו רק בקווים כלליים), ושני הראשונים להתמודד עם הבעיה הזו היו אלונזו צ'רץ' ואלן טיורינג. כל אחד מהם הציע פורמליזם משלו (שניהם שקולים זה לזה מבחינת כוחם החישובי), והוכיח עבור הפורמליזם הזה שבעיית ההכרעה היא בלתי פתירה. צ’רץ’ הקדים מעט את טיורינג, והמודל שלו (תחשיב הלמבדא) הוא בעל עניין גם בימינו, והיווה את ההשראה לחלק משפות התכנות המתוחכמות של ימינו (Lisp, ML, Haskell), אך המודל שזכה ל”הצלחה” גדולה יותר במרוצת הזמן הוא זה של טיורינג, אולי מכיוון שהוא כל כך דומה למחשבים המוכרים לנו (וחשוב לזכור שטיורינג המציא אותו עוד לפני שהיה מחשב). המודל הזה הוא “מכונת הטיורינג” המפורסמת שאני כל הזמן מתחייב שאגיע אליה, ובפוסט הבא אני נשבע שאעשה זאת.