בתשובה ללודביג, 24/02/04 6:26
 |
|
 |
||
|
||||
 |
1. כן. ההגדרה של מערכת לא עקבית היא שהיא יכולה להוכיח דבר והיפוכו. לכן, אי-עקביות (אם היא קיימת) ניתנת להוכחה בתוך המערכת. במצב זה, ניתן לראות שאפשר להוכיח באמצעות המערכת *כל* דבר (וגם את היפוכו), מה שכמובן הופך אותה ללא מעניינת. נכון שאפשר אז גם להוכיח שהיא לא עקבית וגם להוכיח שהיא כן עקבית (בהנחה שעקביות-עצמית בכלל ניתנת לניסוח בתוך המערכת, מה שלא תמיד המצב), כמו שאפשר להוכיח גם ש-X=X וגם ש=X שונה מ-X; זה לא נורא מעניין כי זה כבר לא נכון שמה שאפשר להוכיח הוא אמיתי. מובן מאליו שלוגיקאים מקווים מאוד שהמערכות בהן הם עובדים אינן כאלה, ולעיתים ניתן להוכיח זאת (באמצעות מערכות רחבות יותר). 2. לא, אין קשר ל"לא הצלחנו", הטענה היא שאי-אפשר. אבל אתה צודק, צריך לסייג ב"אם היא עקבית". 3. כן. הנה דוגמה: יש מערכת הנקראת "אקסיומות פֵּאָנו (מסדר ראשון) של תורת המספרים". זו תורה לוגית המאפשרת לדון במספרים הטבעיים, בחיבור ובכפל, ולהוכיח משפטים כמו "כל מספר ראשוני המשאיר שארית 1 בחלוקה ל-4 הוא סכום של שני ריבועים", וכו'. צריך להבין שלא כל טענה מתמטית בכלל ניתנת לניסוח בתוך המערכת הזו: למשל, הטענה "לכל פונקציה רציפה על הכדור יש נקודת שבת" היא כזו. לעומת זאת, הטענה "מערכת פאנו היא עקבית" דווקא כן ניתנת לניסוח כטענה בתוך המערכת - ברם, לפי גדל, אי אפשר להוכיח אותה במערכת זו. למרבה השמחה אפשר כן להוכיח אותה במערכת חזקה יותר, למשל אחת הנקראת ZF ומכילה אקסיומות של תורת הקבוצות. מה הערך של הוכחה כזו? פשוט, היא עוזרת לך להקטין את מספר הדברים בהם צריך להאמין. אם אתה מאמין ש-ZF עקבית, קיבלת במתנה שגם פאנו כזו. |
 |
 |
 |
