בתשובה לאלון עמית, 30/12/09 8:25
 |
|
 |
||
|
||||
 |
אתה כתבת שאי אפשר אפילו לנסח את משפט אי השלמות לתורות מסדר שני . לעומת זאת בתגובה 166640 כתבת לד"ר טי "אני בטוח שאתה מכיר את משפט אי-השלמות ללוגיקה מסדר שני" בקיצור יא שקרן רימית את כולם וחשבת שלא יעלו עליך. אז עד שלא תסביר אני אחשוב שאתה שקרן ואם ההסבר שלך יהיה מספיק טוב אני אחשוב שאתה סתם חמור קופץ בראש. |  |
 |
 |
|
|
|
||
|
||||
|
במקום להתעמק בתגובות עתיקות (ושגויות) שלי, תוכל ללמוד הרבה יותר מקריאת ספרות בנושא (כמו הספר עליו המלצתי). התגובה ההיא נכתבה בשנת 2003, ואת רוב מה שאני יודע על הנושא למדתי אחר-כך - בין השאר בעקבות העניין שהתעורר בי במהלך הדיון ההוא (ד"ר טי היה בבת אחת מתדיין בלתי-נסבל וגם הרבה יותר נעים לדיון ממך). מה ש*התכוונתי* להזכיר אז היה המשפט שאומר שאין ללוגיקה מסדר שני משפט שלמות, ובבורותי קראתי לזאת "משפט אי-השלמות ללוגיקה מסדר שני". אבל אפילו אז הבנתי שאין מדובר ב"משפט אי-השלמות של גדל". כפי שהוסבר כבר, ה"שלמות" של משפט השלמות וה"אי-שלמות" של משפט אי-השלמות הן מושגים שונים לחלוטין. משפט אי-השלמות של גדל אומר שבתנאים מסויימים קיים פסוק שאין לו הוכחה וגם לשלילתו אין כזו. זהו משפט מתמטי, לא פילוסופי ולא מטא-מתמטי, ומכאן שיש משמעות פורמלית למושג "הוכחה" המופיע בניסוח שהרגע ציטטתי. משמעות זו היא שרשרת של פסוקים העונה על התנאים הטכניים של "הוכחה" עבור תחשיב הפסוקים מסדר ראשון. דא עקא, שלתחשיב הפסוקים מסדר שני אין מושג כזה של שרשרת המהווה הוכחה. ועוד היבט: בכל פעם שאתה מפעיל (בהצלחה) את המשפט הזה על מערכת אקסיומות מסויימת, אתה יכול להסיק (בעזרת משפט השלמות) שלאותה מערכת יש שני מודלים שונים. לאריתמטיקה מסדר שני יש מודל יחיד (זוהי תורה קטגורית), וממילא אתה יכול לראות שאי-אפשר להפעיל עליה את המנגנון הזה. דבר אחד נכון בהחלט: גם באריתמטיקה מסדר שני יש משפטים שלא ניתן להוכיח-פורמלית, אבל זאת מסיבה פשוטה מאוד: אין דרך פורמלית להצרין "נביעה לוגית" בלוגיקה מסדר שני, וממילא אין לנו יכולית להוכיח-פורמלית משפטים בלוגיקה כזו. המונח "אקסיומות פאנו" יכול להתייחס גם לניסוח מסדר ראשון (עם סכמת-אקסיומות עבור אינדוקציה) וגם לניסוח מסדר שני. דומני שכיום מקובל הרבה יותר להתייחס לסדר ראשון. זה לא מאוד משנה - העיקר הוא להבין, בכל הקשר נתון, על איזו תורה מדובר (שכן ההבדלים ביניהן, כפי שהסברתי, מהותיים מאוד). ועכשיו, מסיבות שאני בטוח שאתה מבין, אפרוש סופית מהדיון איתך. אם משהו עדיין לא ברור, קרא את הספר עליו המלצתי או את ספרו המצויין של Torkel Franzen. |
|
|
|
|
|
|
||
|
||||
|
לא בהכרח מלמד לגבי תרבות הדיון, אבל ד"ר טי כנראה יודע חשבון טוב מאינקוגניטו. |
|
|
|
|
|
|
||
|
||||
|
והוא אף מחזיק ביכולת להודות בטעות (תגובה 171334). אילו ידעתי אז את כל מה שאני יודע היום הייתי יכול לעזור לו להגיע למסקנה הזו הרבה יותר מהר. | |
|
|
|
|
|
||
|
||||
|
חידוד קטן: אין בעיה להגדיר "מערכת הוכחה" עבור לוגיקה מסדר שני - למשל, רמאות קטנה שנקראת "הוכחה סמנטית", שבה אומרים שקבוצת פסוקים א' מוכיחה את הפסוק ב' אם כל מודל ל-א' הוא מודל לב' (כלומר, א' גורר סמנטית את ב'). כמובן שזו מערכת הוכחה חסרת כל ערך, אבל מבחינה הגדרתית היא לגיטימית. הבעייתיות הרלוונטית במערכת הזו היא שזו לא מערכת *אפקטיבית*, כלומר דרישת האפקטיביות (שהיא הרי קריטית אצל גדל) היא מה שנכשל הפעם, ולא השלמות (אני רואה את גדל כמעין משפט Trade-off - אי אפשר להיות בו זמנית גם שלמים, גם עקביים וגם אפקטיביים). (אני מודה ש"הוכחה סמנטית" הוא מושג שבו נתקלתי רק בהקשר של תחשיב הפסוקים, ושם אפילו הייתה לו תועלת כלשהי; אבל אני לא רואה בעיה עם ההכללה האידיוטית שלי, מבחינה עקרונית). |
|
|
|
|
|
|
||
|
||||
|
ודאי - לכן הדגשתי "להצרין". זו לא "רמאות", זו פשוט הדגשת ההבדל בין נביעה לוגית ליכיחות פורמלית. משפט השלמות של גדל מראה שההבדל הזה לא קיים בלוגיקה מסדר ראשון, וחסרונו בלוגיקה מסדר שני מראה את הבעייתיות של מערכות אקסיומטיות מסדר שני. | |
|
|
|
|
|
||
|
||||
|
1) גם לי נמאס מהדיון הזה. 2) יש משפט אי שלמות לסדר שני. 3) רק בריאות. 4)ביי. |
|
|
|
|
|
|
||
|
||||
|
(נסיון אחרון) 2) רפרנס לספר (Textbook, כזה שמוכיח דברים באופן רציני) שמנסח ומוכיח את המשפט? (אם יש רק מאמר, אז מאמר) |
|
|
|
|
|
|
||
|
||||
|
(מאוד ייתכן שיש משפט המכונה בשם הזה - אז מה? כל מה שאמרתי הוא שמשפט אי-השלמות הראשון של גדל מנוסח באופן כזה שאינו חל על תורות מסדר שני, כי הוא מניח כנתון קיומה של מערכת הוכחה פורמלית). | |
|
|
|
|
|
||
|
||||
|
(וואו, נכנסת לשדה מוקשים. עכשיו אפשר לשלוף לך ספר שמשחק באופן שונה עם הטרמינולוגיה וכן מדבר על משפט אי השלמות הראשון, במובן של ה-Tradeoff שהזכרתי קודם) | |
|
|
|
|
|
||
|
||||
|
יכול להיות. אני לא חושב שזה מאוד משנה - בסה''כ יש כאן סדרה לא ארוכה של טענות ברורות מאוד לגבי היכולת להוכיח באופן פורמלי דברים לגבי מספרים טבעיים. אלו שאלות מעניינות שאני בד''כ נהנה לדון בהן (יותר מדי נהנה לפעמים), אבל לא באופן שהדיון הזה התדרדר אליו. | |
|
|
|
|
|
||
|
||||
|
תאמין לי אם הייתי יודע שעל זה הדיון הייתי מוותר לך מלכתחילה, אז משפט גדל לא מדבר על סדר שני זה המשפט השני שמדבר על סדר שני. ביג דיל. |
|
|
|
|
|
|
||
|
||||
|
בדיוק: ביג דיל. (על מה בדיוק היית צריך "לוותר" לי? ביקשת ממך משהו?) | |
|
|
|
|
|
||
|
||||
|
(צ''ל ''ביג דיל''. גם לדעתי שמות המשפטים אינם חשובים.) | |
|
|
|
|
|
||
|
||||
|
דיברתי עם גדי, לא שאכפת לי שאתה מדבר עם הטרחן שקרא לך שקרן, פשוט משמעות המילה ''לך'' משתנה. | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |