לא כך. "כל מה שאנחנו מוכיחים בתחשיב היחסים הוא נכון" זו תוצאה פשוטה יותר; משפט השלמות (עבור תחשיב היחסים) אומר את ה...הממ... לא ההיפך בדיוק, אבל את זה: "כל מה שנכון אפשר להוכיח בתחשיב היחסים". זו נשמעת כמו טענה יומרנית קצת, אז כדאי להסביר.
תחשיב היחסים הוא, ביסודו של דבר, מערכת הוכחה. מי שרוצה להשתמש בה יכולה לבחור לעצמה שפה (מונחים יסודיים כמו "נקודה" או "+") ואוסף של אקסיומות, ואז ביכולתה להתחיל לגזור מסקנות פורמליות מהאקסיומות: תחשיב הפסוקים מתאר מה היא גזירה תקפה.
למערכת אקסיומות נתונה יש בד"כ הרבה *מודלים* - "עולמות" של עצמים המקיימים את האקסיומות, אחרי שמסכימים איזה עצם בעולם להתאים לכל מונח בשפה. אם משהו נכון ב*כל* מודל, אומרים שהוא "נכון". משפט השלמות מבטיח לנו שאם משפט בשפה הוא נכון במובן הזה, כלומר שהוא מתחייב מהאקסיומות, אז הוא גם ניתן להוכחה במובן הפורמלי, המכני (כלומר, סדרה של פסוקים שכל אחד מהם הוא אקסיומה או שהוא נובע מקודמיו דרך אחת המניפולציות המותרות בתחשיב היחסים).
המשפט הזה הוא טענה על מערכת ההוכחה, לא על אוסף ספציפי של אקסיומות. השלמות במובן של משפט *אי-השלמות* של גדל היא אחרת: מערכת אקסיומות היא שלמה אם"ם לכל פסוק 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.
|
RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש