משפט השלמות לתחשיב הפסוקים

בפוסט הקודם הצגתי מערכת הוכחה (חלקית, עוד לא גמרנו) לתחשיב הפסוקים והוכחתי שהיא מקיימת את משפט הדדוקציה: אם \( \Phi\cup\left\{ \alpha\right\} \vdash\beta \) אז \( \Phi\vdash\alpha\to\beta \). הפעם אני רוצה להמשיך לבנות את מערכת ההוכחה הזו ולהראות שהיא מקיימת את התכונה שלשמה היא קיימת: להוכיח כל מה ש”נכון”, דהיינו אם \( \Phi\models\varphi \) אז \( \Phi\vdash\varphi \) (זכרו: \( \Phi \) היא קבוצת פסוקים כלשהי של “הנחות”; מערכת ההוכחה שלנו מסתתרת כולה בתוך הסימן \( \vdash \)). ההוכחה עצמה היא מרהיבה וכוללת לפחות שני רעיונות שלטעמי הם מקסימים; אולי הדבר הכי נחמד בה הוא שעיקר העבודה היא בכלל הוכחה של טענה אחרת שנראית לא קשורה ממבט חטוף ראשון אבל היא בעצם לב העניין. כדי להציג אותה, אזדקק להגדרה אחת אחרונה - עקביות.

אנחנו אומרים שקבוצת פסוקים \( \Phi \) היא עקבית אם אי אפשר להוכיח ממנה דבר ושלילתו, כלומר לא קיים \( \varphi \) כך שגם \( \Phi\vdash\varphi \) וגם \( \Phi\vdash\neg\varphi \). אם \( \Phi \) עושה דבר כזה, אז ממשפט הנאותות של מערכת ההוכחה שלנו נובע ש-\( \Phi\models\varphi \) וגם \( \Phi\models\neg\varphi \), כלומר כל השמה שמספקת את \( \Phi \) בו זמנית מספקת גם את \( \varphi \) וגם את \( \neg\varphi \) וזה בלתי אפשרי עם ההגדרות שלנו ל”מספקת”; המסקנה היא שאם \( \Phi \) היא לא עקבית, אין השמה שמספקת אותה. אם אין השמה שמספקת אותה, אז לכל \( \psi \) שלא יהיה מתקיים \( \Phi\models\psi \) (“באופן ריק”) ולכן, אם מערכת ההוכחה שלנו מקיימת את משפט השלמות, אז \( \Phi\vdash\psi \) לכל \( \psi \). במילים אחרות: במערכת הוכחה “נורמלית” (שמקיימת שלמות ונאותות), קבוצה לא עקבית של פסוקים מוכיחה הכל. באנגלית קוראים לזה Principle of Explosion ובעברית אין לי מושג אם יש לזה שם.

