|
||||
|
||||
"שום שפה פורמלית איננה שלמה, כלומר לכל שפה פורמלית תמיד יהיו הוכחות שלא יהיה ניתן לנסח בה" יותר במדויק, לכל שפה פורמלית יש *טענה* (נקרא לה "טענת-גדל") שהיא נכונה אך לא ניתן להוכיחה באותה שפה. אבל האם בני אדם יכולים לראות את נכונות טענות גדל? לא! לא רק שבני אדם לא יכולים לראות את נכונות טענות-גדל, הם לא יכולים לראות את הטענות בכלל. בפרט, גדל הראה איך בונים טענת-גדל עבור "פרינקיפה מתמטיקה", ושכנע אותנו שהטענה קיימת, אבל לא הראה את הטענה עצמה. הסיבה היא, כמובן, שהטענה ארוכה מכפי תפיסת אנוש. במונחי הורסיה שלך, טענת-גדל (ובוודאי הוכחה שלה) לא ניתנת להבעה בשפה טבעית, כי בשפה טבעית מבעים חייבים להיות מוגבלים באורכם (בהתחשב בדרישתך ששפה טבעית תהיה משהו שאנשים מבינים). אותה התנגדות תקפה, בשינויים הנדרשים, גם לורסיה המקורית של לוקאס, וגם לזו של פנרוז. |
|
||||
|
||||
המשפט של גדל הוא קונסטרוקטיבי. יש הרבה משפטי קיום במתמטיקה שמוכיחים שקבוצה מסוימת קיימת מבלי להציג שום בנייה מפורשת, אבל המשפט של גדל איננו אחד מהם. יש בו תיאור מדוקדק, אלגוריתמי, של האופן בו נבנית הטענה שאיננה נתנת להוכחה בשפה הפורמלית הנתונה (אקסיומות וכללי הסק). כל פעולה חישובית סופית היא בתחום "תפיסת אנוש", ללא תלות באורכה (למעשה, ההגדרה של "תהליך חישובי" תלויה בכך, למשל בהקשר לתזת צ'רצ'-טיורינג). היא אולי לא בתחום "סבלנות אנוש", "אורך חיי אנוש" וכדומה, אבל כל אלו לא קשורים לתפיסה. אילו היית יכול לתרגם את התפיסה המתמטית האנושית לאלגוריתם, לאלגוריתם זה לא היו שום מגבלות טכניות מהסוג הנ"ל. הוא יכול היה לטפל גם בטענת-גדל עבור הפרינקיפיה מתמטיקה, והיית יכול להפעיל עליו את הטיעון של לוקאס. ואם אתה בכל זאת מתעקש שלמגבלות הסבלנות והערנות האנושית יש איזה קשר מהותי לתפיסתו המתמטית, הנה פתרון אלטרנטיבי שמנטרל את הבעייה לחלוטין. למחשב (או, ליתר דיוק, למכונת טיורינג) אין שום בעייה לטפל במבעים בכל אורך סופי שהוא. כעת, השווה את היכולת המתמטית של מחשב (A) ליכולת המתמטית של אדם+מחשב (B). מערכת B יכולה לטפל גם בטענת-גדל עבור הפרינקיפיה מתמטיקה, וגם בטענת-גדל עבור השפה הפורמלית שמתארת את היכולת המתמטית של מערכת B עצמה (אם, לכאורה, קיימת כזו). אז מה תאמר עכשיו? האם מערכת B יכולה להיות אלגוריתמית? |
|
||||
|
||||
אין שום בעיה להביע את טענת גדל לתורה נתונה כמו ZFC או הפרינקיפה, והיא אינה ארוכה מתפיסת אנוש. הבעיה היא שגם התאור שלך "לכל שפה פורמלית יש *טענה* (נקרא לה "טענת-גדל") שהיא נכונה אך לא ניתן להוכיחה באותה שפה" אינו נכון. ראשית כל, הערה טכנית - מדובר על תורה ולא על שפה. שנית, משפט גדל מתאר איך בונים טענת-גדל עבור תורה נתונה (העומדת בתנאי המשפט). טענת גדל הנ"ל נכונה אך אינה ניתנת להוכחה *אם ורק אם התורה עקבית*. מכיון שאיננו יודעים אם התורה עקבית או לא, הרי שגם אנחנו לא יודעים אם טענת-גדל הנ"ל נכונה או לא. |
|
||||
|
||||
שאלה שכל הזמן עונים לי עליה וכל הזמן אני שואל מחדש: "נכונה" - באיזה מודל? אם היא הייתה נכונה בכל המודלים, אז לא נובע ממשפט השלמות של גדל שהיא יכיחה? ואם קיים מודל שבה היא לא נכונה, מדוע ה"אם ורק אם" לא מראה שהתורה לא עקבית? |
|
||||
|
||||
שאלה טובה. התשובה הלא מספקת היא שהוא נכון ב''עולם האמיתי''. לפרטים, פנה לאורי של מחר. |
|
||||
|
||||
(היום זה אורי של מחר?) |
|
||||
|
||||
(זה היה אורי של שלשום) לענינינו: הניסוח "לכל תורה עקבית ו.... יש פסוק נכון שאינו יכיח בה" מניח מראש שיש "עולם אמיתי", שהפסוק הנ"ל נכון בו. כתבתי קצת יותר, אבל במקום זה בוא נשאל שאלה: כשאנחנו אומרים שהתורה עקבית, איפה הפסוק הזה נכון? |
|
||||
|
||||
המממ. תפסת אותי. לא חשבתי על תורות אף פעם בתור מודלים של איזו תורה אחרת. על תורות מסדר ראשון אפשר לחשוב בתור קבוצות, לא? כלומר, אפשר לדבר על ה-Von Neumann universe, למשל. |
|
||||
|
||||
על כל דבר במתמטיקה אפשר לחשוב בתור קבוצה (פחות או יותר). בכל אופן, יש מין שאלת ביצה-תרנגולת כאן. אם יש לך לוגיקה, אתה יכול בעזרתה לדבר על קבוצות ועל כל היקום המתמטי, אם יש לך קבוצות, אתה יכול בעזרתן לתאר את הלוגיקה, אבל משהו צריך לבוא קודם, לא? חזרה לגדל: הניסוח המועדף עלי אומר: כל תורה, או שאין לה תאור סופי, או שהיא פשוטה (במובן שאי אפשר לנסח טענות מסוימות) או שאינה עקבית (אפשר להוכיח ולהפריך כל דבר) או שאינה שלמה (יש פסוקים אי אפשר להוכיח או להפריך). אם אתה מניח שיש מספרים טבעיים "אמיתיים" שם בחוץ, אז אין תאור סופי נכון ומלא שלהם. בפרט אם התאור שלי סופי ונכון, אז הוא אינו מלא, כלומר, יש טענות נכונות שהוא אינו מראה. |
חזרה לעמוד הראשי |
מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
RSS מאמרים | כתבו למערכת | אודות האתר | טרם התעדכנת | ארכיון | חיפוש | עזרה | תנאי שימוש | © כל הזכויות שמורות |