משפט השלמות של גדל, ההוכחה (חלק ב')

אנו ממשיכים בהוכחת משפט השלמות של גדל. כזכור, בפוסט הקודם הוכחנו שאם $latex \Phi$ היא תורה עקבית מקסימלית מעל מילון $latex \tau$ שבנוסף לכך קיימת עבורה קבוצת עדים $latex C$, אז קיים ל-$latex \Phi$ מודל. זה מספיק כדי לסיים את ההוכחה, בתנאי שנוכיח שכל תורה עקבית $latex \Phi$מעל מילון $latex \tau$ ניתן להרחיב לתורה עקבית מקסימלית שקיימת עבורה קבוצת עדים.

לפני שנזכיר מה זה בכלל עדים וניגש לחלק הזה בהוכחה, בואו נסיים עם ה"עקבית מקסימלית" שהוא פשוט יותר מכיוון שכבר עשינו את זה בדיוק בהוכחת משפט השלמות לתחשיב הפסוקים. נניח שיש לנו תורה עקבית $latex \Phi$ ואנחנו רוצים להרחיב אותה לתורה עקבית מקסימלית $latex \Phi^{\prime}$; פשוט נמספר את כל הפסוקים הקיימים, $latex \varphi_{1},\varphi_{2},\varphi_{3},\dots$ ואז נגדיר אינדוקטיבית סדרה של תורות $latex \Phi_{0},\Phi_{1},\Phi_{2},\dots$ באופן הבא: $latex \Phi_{0}=\Phi$ ולכל $latex n$, אם $latex \Phi_{n}\cup\left\{ \varphi_{n}\right\} $ עקבית אז $latex \Phi_{n+1}=\Phi_{n}\cup\left\{ \varphi_{n}\right\} $ ואחרת $latex \Phi_{n+1}=\Phi_{n}$. לבסוף נגדיר $latex \Phi^{\prime}=\bigcup_{n=0}^{\infty}\Phi_{n}$. ברור ש-$latex \Phi^{\prime}$ עקבית בזכות תעלול סטנדרטי שמסתמך על סופיות של הוכחות: אם $latex \Phi^{\prime}$ אינה עקבית אז היא מוכיחה דבר והיפוכו, ושתי ההוכחות הללו סופיות ולכן משתמשות במספר סופי של הנחות מתוך $latex \Phi^{\prime}$ ולכן, אם $latex n$ הוא האינדקס המקסימלי של הנחה שבה משתמשים בהוכחות הללו, כבר $latex \Phi_{n}$ אינה עקבית, בסתירה לתהליך הבניה שלנו.

כדי לראות ש-$latex \Phi^{\prime}$ עקבית מקסימלית בואו ניקח תורה עקבית כלשהי שמכילה אותה, $latex \Phi^{\prime}\subseteq\Psi$ ונראה שהן שוות. אם $latex \varphi\in\Psi$ אז בפרט $latex \Phi^{\prime}\cup\left\{ \varphi\right\} $ עקבית; נסתכל על המספור של $latex \varphi$ בסידור של הפסוקים שלנו, אז $latex \varphi=\varphi_{n}$ עבור $latex n$ כלשהו. מכיוון ש-$latex \Phi^{\prime}\cup\left\{ \varphi_{n}\right\} $ עקבית כך גם $latex \Phi_{n}\cup\left\{ \varphi_{n}\right\} $ ולכן הוספנו את $latex \varphi_{n}$ ל-$latex \Phi_{n+1}$ ומכאן ש-$latex \varphi\in\Phi^{\prime}$ כנדרש. בקיצור, ההוכחה הזו פשוטה מאוד.

פרט, כמובן, לכך שאני עובד עליכם. האם אתם רואים היכן?

נקודה שלא היה צריך להתייחס אליה בתחשיב הפסוקים ולכן קל מאוד לא לשים לב אליה עכשיו היא ההנחה המובלעת שלי שיש רק מספר בן מניה של פסוקים ולכן אפשר למספר אותם ואפשר לבנות סדרה של תורות ואז לאחד את כולן. אלא שמספר הפסוקים תלוי במספר הסימנים שיכולים להופיע בפסוק. כל עוד היה לנו רק מספר בן מניה של סימנים הכל היה טוב ויפה, אבל בלוגיקה מסדר ראשון המילון $latex \tau$ לא חייב להיות בן מניה.

אז מה הפתרון? אם להשתמש בקללה, אינדוקציה טרנספיניטית; ואם לא להשתמש בקללה – חכו לסוף הפוסט ואתייחס לזה. לעת עתה ועד לסוף הפוסט נניח שהמילון שלנו כן בן מניה. ההוכחה שנציג תהיה זהה באופיה להוכחה במקרה הכללי, אבל היא תהיה טיפה ממוקדת יותר בעניינים החשובים ולא בדרך שבה מתמודדים עם כך שקבוצת הפסוקים לא בת מניה.

בואו נעבור כעת לאתגר האמיתי: נתונה לנו תורה עקבית $latex \Phi$ ואנחנו רוצים להרחיב אותה לתורה עקבית $latex \Phi^{\prime}$ ואת המילון למילון מורחב $latex \tau^{\prime}$ כך שקיימת קבוצת עדים $latex C$. נזכיר מה זה אומר: זה אומר שלכל נוסחה $latex \varphi\left(x\right)$ עם משתנה חופשי יחיד $latex x$ קיים קבוע $latex c\in C$ כך ש-$latex \Phi^{\prime}\vdash\exists x\varphi\left(x\right)\to\varphi\left(c\right)$.

הרעיון הוא כזה: את $latex \tau$ נרחיב על ידי כך שניקח קבוצה בת מניה $latex C$ של סימנים שלא מופיעים ב-$latex \tau$ ונוסיף אותה לאוסף הקבועים של $latex \tau$. כעת נמספר את כל הנוסחאות עם משתנה חופשי יחיד, $latex \varphi_{1}\left(z_{1}\right),\varphi_{2}\left(z_{2}\right),\varphi_{3}\left(z_{3}\right),\dots$. אני בכוונה משתמש כאן במשתנה $latex z$ כדי להבהיר שהאינדקס שלו הוא אינדקס שמתאים ל-$latex \varphi$ שלו, לא לערך ה"אמיתי" שלו. מבלבל? הכוונה שלי היא לכך שייתכן ש-$latex \varphi_{1}$ היא הנוסחה $latex \forall x_{17}\left(x_{17}=f\left(x_{17}\right)\right)$, כלומר כאן $latex z_{1}=x_{17}$. למי שעדיין לא עוקב – לא לדאוג, זה חסר כל חשיבות להמשך.

עכשיו נעשה את הדבר הצפוי ביותר בעולם. נגדיר סדרה $latex \Phi_{0},\Phi_{1},\Phi_{2},$ של תורות באופן הבא: $latex \Phi_{0}=\Phi$ ולכל $latex n\ge1$ , $latex \Phi_{n+1}=\Phi_{n}\cup\left\{ \exists z_{n}\varphi_{n}\left(z_{n}\right)\to\varphi_{n}\left(c_{n}\right)\right\} $, כאשר $latex c_{n}$ הוא איבר כלשהו מתוך $latex C$ שטרם נבחר (כלומר, אינו שייך לקבוצה $latex \left\{ c_{1},c_{2},\dots,c_{n-1}\right\} $ – קיים כזה כי זו קבוצה סופית ואילו $latex C$ אינסופית). לבסוף נגדיר $latex \Phi^{\prime}=\bigcup_{n=0}^{\infty}\Phi_{n}$. ברור לגמרי שקיבלנו תורה ש-$latex C$ היא קבוצת עדים עבורה. השאלה היחידה היא האם $latex \Phi^{\prime}$ עקבית. כמו קודם, מספיק להוכיח שאם $latex \Phi_{n}$ עקבית אז $latex \Phi_{n+1}$ עקבית, כלומר ש-$latex \Phi_{n}\cup\left\{ \exists z_{n}\varphi_{n}\left(z_{n}\right)\to\varphi_{n}\left(c_{n}\right)\right\} $ עקבית. כאן סוף סוף נצטרך טיפונת להפשיל שרוולים.

אם כן, הבה ונניח ש-$latex \Phi_{n}\cup\left\{ \exists z_{n}\varphi_{n}\left(z_{n}\right)\to\varphi_{n}\left(c_{n}\right)\right\} $ אינה עקבית. באופן כללי, אם $latex \Phi\cup\left\{ \psi\right\} $ אינה עקבית אז $latex \Phi\vdash\neg\psi$ – זה נובע מהאקסיומות של תחשיב הפסוקים. וכבר ראינו את זה אז (ליתר דיוק אז זה היה שאם $latex \Phi\cup\left\{ \neg\psi\right\} $ אינה עקבית את $latex \Phi\vdash\psi$ אבל זה אותו הדבר). מכאן ש-$latex \Phi_{n}\vdash\neg\left[\exists z_{n}\varphi_{n}\left(z_{n}\right)\to\varphi_{n}\left(c_{n}\right)\right]$. אני טוען שנובעים מכך שני דברים: $latex \Phi_{n}\vdash\exists z_{n}\varphi_{n}\left(z_{n}\right)$ וגם $latex \Phi_{n}\vdash\neg\varphi_{n}\left(c_{n}\right)$. ראינו את זה בפוסט הקודם אבל זה כל כך קריטי שאסביר שוב למה זה קורה. הטענה, באופן כללי, היא שאם $latex \Phi\vdash\neg\left(\alpha\to\beta\right)$ אז $latex \Phi\vdash\alpha$ וגם $latex \Phi\vdash\neg\beta$. על מנת להוכיח זאת אנו נעזרים בכך שתבנית הפסוק הבא היא טאוטולוגיה של תחשיב הפסוקים ולכן יכיחה מ-$latex \Phi$: $latex \neg\left(\alpha\to\beta\right)\to\alpha$, וכך גם עבור $latex \neg\left(\alpha\to\beta\right)\to\neg\beta$.

כעת מגיע החלק הכי עדין בכל הוכחת משפט השלמות של גדל, לטעמי: אנו יודעים ש-$latex \Phi_{n}\vdash\neg\varphi_{n}\left(c_{n}\right)$. עוד אנחנו יודעים ש-$latex c_{n}$ הוא סימן קבוע חדש, כזה שלא הופיע כלל ב-$latex \Phi_{n}$. פירוש הדבר הוא שאפשר לקחת את סדרת ההוכחה של $latex \neg\varphi_{n}\left(c_{n}\right)$ ובכל מקום שבו מופיע בה $latex c_{n}$ לכתוב במקומו $latex y$ כאשר $latex y$ הוא שלא מופיע בהוכחה של $latex \neg\varphi_{n}\left(c_{n}\right)$ מ-$latex \Phi_{n}$. ההוכחה תמשיך להיות תקפה גם עבורו – צריך להוכיח זאת באינדוקציה, אבל אחמוק מלעשות זאת. המסקנה היא ש-$latex \Phi_{n}\vdash\neg\varphi_{n}\left(y\right)$ ומכיוון שניתן להפעיל את Gen (כי $latex y$ לא מופיע בהנחות שנדרשו לצורך ההוכחה), נקבל $latex \Phi_{n}\vdash\forall y\neg\varphi_{n}\left(y\right)$, או בסימון שונה, $latex \Phi_{n}\vdash\neg\exists y\varphi_{n}\left(y\right)$, והרי ראינו ש-$latex \Phi_{n}\vdash\exists z_{n}\varphi_{n}\left(z_{n}\right)$, כלומר קיבלנו ש-$latex \Phi_{n}$ מוכיחה פסוק ושלילתו (עד כדי הביצוע הפורמלי של החלפת $latex z_{n}$ ב-$latex y$), כלומר $latex \Phi_{n}$ אינה עקבית. זה מסיים את ההוכחה ש-$latex \Phi^{\prime}$ היא עקבית, ולכן מסיים את ההוכחה של משפט השלמות כולו. אבל רק כאשר $latex \tau$ היה מילון בן מניה.

מה קורה כאשר $latex \tau$ לא בן מניה? כאן אין מנוס – אנחנו זקוקים לכלי מתמטי חזק יחסית – אקסיומת הבחירה. אקסיומת הבחירה, כזכור, שקולה לעקרון הסדר הטוב; הוא מאפשר לנו לסדר בסדר טוב את קבוצת כל הנוסחאות, ולהפעיל עליה אינדוקציה שדומה מאוד לאינדוקציה רגילה – אינדוקציה טרנספיניטית. בפועל זה מתבצע כך: אם $latex \alpha$ הוא העוצמה של המילון, ולכן של קבוצת הנוסחאות מעליו, אז מוסיפים קבוצה $latex C=\left\{ c_{\beta}\ |\ \beta<\alpha\right\} $ של קבועים, מסדרים את כל הנוסחאות $latex \varphi$ בסידור טוב עם אותו סודר, כלומר $latex \varphi_{\beta}$ לכל $latex \beta<\alpha$, וכעת לכל סודר $latex \beta$ מגדירים את $latex \Phi_{\beta}$ באופן הבא: $latex \Phi_{0}=\Phi$, ו-$latex \Phi_{\beta+1}=\Phi_{\beta}\cup\left\{ \exists z_{\beta}\varphi_{\beta}\left(z_{\beta}\right)\to\varphi_{\beta}\left(c_{\beta}\right)\right\} $ – עד כאן בדיוק כמו אינדוקציה רגילה. צריך רק לטפל גם במקרה של סודר גבולי ולהגדיר את $latex \Phi_{\beta}$ עבורו באופן הטבעי: $latex \Phi_{\beta}=\bigcup_{\gamma<\beta}\Phi_{\gamma}$. יש להראות שגם $latex \Phi_{\beta}$ עקבית אם $latex \Phi_{\gamma}$ עקבית לכל $latex \gamma<\beta$, ופה הסופיות של הוכחה נחלצת לעזרתנו בדיוק כמו קודם – מניחים בשלילה ש-$latex \Phi_{\beta}$ לא עקבית, מסתכלים על קבוצת כל הסודרים שמתאימים לקבוצות $latex \Phi_{\gamma}$ שבהנחות מתוכן משתמשים בהוכחה של דבר והיפוכו מתוך $latex \Phi_{\beta}$, לוקחים את הסודר המקסימלי (יש כזה כי זו קבוצה סופית) ומקבלים $latex \Phi_{\gamma}$ שאינה עקבית, בסתירה להנחת האינדוקציה. אם כן, כפי שאנו רואים, עניין המילון הלא בן מניה לא מציב קושי טכני או רעיוני חריג; אבל הוא דורש קצת יותר רקע מתמטי שחבל לדרוש אותו מקוראים שרק רוצים להכיר את משפט השלמות.

השלמנו את הוכחת משפט השלמות, ובפני עצמו זה נראה לי כמו הישג לא רע בכלל – הנה מצאנו מערכת הוכחה שלמה ונאותה למשהו מורכב כמו לוגיקה מסדר ראשון! עם זאת, למשפט השלמות יש כמה השלכות לא טריוויאליות בכלל שאציג בפוסט הבא, ואני מקווה שלפחות עבור חלקכם (שלא מכיר את התוצאות הללו כבר) מה שאציג יתן לכם נקודת מבט חדשה על הלוגיקה המתמטית ואולי על המתמטיקה בכלל; אני יודע שזה מה שקרה לי.

12 תגובות בנושא “משפט השלמות של גדל, ההוכחה (חלק ב')”

  1. תודה על הפוסט המעניין!

    יש נקודה אחת שמבלבלת אותי: בפוסט אתה מראה שאפשר לבנות תורה עקבית מקסימלית, כלומר, כזו שלכל פסוק, מוכיחה או אותו או את שלילתו. אבל האם משפט האי-שלמות לא מראה שתורה כזו לא יכולה להתקיים?
    אני מנחש שהנקודה היא שהמשפט של גדל תקף רק לתורות שניתן להכריע עבורן האם פסוק הוא אקסיומה או לא, ושהתורה שבנית בפוסט הזה לא מקיימת את התכונה הזו. זו הנקודה? או שיש כאן משהו אחר?

  2. אכן, התורה שאני בונה פה היא לא כריעה(/רקורסיבית/אפקטיבית – בחר את השם שאתה מכיר לתכונה הזו).

  3. שלום גדי,
    ראשית, תודה על הבלוג הנהדר! אני עוקב אחריו כבר מספר שנים ומוצא שההסברים שלך בהרבה מקרים מאירים פנים חדשות במתמטיקה.
    נדמה לי שיש טעות (קצת טכנית, אני מודה) בהוכחה שלמעלה. הטענה העיקרית היא שכל תורה עקבית ניתנת להרחבה לתורה עקבית מקסימלית בעלת תכונת הנקין. ההוכחה התבצעה בכך שהראית שכל תורה עקבית ניתנת להרחבה לתורה עקבית מקסימאלית, ושכל תורה עקבית ניתנת להרחבה לתורה עקבית עם תכונת הנקין. יש לשים לב אבל שצעד ההרחבה לתורה עם תכונת הנקין מאבד את המקסימליות של התורה – שהרי הוספנו קבועים לשפה, ועתה נוצרו פסוקים חדשים שהם ושלילתם לא נמצאים בתורה.
    כמובן שאפשר לתקן את ההוכחה בזה שמבצעים בכל צעד אידוקציה, בנוסף להוספת סימן הקבוע והפסוק המתאים לו גם השלמה לתורה עקבית מקסימלית בהינתן השפה החדשה.

  4. האם באמת צריך להרחיב מחדש בכל צעד באינדוקציה? אני כבר לא זוכר את הפרטים הטכניים לעומק אבל דומני שהכוונה שלי (שלא כתובה במפורש בפוסט) הייתה שאת תהליך ההרחבה לתורה עקבית מקסימלית עושים אחרי שגורמים להוסיף את העדים.

  5. אתה צודק כמובן – אם מוסיפים את העדים לפני ההרחבה לתורה שלמה אז לא צריך את האינדוקציה הכפולה. טעות שלי.

  6. אני חושב שנכנעתי מהר מדי. עדיין יש כאן נקודה עדינה בשלב הוספת העדים: לאחר הוספת הקבועים החדשים, בנוסף לפסוקים חדשים נוצרים גם נוסחאות חדשות. העדים הם רק לנוסחאות בשפה המקורית, ולא לנוסחאות בשפה המורחבת, שעלולים לכלול בעצמם את הקבועים החדשים. את זה אפשר לפתור על ידי זה שתהליך הוספת הקבועים נעשה באינדוקציה כפולה (מגדירים סדרה עולה של תורות שלכל אחת יש עדים עבור התורות המוכלות בה, ולוקחים את האיחוד).

    תודה לידידי רע גולן על השיחה בנושא, ושהאיר את עיני שהבעיתיות הזאת מופיעה גם בכמה מספרי הלימוד הסטנדרטיים. ותודה לך שוב על הבלוג.

  7. מיכאל, אני לא בטוח שאתה צודק. הנה האופן שבו נראה לי שהדברים מתנהלים:
    1) מרחבים את התורה שלנו לתורה עקבית מקסימלית, סתם כי אפשר (אולי צריך את זה בהמשך?)
    2) מרחיבים את השפה שלנו על ידי הוספת קבוצת קבועים בגודל המתאים.
    3) ממספרים את כל הנוסחאות בשפה *המורחבת* ואז מרחיבים סדרתית את התורה שלנו כדי שתכיל עדים ועדיין תהיה עקבית.
    4) קיבלנו תורה שמכילה עדים והיא עקבית. מרחבים אותה (מבלי להרחיב את השפה) כדי שתהיה עקבית מקסימלית.

    אני מפספס משהו? נדמה לי שבספר שהלכתי לפיו (קיזלר וצ'נג) זה מה שהם עושים, בלי אינדוקציה כפולה, וזה נחשב לספר טוב.

  8. הבעיתיות היא בשלב 3. לפי איך שתיארת את בחירת הקבוע שיעיד על הנוסחא, ייתכן והוא כבר מופיע באחד הנוסחאות הקודמות, או אפילו בנוסחא עצמה שהוא אמור להעיד עליה. אמנם דרשת שהוא יהיה קבוע שונה מה*עדים* הקודמים, אך מכיוון שהנוסחאות הם עכשיו בשפה המורחבת ייתכן והוא יופיע מבלי להיות עד. מצב כזה יכול לגרום לתורה לא עקבית. קיזלר וצ'נג נמנעים מזה ע"י הדרישה שהקבוע יהיה חדש לגמרי, כלומר שהוא לא הופיע לא בתור עד ולא באף אחד מהנוסחאות הקודמות או הנוסחא שהוא אמור להעיד עליה (והם טורחים להסביר למה תמיד קיים קבוע כזה). בדרך זו באמת אפשר להמנע מרמת אינדוקציה נוספת.
    הפתרון שאני הצעתי (וכך לימדו בקורס בעברית, בזמנו) הוא להשאיר את בחירת הקבוע כמו שתיארת, אבל למספר רק את הנוסחאות בשפה המקורית. בדרך זו אנחנו מוכיחים שכל תורה עקבית מוכלת בתורה עקבית בשפה מורחבת, שבה לכל נוסחא בשפה המקורית יש עד. אם לוקחים סדרה עולה של תורות כאלה, הרי שהאיחוד יהיה הרחבה עקבית של השפה המקורית בה לכל נוסחא יש עד.
    נדמה לי שצריך לבחור באחת משתי הדרכים האלה – או להשאיר את צעד האינדוקציה כמו שהוא, אבל לעשות רמה נוספת של אינדוקציה, או להשתמש בצעד אינדוקציה קצת יותר מורכב (אם כי לא בהרבה). איכשהו נראה לי שבהוכחה שגם ככה יש בה מרכיב אינדוקטיבי מאד חזק, יותר טבעי לבחור בדרך הראשונה, אבל זה כבר עניין של טעם.

כתיבת תגובה

האימייל לא יוצג באתר. שדות החובה מסומנים *