|
|
|
||
|
||||
|
2. אין צורך לסייג: אי-אפשר להוכיח עקביות, בין אם מפני שהמערכת לא עקבית, ובין אם מפני שהיא עקבית ואי-אפשר להוכיח את זה. | |
|
|
|
|
|
||
|
||||
|
זה סתם ניטפוק לא מעניין, אבל אם המערכת לא עקבית, למה היא לא יכולה להוכיח שהיא עקבית? פורמלית, היא כן, והיא יכולה גם להוכיח את ההיפך וזה כאמור לא ממש מעניין. -- (גזור וזרוק) -- אם המערכת היא T, ו-X מסמן איזושהי סתירה כמו "a וגם לא a", אז: T |= (X -> con(T)) כי אגף ימין הוא טאוטולוגיה, וגםT |= X כי T לא עקבית, ומכאן בגרסת מודוס-פוננס ליכיחות,T |= con(T) לא?
|
|
|
|
|
|
|
||
|
||||
|
יכול להיות שזו סתם קטנוניות טכנית, אבל הוכחות פורמליות לא עובדות עם טאוטולוגיות של תחשיב פסוקים? הטענה (a!=a --> B) איננה מהווה טאוטולוגיה בתחשיב הפסוקים, וממילא לא ניתן להשתמש בה כאקסיומה בהוכחה. אני חושב שעל מנת להראות שסתירה בתחשיב יחסים מוכיחה כל טענה אפשר לשחזר את הוכחת משפט השלמות של גדל, כאשר לכל טענה A ניתן לטעון ש "כל מודל של T מקיים A" (באופן ריק). | |
|
|
|
|
|
||
|
||||
|
אני לא בטוח שצריך דווקא את תחשיב הפסוקים, עקרונית כל מה שדרוש הוא שפה ומערכת הוכחה. לרוב דורשים שמערכת ההוכחה תהיה sound ושלמה, אבל לצורך הזה אני לא חושב שאפילו צריך שלמות. במערכת הוכחה סבירה, כלל הגזירה הבאה (הוכחה על דרך השלילה) יהיה אקסיומה, או מסקנה מכללים אחרים: אם T, ~f |- g ו-T, ~f |- ~g אזT |- f ונראה לי שזה כל מה שדרוש. (למעלה השתמשתי בטעות ב-=| במקום ב -|, זה לא משנה הרבה אך התכוונתי להסקה פורמלית, לא לנכונות בכל מודל. אולי זה מה שבלבל).
|
|
|
|
|
|
|
||
|
||||
|
חשבתי על זה עוד קצת, אבל עדיין נראה לי שיש איזו בעיה עקרונית. הרי מערכת ההוכחה היא "טיפשה". היא מסוגלת לזהות רק סתירות של תחשיב פסוקים (כי היא כוללת את הטאוטולוגיות של פסוקים כאקסיומות). ברור שאם כבר ידוע ש T -מוכיחה- טענה ושלילתה אז ניתן להוכיח הכל, אבל סתם מכך שיצרנו תורה לא עקבית (למשל, תורה של מרחב וקטורי ממימד n יחד עם אופרטור שהינו חח"ע אבל לא על) עוד אין לנו סדרת הוכחה. בשביל להראות שמספיק שב T יש סתירה על מנת לייצר הוכחה של כל טענה יש לטעון שלפי קומפקטיות יש לנו אוסף סופי של טענות שבהן כבר יש סתירה, ומשם בעצם לשחזר את הוכחת משפט השלמות. רק במקרה שהסתירה ב T נובעת מסתירה של תחשיב פסוקים אז "יש לנו מזל" וההוכחה נעשית מובנת מאליה. אבל באוסף הטענות שכולל את האקסיומות של מרחב וקטורי ממימד n בצרוף הטענה על אופרטור חח"ע ולא על אין שום סתירה של תחשיב פסוקים. בקיצור, אם אני לא טועה יש הבדל בין העובדה (הטריוויאלית לגמרי) שאם מערכת מוכיחה טענה ושלילתה אז היא מוכיחה כל טענה, לבין העובדה שאם במערכת -קיימת- סתירה (קרי, היא איננה עקבית, אין לה שום מודל) אז ניתן לייצר ממנה הוכחה לכל טענה. הוכחת העובדה השניה היא כבר פחות או יותר משפט השלמות. | |
|
|
|
|
|
||
|
||||
|
רגע, נדמה לי שהקושי הוא שאתה מגדיר מערכת לא-עקבית ככזו שאין לה מודל, ואני הגדרתי מערכת לא-עקבית ככזו שמוכיחה דבר והיפוכו. במערכות שלמות, כפי שציינת, זה אותו דבר. אני חושב שנתקלתי בשתי ההגדרות. | |
|
|
|
|
|
||
|
||||
|
sound = נאותה. (סליחה על ההפרעה, תמשיכו). | |
|
|
|
|
|
||
|
||||
|
חשבתי שמדובר על הוכחה מבחוץ (במערכת עקבית) שהמערכת (הלא-עקבית) ''שלנו'' היא עקבית, וזה כמובן בלתי אפשרי. אבל זה לא מאד מעניין. | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |