תחשיב הפסוקים - על נביעה לוגית והוכחות

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

האובייקט הבסיסי בתחשיב הפסוקים היה משתנים לוגיים, \( X_{1},X_{2},X_{3},\dots \). ההנחה היא שאנחנו מייחסים למשתנים הללו משמעות כלשהי, אבל מבחינה פורמלית תחשיב הפסוקים לא מתעניין במשמעות הזו. כל מה שהוא מתעניין בו הוא האם המשתנים מקבלים ערך \( \mbox{T} \) או \( \mbox{F} \). בואו נתחיל עם דוגמה קונקרטית כדי להבין איך זה הולך. את המושג של גרף אני מניח שרוב הקוראים מכירים, אבל למי שלא: גרף \( G=\left(V,E\right) \) מורכב מקבוצה כלשהי (לא בהכרח סופית) של צמתים \( V \), ושל זוגות של צמתים \( E\subseteq V^{2} \) שנקראים קשתות. חושבים על כך כאילו אם \( \left(u,v\right)\in E \) אז הצמתים \( u,v \) מחוברים בקשת, ואחרת לא. עכשיו, את הצמתים של \( G \) אפשר לצבוע; אני אניח לצורך פשטות שמותר לצבוע אותם רק באדום, כחול או ירוק. פורמלית, צביעה היא פונקציה \( f:V\to\left\{ \mbox{R,G,B}\right\} \) שלכל צומת מתאימה את הצבע שבו הוא נצבע (כל צומת חייב להיצבע). האתגר בדרך כלל הוא למצוא צביעה “חוקית” שבה אין שני צמתים שמחוברים בקשת וצבועים באותו הצבע - כלומר, \( f\left(u\right)\ne f\left(v\right) \) לכל קשת \( \left(u,v\right)\in E \) בגרף. לא תמיד יש צביעה כזו; למעשה, הבעיה “האם ניתן לצבוע גרף \( G \) נתון באופן חוקי באמצעות שלושה צמתים” היא בעיה \( \mbox{NP} \)-שלמה, מה שאומר שהיא ככל הנראה קשה לפתרון מבחינה חישובית. למה זה בכלל מעניין מישהו? ובכן, בעולם הגדול צביעה של גרפים היא הפשטה נאה לבעיות של הקצאת משאבים; בעולם הקטן שלנו היא פשוט דוגמה יפה למה שאני רוצה לדבר עליו.

נניח שנתון לי גרף \( G \). כעת, לכל צומת \( v \) אני הולך להגדיר שלושה משתנים: \( X_{R}^{v},X_{G}^{v},X_{B}^{v} \). אם \( X_{R}^{v}=\mbox{T} \), אני מפרש את זה בתור האמירה “הצומת \( v \) נצבע בצבע \( \mbox{R} \)”. מבחינת תחשיב הפסוקים עצמו, כל מה שהוא יודע זה ש”המשתנה \( X_{R}^{v} \) קיבל את הערך \( \mbox{T} \) בהשמה” - כל היתר הוא בדמיון שלי (גם לקרוא למשתנה הזה \( X_{R}^{v} \) זה בדמיון שלי; בפועל כל המשתנים הם מהצורה \( X_{k} \) כאשר \( k \) הוא מספר טבעי כלשהו).

כעת, כל השמה למשתנים מגדירה צביעה של הגרף \( G \), אבל אף אחד לא מבטיח לי שהצביעה הזו הגיונית בכלל; ייתכן שיש צומת שנצבע ביותר מאשר צבע אחד; ייתכן שיש צומת שלא נצבע באף צבע; וכמובן, אף אחד לא מבטיח שהצביעה תהיה חוקית במובן זה שכל שני צמתים שכנים לא צבועים באותו הצבע. בכדי להבטיח שהצביעה תהיה בסדר אני צריך להוסיף מגבלות על הצביעה - כלומר, על ההשמות החוקיות. האופן שבו אני עושה את זה הוא להגדיר קבוצה של פסוקים, \( ,\Phi_{G} \) כך שכל השמה שמספקת את כל הפסוקים של \( \Phi_{G} \) חייבת להיות, בפרשנות שלי, צביעה חוקית. אילו פסוקים \( \Phi_{G} \) תכיל?

ובכן, לכל צומת \( v\in V \), \( \Phi_{G} \) תכיל את הפסוק \( X_{R}^{v}\vee X_{G}^{v}\vee X_{B}^{v} \) שאומר “הצומת \( v \) צבוע לפחות בצבע אחד”. היא תכיל את הפסוק \( \neg\left(X_{R}^{v}\wedge X_{G}^{v}\right)\wedge\neg\left(X_{R}^{v}\wedge X_{B}^{v}\right)\wedge\neg\left(X_{G}^{v}\wedge X_{B}^{v}\right) \) שאומר “הצומת \( v \) אינה צבועה ביותר מצבע אחד”; ולכל קשת \( \left(u,v\right)\in E \), \( \Phi_{G} \) תכיל את הפסוק \( \neg\left(X_{R}^{v}\wedge X_{R}^{u}\right)\wedge\neg\left(X_{G}^{v}\wedge X_{G}^{u}\right)\wedge\neg\left(X_{B}^{v}\wedge X_{B}^{u}\right) \) שאומר “הצמתים \( v,u \) אינם צבועים באותו הצבע”.

זה משלים את התיאור של \( \Phi_{G} \), אבל הכיף רק מתחיל. לא קשה להוכיח (באופן מתמטי “רגיל”, לא באופן פורמלי) שאם הגרף \( G \) מכיל ולו קשת יחידה, אז לא כל הצמתים בגרף בעלי אותו צבע (כי מה עם שני הצמתים שמחוברים בקשת?). בואו נניח לצורך פשטות ש-\( G \) סופי וקבוצת הקשתות שלו לא ריקה, אז הפסוק הבא נכון עבור כל השמה שמספקת את כל פסוקי \( \Phi_{G} \): \( \neg\left(\bigwedge_{v\in V}X_{R}^{v}\right)\wedge\neg\left(\bigwedge_{v\in V}X_{G}^{v}\right)\wedge\neg\left(\bigwedge_{v\in V}X_{B}^{v}\right) \). הפסוק הזה כמובן דומה לפסוקים שהוספנו ל-\( \Phi_{G} \), אבל הוא לא נמצא ב-\( \Phi_{G} \). מצד שני, די בבירור הוא “נובע” מתוך \( \Phi_{G} \) - גם מבחינה אינטואיטיבית, אבל גם מבחינה פורמלית; באופן כללי אנחנו אומרים שפסוק \( \varphi \) נובע לוגית מקבוצת פסוקים \( \Phi \) אם כל השמה שמספקת את \( \Phi \) (דהיינו, מספקת את כל הפסוקים ב-\( \Phi \)) מספקת גם את \( \varphi \). מסמנים זאת \( \Phi\models\varphi \). בפרט, פסוקים שכל השמה מספקת אותם נקראים טאוטולוגיות ומסמנים זאת \( \models\varphi \) (אבל כמובן שאם \( \varphi \) טאוטולוגיה אז אפשר לכתוב גם \( \Phi\models\varphi \) לכל \( \Phi \) שרק נרצה).

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

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

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

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

שלוש הדרישות שלעיל לא באמת מגדירות בשום צורה איך מערכת ההוכחה תעשה את מה שאנחנו דורשים ממנה, ובצדק; למה להגביל את עצמנו? תחת זאת, אפשר פשוט לדבר על מערכות הוכחה קונקרטיות ולראות שהן מקיימות את הדרישות הבסיסיות שלנו. מה שאציג כעת תהיה מקרה פרטי של מחלקה גדולה של מערכות הוכחה “מערכות הילברט” (שהקרדיט על תיאורן הפורמלי, פחות או יותר, מגיע להילברט ולפרגה). במערכת כזו יש לנו אקסיומות, ויש לנו כללי היסק, והוכחה של \( \varphi \) מתוך קבוצת הנחות \( \Phi \) היא סדרה סופית של פסוקים \( \psi_{1},\dots,\psi_{n} \) כך ש-\( \psi_{n}=\varphi \), וכל \( \psi_{i} \) הוא או אקסיומה, או הנחה מתוך \( \Phi \), או שהוא נובע מ-\( \psi_{j} \)-ים קודמים על ידי הפעלת כלל היסק. כדי שהמערכת תהיה אפקטיבית רק צריך לבחור אקסיומות שניתן לזהות אותן באופן אלגוריתמי (כלומר, או שתהיה קבוצה סופית של אקסיומות, או - אם זו קבוצה אינסופית - שלפחות יהיה קל לזהות מהי אקסיומה, למשל כי היא מתאימה לאיזו שהיא תבנית ברורה) ולבחור כללי היסק שניתן לזהות את הפעלתם באופן אלגוריתמי.

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

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

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

1. \( \alpha\to\beta \) (ניתן להוכחה מ-\( \Phi \)).
2. \( \alpha \) (הנחה).
3. \( \beta \) (\( \mbox{MP} \) על 1,2).

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

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

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

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

1. \( \beta \) (אקסיומה/הנחה).
2. \( \beta\to\left(\alpha\to\beta\right) \) (תבנית אקסיומה מס' 1).
3. \( \alpha\to\beta \) (\( \mbox{MP} \) על 1,2)

אוקיי, זה היה קל. אז טיפלנו במקרה שבו \( \beta \) היא אקסיומה/הנחה; דחינו לעת עתה את המקרה שבו \( \beta=\alpha \); מה נותר? המקרים שבהם \( \beta \) אינה אקסיומה/הנחה/\( \alpha \) ועם זאת מוכיחים את \( \beta \) מתוך \( \Phi\cup\left\{ \alpha\right\} \). מסקנה: בסיטואציה כזו, \( \beta \) חייבת להתקבל על ידי הפעלת \( \mbox{MP} \) על שני פסוקים שניתן להניח באינדוקציה (על אורך ההוכחה) שעליהם משפט הדדוקציה כבר חל. כלומר, יש איזה שהוא פסוק \( \gamma \) כך ש-\( \Phi\cup\left\{ \alpha\right\} \vdash\gamma\to\beta \) וגם \( \Phi\cup\left\{ \alpha\right\} \vdash\gamma \), ובגלל שאפשר להניח שמשפט הדדוקציה מתקיים עבורם, אז \( \Phi\vdash\alpha\to\gamma \) ו-\( \Phi\vdash\alpha\to\left(\gamma\to\beta\right) \). האם די לנו בשני אלו, בתבנית האקסיומה הנוכחית וב-\( \mbox{MP} \) כדי להוכיח את \( \alpha\to\beta \)? ובכן, לא. אז מה עושים? מוסיפים עוד תבנית אקסיומה שתפורה בדיוק לסיטואציה הזו: התבנית \( \left[\alpha\to\left(\gamma\to\beta\right)\right]\to\left[\left(\alpha\to\gamma\right)\to\left(\alpha\to\beta\right)\right] \). תסתכלו על הרכיבים של התבנית ותראו אם אתם מזהים מהיכן היא מגיעה; ובדקו באופן כלשהו שהתבנית הזו היא אכן טאוטולוגיה. לתבנית האקסיומה הזו אני קורא תבנית אקסיומה מס' 2.

עכשיו ההוכחה היא טריוויאלית:

1. \( \alpha\to\gamma \) (ניתן להוכחה מ-\( \Phi \)).
2. \( \alpha\to\left(\gamma\to\beta\right) \) (ניתן להוכחה מ-\( \Phi \)).
3. \( \left[\alpha\to\left(\gamma\to\beta\right)\right]\to\left[\left(\alpha\to\gamma\right)\to\left(\alpha\to\beta\right)\right] \) (תבנית אקסיומה מס' 2).
4. \( \left(\alpha\to\gamma\right)\to\left(\alpha\to\beta\right) \) (\( \mbox{MP} \) על 2,3).
5. \( \alpha\to\beta \) (\( \mbox{MP} \) על 1,4).

נשאר לנו רק לטפל בחוב מההתחלה - להראות שאפשר להוכיח את \( \alpha\to\alpha \). עכשיו יש לנו כלי נשק חדש - שתי תבניות אקסיומה שנמצאות ברשותנו ואנחנו לא מהססים להשתמש בהן. מפתה להשתמש בתבנית הראשונה כשמציבים בה \( \alpha \) במקום \( \beta \) ומקבלים \( \alpha\to\left(\alpha\to\alpha\right) \), רק שזה לא עוזר לנו במיוחד כי אנחנו לא יכולים להוכיח את \( \alpha \) בשום צורה. כנראה שתבנית אקסיומה 1 לבדה לא ממש תעזור לנו וצריך להשתמש גם ב-2. בואו נציב גם ב-2 \( \alpha \) במקום הכל ונראה מה נקבל:

1. \( \alpha\to\left(\alpha\to\alpha\right) \) (תבנית אקסיומה מס' 1).
2. \( \left[\alpha\to\left(\alpha\to\alpha\right)\right]\to\left[\left(\alpha\to\alpha\right)\to\left(\alpha\to\alpha\right)\right] \) (תבנית אקסיומה מס' 2).
3. \( \left(\alpha\to\alpha\right)\to\left(\alpha\to\alpha\right) \) (\( \mbox{MP} \) על 1,2).

ו.. נתקענו. כדי להפיק תועלת מ-\( \left(\alpha\to\alpha\right)\to\left(\alpha\to\alpha\right) \) נצטרך להוכיח את \( \alpha\to\alpha \), וזה בדיוק מה שאנחנו מנסים להוכיח! אז מה יצא לנו מכל זה?

אם כן, אולי לא כדאי מייד להציב גם ב-\( \beta \) וגם ב-\( \gamma \) את \( \alpha \)? אולי יש הצבה קצת יותר מועילה שאפשר לעשות? עם זאת, לא כדאי להציב דברים מופרעים יותר מדי: אם אנחנו מתכננים להשתמש ב-\( \left[\alpha\to\left(\gamma\to\beta\right)\right]\to\left[\left(\alpha\to\gamma\right)\to\left(\alpha\to\beta\right)\right] \), זה אומר שנצטרך להפעיל עליה \( \mbox{MP} \). זה אומר שנצטרך להוכיח איכשהו את \( \left[\alpha\to\left(\gamma\to\beta\right)\right] \), וזה אומר ש-\( \left[\alpha\to\left(\gamma\to\beta\right)\right] \) חייב להתאים למבנה של תבנית אקסיומה כלשהי - מן הסתם, תבנית אקסיומה מס’ 1. שימו לב איך אין לנו ברירה ואנחנו ממש נדחפים לכך שנהיה חייבים לבחור \( \beta=\alpha \), אחרת \( \left[\alpha\to\left(\gamma\to\beta\right)\right] \) לעולם לא תתאים לתבנית של אקסיומה מס’ 1. לעומת זאת, ל-\( \gamma \) יש לנו חופש בחירה מוחלט; בואו נתחיל נסיון הוכחה חדש ונראה מה ישתלם לנו לבחור בתור ערכו של \( \gamma \).

1. \( \left[\alpha\to\left(\gamma\to\alpha\right)\right]\to\left[\left(\alpha\to\gamma\right)\to\left(\alpha\to\alpha\right)\right] \) (תבנית אקסיומה מס' 2).
2. \( \alpha\to\left(\gamma\to\alpha\right) \) (תבנית אקסיומה מס' 1).
3. \( \left(\alpha\to\gamma\right)\to\left(\alpha\to\alpha\right) \) (\( \mbox{MP} \) על 1,2).

אנחנו כמעט שם! רק צריך לבחור ערך ל-\( \gamma \) כך ש-\( \alpha\to\gamma \) ייראה כמו תבנית האקסיומה \( \alpha\to\left(\beta\to\alpha\right) \). אם כן, מתבקש לבחור \( \gamma=\alpha\to\alpha \), ולקבל:

1. \( \left[\alpha\to\left(\alpha\to\alpha\right)\right]\to\left(\alpha\to\alpha\right) \) (הצבנו \( \gamma=\alpha\to\alpha \)).
2. \( \alpha\to\left(\alpha\to\alpha\right) \) (תבנית אקסיומה מס' 1).
3. \( \alpha\to\alpha \) (\( \mbox{MP} \) על 1,2).

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

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