(http://xkcd.com/704/)

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

כדי להבין איך הקסם הזה קורה, אני נזקק לעוד תכונה אחת של מערכת ההוכחה שלי: הוכחה בשלילה. אני רוצה לטעון שאם \( \Phi\cup\left\{ \neg\varphi\right\} \) אינה עקבית, אז \( \Phi\vdash\varphi \) (זוהי בדיוק הוכחה בשלילה כפי שאנחנו מכירים אותה ממתמטיקה יומיומית; יש לנו הנחות \( \Phi \); אנחנו מניחים ש-\( \varphi \) אינו נכון, מוכיחים מכך סתירה, ומסיקים ש-\( \varphi \) כן נכון, בהינתן ההנחות \( \Phi \)). לרוע המזל, מערכת ההוכחה שלי עד כה אינה מסוגלת לבצע את הקסם הזה, ולכן אני נזקק לתבנית אקסיומה אחת אחרונה.

ראשית, בואו ננסה להבין מה יש לנו. אם \( \Phi\cup\left\{ \neg\varphi\right\} \) אינה עקבית, אז בואו נניח שמערכת ההוכחה שלנו כבר חזקה מספיק כדי שלכל \( \psi \) יתקיים \( \Phi\cup\left\{ \neg\varphi\right\} \vdash\psi \), ואז נוכל להסיק ממשפט הדדוקציה \( \Phi\vdash\neg\varphi\to\psi \). עכשיו, כלל ידוע במתמטיקה הוא שלהגיד “אם אלף אז בית” שקול ללהגיד “אם לא בית אז לא אלף”. זה בדיוק מה שעשיתי לכם לפני שניה - אמרתי “אם תורה היא לא עקבית אין לה מודל” שהיה שקול ל”אם לתורה יש מודל היא עקבית”. מערכת ההוכחה שלנו עדיין לא יודעת לבטא את העקרון הזה בצורה תחבירית (אין לה את היכולת ליצור מחרוזת שזה מה שהיא אומרת), אז נוסיף לה תבנית אקסיומה שאומרת בדיוק את זה: \( \left(\neg\alpha\to\neg\beta\right)\to\left(\beta\to\alpha\right) \). זוהי תבנית אקסיומה מס' 3. אתם מוזמנים לבדוק שזוהי אכן טאוטולוגיה.

עכשיו הוכחה של “משפט ההוכחה בשלילה” היא קלה. בואו נבחר בתור \( \psi \) טאוטולוגיה כלשהי ש-\( \Phi \) יודעת להוכיח (\( \varphi\to\left(\varphi\to\varphi\right) \) לאלו מכם שרוצים להיות קונקרטיים, אבל זה חסר חשיבות). אז הוכחה של \( \varphi \) תיראה כך:

1. \( \neg\varphi\to\neg\psi \) (ממשפט הדדוקציה).
2. \( \left(\neg\varphi\to\neg\psi\right)\to\left(\psi\to\varphi\right) \) (תבנית אקסיומה 3).
3. \( \psi\to\varphi \) (\( \mbox{MP} \) על 1,2).
4. \( \psi \) (טאוטולוגיה שיכיחה מ-\( \Phi \)).
5. \( \varphi \) (\( \mbox{MP} \) על 3,4).

סיימנו עם משפט ההוכחה בשלילה, אבל רק בהנחה שעקרון הפיצוץ אכן מתרחש במערכת ההוכחה שלנו. בפועל זה קורה בדיוק “בזכות” תבנית אקסיומה 3: נניח ש-\( \Phi \) אינה עקבית, כלומר \( \Phi\vdash\varphi \) וגם \( \Phi\vdash\neg\varphi \) עבור \( \varphi \) כלשהו. בואו נראה הוכחה של \( \psi \) כלשהו:

1. \( \left(\neg\psi\to\neg\varphi\right)\to\left(\varphi\to\psi\right) \) (תבנית אקסיומה 3).
2. \( \neg\varphi\to\left(\neg\psi\to\neg\varphi\right) \) (תבנית אקסיומה 1).
3. \( \neg\varphi \) (ניתן להוכחה מ-\( \Phi \)).
4. \( \neg\psi\to\neg\varphi \) (\( \mbox{MP} \) על 2,3).
5. \( \varphi\to\psi \) (\( \mbox{MP} \) על 1,4).
6. \( \varphi \) (ניתן להוכחה מ-\( \Phi \)).
7. \( \psi \) (\( \mbox{MP} \) על 5,6).

בואו נבין עכשיו למה הטענה “אם \( \Phi \) עקבית אז יש לה מודל” גוררת את משפט השלמות. יהא \( \varphi \) כך ש-\( \Phi\models\varphi \). אם \( \Phi\cup\left\{ \neg\varphi\right\} \) אינה עקבית, אז סיימנו; ממשפט ההוכחה בשלילה, \( \Phi\vdash\varphi \). אחרת, אם \( \Phi\cup\left\{ \neg\varphi\right\} \) כן עקבית, אז מההנחה שלנו קיים לה מודל. המודל הזה הוא השמה שמספקת בו זמנית את כל פסוקי \( \Phi \) ואת \( \neg\varphi \); אבל מכיוון ש-\( \Phi\models\varphi \) כל השמה שמספקת את כל פסוקי \( \Phi \) מספקת גם את \( \varphi \) - סתירה לכך שההשמה מספקת את \( \neg\varphi \). זה הכל.

שימו לב שההוכחה הזו איננה קונסטרוקטיבית; היא לא מצביעה על האופן שבו אפשר, בהינתן \( \varphi \) שמקיים \( \Phi\models\varphi \), לבנות הוכחה עבורו. האם אתם מזהים היכן בהוכחה השלב הלא קונסטרוקטיבי? ההוכחה בסך הכל אומרת “לא ייתכן ש-\( \Phi\cup\left\{ \neg\varphi\right\} \) עקבית”, ומכאן אנחנו מסיקים ש-\( \Phi\vdash\varphi \) ממשפט ההוכחה בשלילה; אבל משפט ההוכחה בשלילה עצמו מניח שבגלל ש-\( \Phi\cup\left\{ \neg\varphi\right\} \) לא עקבית, אז קיימת הוכחה במערכת הזו לזוג כלשהו של \( \psi \) ו-\( \neg\psi \). אחרי שיש לנו ביד את ההוכחה הזו, כל מה שנשאר הוא כמה צעדים פשוטים ומוגדרים היטב. אבל איך ההוכחה של הזוג הזה נראית, אין לנו מושג.

אפשר לחשוב על מה שעשינו גם כך: לפני רגע רצינו להוכיח טענה על התחביר באמצעות הנחה על הסמנטיקה (הנחנו ש-\( \Phi\models\varphi \) ורצינו להסיק \( \Phi\vdash\varphi \)), ועכשיו הפכנו את היוצרות: אנחנו מניחים משהו על התחביר - ש-\( \Phi \) עקבית - ורוצים להסיק מזה משהו על הסמנטיקה - שיש ל-\( \Phi \) מודל. כל שארית ההוכחה שלנו תעסוק בנסיון לבנות ל-\( \Phi \) את המודל הזה. הבניה הזו נתקלת בקושי לא צפוי, עם פתרון לא צפוי, שלטעמי הוא החלק המקסים ביותר כאן: מסתבר שקשה למצוא מודל ל-\( \Phi \) דווקא בגלל שיש לנו יותר מדי חופש בחירה - יש יותר מדי השמות שיש להן “פוטנציאל להיות מודל ל-\( \Phi \)”. הפתרון יהיה להרחיב את \( \Phi \) לתורה עקבית גדולה בהרבה, שהרבה יותר קשה לספק אותה - יהיה לה רק מודל אחד ויחיד. דווקא בגלל אובדן החופש הזה, הרבה יותר קל למצוא את המודל הזה; אין לנו שום בחירה בבניה שלו ולכן הוא ממש “בונה את עצמו”.

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

כאמור, המטרה שלי היא למצוא מודל ל-\( \Phi \), אבל זה לא קל. מודל ל-\( \Phi \) הוא סדרה של ערכי \( \mbox{T/F} \) שאני מציב למשתנים \( X_{1},X_{2},X_{3},\dots \). אני יכול להתחיל בלהגיד “טוב, אם הצבת \( \mbox{T} \) ב-\( X_{1} \) לא הופכת אף פסוק ב-\( \Phi \) לבלתי ניתן לסיפוק, נציב בו \( \mbox{T} \); אחרת, נציב בו \( \mbox{F} \), ואם גם זה לא יספק אני איכשהו אראה ש-\( \Phi \) לא עקבית”. נניח לרגע שאני יכול לעשות את ה”איכשהו” הזה, האם זה פתר את בעיותי? לא, כי הצבתי ערך רק למשתנה \( X_{1} \). עכשיו צריך להציב גם ל-\( X_{2} \), בהינתן ההצבה שבחרתי עבור \( X_{1} \). ואז צריך עבור \( X_{3} \) בהינתן ההצבה שבחרתי עבור \( X_{1},X_{2} \). ואז ב-\( X_{12414} \) אני אתקע פתאום כי אראה שאין לי דרך לספק את \( \Phi \) לא כשמציבים \( \mbox{T} \) ולא כשמציבים \( \mbox{F} \) ב-\( X_{12414} \), אבל, אם רק הייתי בוחר להציב את הערך ההפוך ב-\( X_{1} \), אז כתוצאה מכך הייתה מתקבלת סדרת הצבות שונה לגמרי בכל שאר המשתנים, ואז לא הייתי נתקע ב-\( X_{12414} \). אבל איך אני יכול לוודא את זה? ואיך אני יכול מראש לבחור בהצבה ה”נכונה” עבור כל משתנה? לא ברור. זו הסיבה שהגישה הנאיבית הזו נתקעת.

מה שעושים הוא להגיד “יש לנו פה יותר חופש פעולה מלכתחילה, בואו נגביל אותו!”. נגביל אותו בצורה כזו שעבור כל משתנה רק אחת משתי ההצבות האפשריות של ערכים עבורו לא תוביל לסתירה. לשם כך אנחנו צריכים להרחיב את \( \Phi \) על ידי הוספת פסוקים, ולקבל \( \Phi\subseteq\Psi \). כל מודל של \( \Psi \) הוא גם מודל של \( \Phi \) (כי הוא מספק את כל פסוקי \( \Phi \), ובנוסף לכך עוד פסוקים נוספים) ולכן יהיה די להראות ש-\( \Psi \) הוא בעל מודל. נותר לעשות שלושה דברים: לתאר איך \( \Psi \) הזה אמור להיראות שכל כך יפשט לנו את החיים, להסביר איך מרחיבים את \( \Phi \) לקבלת \( \Psi \), ולהסביר למה ל-\( \Psi \) יש מודל.

כדי להסביר מה \( \Psi \) יהיה בדיוק אין מנוס מלהכניס למשחק מושג מבלבל: תורה שלמה. \( \Psi \) הוא תורה שלמה אם לכל פסוק \( \varphi \) מתקיים \( \Psi\vdash\varphi \) או \( \Psi\vdash\neg\varphi \). כלומר, \( \Psi \) מוכיחה או מפריכה כל פסוק. המילה שלמות כאן והמילה שלמות ב”משפט השלמות לתחשיב הפסוקים” מדברות על דברים שונים לגמרי; השלמות של \( \Psi \) היא שלמות של תורה - קבוצת פסוקים, שממנה “נובע כל דבר או שלילתו”; השלמות של משפט השלמות היא שלמות של מערכת ההוכחה - היא אומרת שבהינתן קבוצת פסוקים שממנה נובע לוגית משהו, אז מערכת ההוכחה מאפשרת לנו להוכיח את אותו המשהו מתוך קבוצת הפסוקים. גם אחרי שאוכיח את משפט השלמות, לא תנבע מכך שום תוצאה כמו “כל קבוצת פסוקים \( \Phi \) היא שלמה”. בקיצור, זוהי בחירה אומללה של שימוש באותה מילה כדי לתאר שני מושגים שונים (אם כי לא בלתי קשורים לזה לזה, כפי שאפשר להבין מכך שאני מדבר על תורה שלמה כחלק מההוכחה של משפט השלמות). הבלבול זלג גם לתחשיב היחסים: ב”משפט השלמות של גדל” השלמות היא של מערכת ההוכחה (זהו אנלוג מורכב יותר למשפט השלמות שאנחנו מוכיחים כרגע) וב”משפטי אי השלמות של גדל” השלמות היא של תורות מסויימות (אריתמטיות, עקביות ואפקטיביות, אם זה אומר לכם משהו).

הטענה שלי היא שלתורה שלמה ועקבית יש בדיוק מודל יחיד - כלומר, לכל משתנה יש בדיוק ערך אחד שאפשר להציב בו כדי שעדיין נספק את \( \Psi \) - אבל קודם כל בואו נבין כיצד ניתן להרחיב את \( \Phi \) לתורה שלמה \( \Psi \). התשובה פשוטה: בכוח! נמספר את כל הפסוקים בעולם במספור כלשהו \( \varphi_{1},\varphi_{2},\varphi_{3},\dots \) כך שכל פסוק מופיע מתישהו במספור; ועכשיו נבנה סדרה של תורות \( \Phi_{0},\Phi_{1},\Phi_{2},\dots \) כך ש-\( \Phi_{0}=\Phi \) ולכל \( n>0 \), אחד משניים: אם \( \Phi_{n-1}\cup\left\{ \neg\varphi_{n}\right\} \) עקבית, אז \( \Phi_{n}=\Phi_{n-1}\cup\left\{ \neg\varphi_{n}\right\} \); אחרת, \( \Phi_{n}=\Phi_{n-1} \). במילים אחרות, אנחנו עוברים פסוק פסוק ולכל פסוק כזה אנחנו בודקים אם ניתן להוסיף את שלילתו לתורה שלנו. אם אפשר (כלומר, העקביות נשמרת) אנחנו מוסיפים. אחרת לא. בצורה הזו די ברור שכל אחת מה-\( \Phi_{n} \) היא עדיין תורה עקבית בפני עצמה. עכשיו בואו ונגדיר \( \Psi=\bigcup\Phi_{n} \), כלומר \( \Psi \) כוללת את כל הפסוקים שמופיעים ולו באחד מה-\( \Phi_{n} \)-ים, ובגלל שבנינו אותם בצורה כזו ש-\( \Phi_{0}\subseteq\Phi_{1}\subseteq\Phi_{2} \), בעצם אפשר לומר שאם פסוק כלשהו נמצא ב-\( \Psi \) אז הוא נמצא בכל ה-\( \Phi_{n} \)-ים החל ממקום מסויים.

אנחנו צריכים להשתכנע ש-\( \Psi \) עקבית וש-\( \Psi \) שלמה. הוכחת העקביות מנצלת את העובדה שהוכחה היא תמיד סופית. נניח לרגע ש-\( \Psi \) לא עקבית, כלומר \( \Psi\vdash\varphi \) וגם \( \Psi\vdash\neg\varphi \) עבור איזה שהוא פסוק \( \varphi \). אז יש לנו שתי הוכחות ששתיהן סופיות; מכיוון שהן סופיות, משתמשים בהן במספר סופי של הנחות מ-\( \Psi \); בשל בניית \( \Psi \) נובע מכך שכל ההנחות הללו נמצאות בכל ה-\( \Phi_{n} \)-ים החל מ-\( n \) מסויים, ולכן החל מ-\( n \) מסויים גם \( \Phi_{n}\vdash\varphi \) ו-\( \Phi_{n}\vdash\neg\varphi \) בסתירה לכך שכל ה-\( \Phi_{n} \) עקביות.

בכל הנוגע לשלמות, הבה וניקח \( \varphi \) כלשהו ונוכיח כי \( \Psi\vdash\varphi \) או \( \Psi\vdash\neg\varphi \). השאלה היא מה קרה בבניית \( \Psi \) בשלב שבו שקלנו אם להוסיף את \( \neg\varphi \) לתורה או לא (כלומר, בשלב של \( \varphi_{n}=\varphi \)). מצד אחד, אם \( \Phi_{n-1}\cup\left\{ \neg\varphi_{n}\right\} \) לא הייתה עקבית, אז ממשפט ההוכחה בשלילה \( \Phi_{n-1}\vdash\varphi_{n}=\varphi \) ולכן גם \( \Psi\vdash\varphi \) (על ידי אותה הוכחה פורמלית בדיוק); מצד שני, אם \( \Phi_{n-1}\cup\left\{ \neg\varphi_{n}\right\} \) כן הייתה עקבית אז \( \neg\varphi\in\Phi_{n} \) ולכן \( \neg\varphi\in\Psi \) ולכן \( \Psi\vdash\neg\varphi \) על ידי הוכחה פשוטה במיוחד: \( \neg\varphi \) עצמה ותו לא.

סיימנו את השלב הזה: הראינו שכל תורה עקבית \( \Phi \) ניתנת להרחבה לתורה עקבית ושלמה \( \Psi \). נותר להוכיח רק שלתורה עקבית ושלמה יש מודל. בניגוד למקרה של \( \Phi \) כללית, עבור \( \Psi \) השלמה אין בעיה להגיד במפורש מה המודל הזה, פשוט כי אין לנו ממש ברירה: לכל משתנה \( X_{i} \), מתקיים בדיוק אחד משניים: \( \Psi\vdash X_{i} \) או \( \Psi\vdash\neg X_{i} \), וזאת כי \( \Psi \) שלמה. אז אם \( \Psi\vdash X_{i} \) נגדיר ש-\( X_{i} \) מקבל \( \mbox{T} \) בהשמה שלנו, ואם \( \Psi\vdash\neg X_{i} \) נגדיר ש-\( X_{i} \) מקבל \( \mbox{F} \). עד כדי כך פשוט. רק צריך להשתכנע שההשמה הזו באמת מספקת כל פסוק ב-\( \Psi \). ליתר דיוק, נוכיח את הטענה החזקה יותר “לכל פסוק \( \varphi \), \( \Psi\vdash\varphi \) אם ורק אם ההשמה מספקת את \( \varphi \)” (חזקה יותר, כי אם \( \varphi\in\Psi \) אז בפרט \( \Psi\vdash\varphi \)).

את ההוכחה הזו אפשר לעשות באינדוקציה על המבנה של פסוקים \( \mbox{WFF} \). כזכור, פסוק כזה הוא או \( \varphi=X_{i} \) עבור משתנה כלשהו, או שהוא מהצורה \( \varphi=\neg\alpha \), או שהוא מהצורה \( \varphi=\alpha\to\beta \).

במקרה הראשון, אם \( \Psi\vdash X_{i} \) אז על פי ההגדרה של ההשמה, \( X_{i} \) מקבל \( \mbox{T} \); ואם \( X_{i} \) קיבל \( \mbox{T} \) אז בהכרח \( \Psi\vdash X_{i} \) (כי אחרת היה מתקיים \( \Psi\vdash\neg X_{i} \) ואז \( X_{i} \) היה מקבל \( \mbox{F} \) בהשמה).

בשני המקרים הבאים נוכל להניח ש-\( \alpha,\beta \) כבר מקיימים את התכונה שהם יכיחים מ-\( \Psi \) אם ורק אם ההשמה מספקת אותם; זוהי בדיוק הנחת האינדוקציה.

במקרה השני, \( \Psi\vdash\neg\alpha \) אם ורק אם \( \Psi\not\vdash\alpha \) (כי \( \Psi \) עקבית ושלמה), כלומר אם ורק אם ההשמה נותנת ל-\( \alpha \) ערך \( \mbox{F} \), כלומר אם ורק אם ההשמה נותנת ל-\( \neg\alpha \) ערך \( \mbox{T} \). זה היה קל; המקרה השלישי טיפה יותר קשה.

במקרה השלישי, נניח קודם כל כי \( \Psi\vdash\alpha\to\beta \). אם \( \alpha \) מקבלת ערך \( \mbox{F} \) בהשמה, סיימנו כי \( \alpha\to\beta \) תמיד יקבל ערך \( \mbox{T} \); אז נניח ש-\( \alpha \) מקבלת \( \mbox{T} \) ולכן, מהנחת האינדוקציה, \( \Psi\vdash\alpha \), ומכאן ש-\( \Psi\vdash\beta \) (כי ההוכחה פשוט מייצרת את \( \alpha \) ואת \( \alpha\to\beta \) ואז מבצעת \( \mbox{MP} \)) ומהנחת האינדוקציה, \( \beta \) מסתפקת על ידי ההשמה. זה מסיים כיוון אחד של ההוכחה; בכיוון השני, נניח כי \( \alpha\to\beta \) הסתפקה בהשמה ונוכיח כי \( \Psi\vdash\alpha\to\beta \). יש שתי דרכים שבהן \( \alpha\to\beta \) יכלה להסתפק; או ש-\( \beta \) קיבלה \( \mbox{T} \), או ש-\( \alpha \) קיבלה \( \mbox{F} \). אם \( \beta \) קיבלה \( \mbox{T} \) אז מהנחת האינדוקציה, \( \Psi\vdash\beta \) ולכן בוודאי ש-\( \Psi\cup\left\{ \alpha\right\} \vdash\beta \) וממשפט הדדוקציה, \( \Psi\vdash\alpha\to\beta \). במקרה השני, אם \( \alpha \) קיבלה \( \mbox{F} \), אז \( \Psi\vdash\neg\alpha \) ולכן \( \Psi\cup\left\{ \alpha\right\} \) לא עקבית. אם היא לא עקבית, אז היא מוכיחה הכל, כולל \( \beta \); שוב קיבלנו ש-\( \Psi\cup\left\{ \alpha\right\} \vdash\beta \) וממשפט הדדוקציה, \( \Psi\vdash\alpha\to\beta \). זה מסיים את הוכחת משפט השלמות.

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