 |
|
 |
||
|
||||
 |
משפט השלמות של גדל: כמה בעיות פילוסופיות. מרצה באנגלית פרופ' ד'ולייט פלויד מבוסטון מגיב: פרופ' שטיינר מהאוניברסיטה העברית בניין לוי בגבעת רם, יום ד' ה-8.3 בשעה 20.00. |
 |
 |
 |
|
|
|
||
|
||||
|
נראה שהכוונה לזה: קצת מוזר שמדובר על משפט ה*שלמות*, אבל אולי. (ולמה "ד'ולייט"?) |
|
|
|
|
|
|
||
|
||||
|
כך זה מופיע בפרסום של ון ליר, למעט ה-ד' ב"כ'ולייט".:) | |
|
|
|
|
|
||
|
||||
|
כן, לכן טרחתי למצוא את הקישור. ראיתי שזו לא טעות שלך. בהחלט ייתכן שפלויד תדבר על קשיים פילוסופיים במשפט השלמות, אבל זה נשמע לי פחות סביר מהחלופה. | |
|
|
|
|
|
||
|
||||
|
עכשיו ראיתי כמה יפה שאפילו בתיקון הטעות לא הצלחתי להגיע ל-ג'... | |
|
|
|
|
|
||
|
||||
|
ולהגיע לז'ולייט - אפילו בתיקון של התיקון! | |
|
|
|
|
|
||
|
||||
|
בפרסום של ון ליר כתוב ג'ולייט. | |
|
|
|
|
|
||
|
||||
|
כן, שכחתי - בעניין השלמות - נראה לי שבון ליר פשוט לא אוהבים חוסר שלמות, הם די פרפקציוניסטים שם... | |
|
|
|
|
|
||
|
||||
|
מה עם תזכורת קצרה מה בדיוק אומר משפט השלמות? | |
|
|
|
|
|
||
|
||||
|
שמערכת היא שלמה אם כל טאוטולוגיה יכיחה בה. | |
|
|
|
|
|
||
|
||||
|
זו הגדרה של שלמות, לא משפט. משפט השלמות, עד שאלון יבוא ויתקן אותי, אומר שתחשיב היחסים (הפרדיקטים) הוא מערכת שלמה. | |
|
|
|
|
|
||
|
||||
|
לא נראה לי שמשפט השלמות מתייחס דווקא לתחשיב הפרדיקטים, אבל אולי באמת נחכה למי שיודע יותר. | |
|
|
|
|
|
||
|
||||
|
תודה לאלון על ההסבר הנאה (אף פעם לא עמדתי על ההבדל הזה בין שלמות תחשיב היחסים לאי-שלמות מערכות האקסיומות). אבל נראה לי שכדאי להבהיר, למי שנשאר מבולבל, שאתה צודק1: משפטי שלמות ייתכנו לכל מיני מערכות גזירה (ובפרט, יש משפטי שלמות לתחשיב הפסוקים ולתחשיב היחסים). אם אומרים "משפט השלמות של גדל" זה כבר מזהה חד-משמעית את משפט השלמות של תחשיב היחסים, כי אותו גדל הוכיח. 1 או שאני טועה. |
|
|
|
|
|
|
||
|
||||
|
בהחלט נכון, אתה לא טועה. | |
|
|
|
|
|
||
|
||||
|
כשאני למדתי את זה, זה היה הניסוח (היה גם משפט מקביל, פשוט יותר, עבור תחשיב הפסוקים), אבל ה''שלמות'' היא לא אותה שלמות כמו של משפט אי השלמות, ואני לא זוכר מה היא בדיוק אומרת. אני זוכר שבצורה לא פורמלית המרצה הסביר שזה אומר שכל מה שאנחנו מוכיחים בתחשיב היחסים הוא נכון (לא שאפשר להוכיח כל דבר או שלילתו - שזו השלמות שמשפט אי השלמות של גדל מראה שלא בהכרח מתקיימת). | |
|
|
|
|
|
||
|
||||
|
לא כך. "כל מה שאנחנו מוכיחים בתחשיב היחסים הוא נכון" זו תוצאה פשוטה יותר; משפט השלמות (עבור תחשיב היחסים) אומר את ה...הממ... לא ההיפך בדיוק, אבל את זה: "כל מה שנכון אפשר להוכיח בתחשיב היחסים". זו נשמעת כמו טענה יומרנית קצת, אז כדאי להסביר. תחשיב היחסים הוא, ביסודו של דבר, מערכת הוכחה. מי שרוצה להשתמש בה יכולה לבחור לעצמה שפה (מונחים יסודיים כמו "נקודה" או "+") ואוסף של אקסיומות, ואז ביכולתה להתחיל לגזור מסקנות פורמליות מהאקסיומות: תחשיב הפסוקים מתאר מה היא גזירה תקפה. למערכת אקסיומות נתונה יש בד"כ הרבה *מודלים* - "עולמות" של עצמים המקיימים את האקסיומות, אחרי שמסכימים איזה עצם בעולם להתאים לכל מונח בשפה. אם משהו נכון ב*כל* מודל, אומרים שהוא "נכון". משפט השלמות מבטיח לנו שאם משפט בשפה הוא נכון במובן הזה, כלומר שהוא מתחייב מהאקסיומות, אז הוא גם ניתן להוכחה במובן הפורמלי, המכני (כלומר, סדרה של פסוקים שכל אחד מהם הוא אקסיומה או שהוא נובע מקודמיו דרך אחת המניפולציות המותרות בתחשיב היחסים). המשפט הזה הוא טענה על מערכת ההוכחה, לא על אוסף ספציפי של אקסיומות. השלמות במובן של משפט *אי-השלמות* של גדל היא אחרת: מערכת אקסיומות היא שלמה אם"ם לכל פסוק S בשפה, או ש-S נכון או ש-S~ נכון (S~ זה "לא S"). אם מערכת אקסיומות T היא לא-שלמה (במובן הזה), יש S שאינו יכיח וגם S~ לא יכיח; מה שמשפט ה*שלמות* אומר במקרה זה הוא שחוסר היכיחות הזו איננו "סתם" מגרעת של כללי הגזירה שלנו, אלא שאכן יש שני מודלים שונים למערכת - שני עולמות אשר באחד מהם S מתקיים ובשני S איננו מתקיים. בלי משפט השלמות, היינו יכולים לקוות שהטענה על אי-שלמות תורת המספרים (למשל) היא לא כה מפחידה: היינו מקווים שמערכת האקסיומות שלנו אכן קובעת באופן חד-משמעי עולם אחד שבו כל S הוא נכון-או-לא-נכון, ורק שעלינו להמשיך ולחפש *כללי גזירה* מתוחכמים יותר שיאפשרו לנו לגזור פורמלית כל מה שנכון. ציטוט של פרנזן: Gödel was the first to prove this theorem (in his doctoral thesis). It's sometimes referred to as "Gödel's completeness theorem", chiefly in order to confuse people.
|
|
|
|
|
|
|
||
|
||||
|
תודה. המרצה שלי אמר פחות או יותר את מה שאתה אמרת, וזה כמובן אני שלא זכרתי אותו נכון. | |
|
|
|
|
|
||
|
||||
|
א. אם כך, האם אין כאן שום עניין של טאוטולוגיות? (משום מה זכור לי שיש). ב. האם יש כאן איזה קישור בין סינטקס לסמנטיקה? |
|
|
|
|
|
|
||
|
||||
|
ב. כן. נובע סינטקטית משמעו ניתן להוכחה פורמלית. נובע סמנטית משמעו נכון בכל מודל המקיים את האקסיומות. משפט השלמות אומר שהשניים שקולים. | |
|
|
|
|
|
||
|
||||
|
ומה ההגדרה הפורמלית ל"מודל" (אם היא לא מסובכת מדי)? | |
|
|
|
|
|
||
|
||||
|
הגדרה לא לגמרי פורמלית יש בתגובה 318055, ומשהו קצת יותר מפורט יש כאן: אם זה לא מספיק פורמלי או ברור, שאל. |
|
|
|
|
|
|
||
|
||||
|
הפילוסופיות שנובעות ממשפט השלמות על תחשיב הפרדיקטים? | |
|
|
|
|
|
||
|
||||
|
לא נכחתי בהרצאה, לצערי. אני עדיין סבור שהכוונה היתה למשפט אי-השלמות, אבל מי יודע. | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |