בפוסט הקודם על לוגיקה סיימתי להוכיח את משפט השלמות לתחשיב הפסוקים. לפני שנעבור הלאה, אני רוצה להתעכב טיפה על המסקנות מכל זה ולדבר עוד קצת על ההוכחה. בואו נתחיל ממסקנה לא טריוויאלית ממשפט השלמות: משפט הקומפטיות. משפט הקומפטיות אומר בפשטות שלתורה \(\Phi\) יש מודל אם ורק אם לכל תת-תורה סופית \(\Phi^{\prime}\subseteq\Phi\) יש מודל. כיוון אחד הוא מובן מאליו (אם לתורה יש מודל, כך גם לכל תת-תורה שלה) אבל הכיוון השני ממש לא – הכיוון השני אומר שאיכשהו אפשר "למשוך למעלה" מודלים עבור חלקים סופיים קטנים של \(\Phi\) ולקבל מהם מודל עבור כל \(\Phi\), שעשויה להיות גדולה ומסובכת בהרבה.

באופן כללי, תוצאות בסגנון "הנה קבוצה \(A\). אם משהו מתקיים לכל תת-קבוצה סופית של \(A\), הוא מתקיים לכל \(A\)" הן משהו שיש בו קריצה אינטואיטיבית ומובילות להרבה טעויות של מתחילים שעושים אותן כשאי אפשר. דוגמה פשוטה: אם \(A=\left(0,1\right)=\left\{ x\in\mathbb{R}|0<x<1\right\} \), הקטע הפתוח של כל הממשיים בין 0 ו-1 לא כולל, אז מתקיימת התכונה שלכל תת-קבוצה סופית של \(A\) יש איבר מינימלי (איבר שקטן מכל יתר האיברים בקבוצה), פשוט כי בכל קבוצה סופית יש איבר מינימלי, אבל ב-\(A\) עצמה אין איבר מינימלי (טוענים ש-\(a\in A\) כלשהו הוא האיבר המינימלי? נההה, \(\frac{a}{2}\) קטן יותר). אז טענה כמו משפט הקומפקטיות היא לא מובנת מאליה, וחשוב לזכור שמשפט הקומפטיות לא מדבר רק על "תורה" ותו לא; הוא מדבר על כל מה שניתן לתאר באמצעות תחשיב הפסוקים. למשל, הראיתי בפוסט קודם איך תחשיב הפסוקים יכול לתאר צביעות של גרף: \(\Phi\) תיארה מה זו צביעה חוקית, ומודל של \(\Phi\) היה צביעה חוקית שכזו. עם טיפה עבודה אפשר להראות בעזרת משפט הקומפקטיות שלגרף יש צביעה חוקית ב-\(n\) צבעים אם ורק אם לכל תת-גרף סופי שלו יש צביעה חוקית ב-\(n\) צבעים. דוגמה אחרת היא ריצופים של המישור: אפשר להראות בעזרת משפט הקומפקטיות שהמישור כולו ניתן לריצוף על ידי קבוצת אריחים כלשהי אם ורק אם כל תת-קבוצה סופית של המישור ניתנת לריצוף על ידי קבוצת האריחים הזו. אלו לא תוצאות טריוויאליות (אם כי ניתן להוכיח אותן גם בדרכים אחרות).

איך מוכיחים את משפט הקומפקטיות בהינתן משפט השלמות? פשוט: משפט השלמות אומר שאם \(\Phi\) עקבית אז קיים לה מודל. גם הכיוון השני ברור – אם ל-\(\Phi\) יש מודל אז אין סיכוי שהיא תוכיח דבר ושלילתו, כי המודל הזה לא יכול לספק גם את הדבר וגם את שלילתו. לכן כדי להוכיח את משפט הקומפקטיות מספיק להראות ש-\(\Phi\) עקבית אם ורק אם כל תת-תורה \(\Phi^{\prime}\) סופית היא עקבית (כלומר, להוכיח שהתכונה "עקביות" כן ניתנת ל"הרמה כלפי מעלה" מכל תת-הקבוצות הסופיות אל הכל). ההוכחה פשוטה למדי ומתבססת על כך שהוכחות פורמליות הן סופיות: מצד אחד, אם \(\Phi^{\prime}\) היא תת-תורה לא עקבית של \(\Phi\) אז אפשר להוכיח ממנה דבר ושלילתו, ואותה הוכחה בדיוק תקפה גם עבור \(\Phi\) ולכן \(\Phi\) אינה עקבית; בכיוון השני, אם \(\Phi\) אינה עקבית אז ניתן להוכיח ממנה דבר ושלילתו ומכיוון שההוכחות הללו סופיות הן משתמשות במספר סופי של הנחות מתוך \(\Phi\), אז פשוט נגדיר את \(\Phi^{\prime}\) להיות קבוצת כל ההנחות הללו, ואז \(\Phi^{\prime}\) לא תהיה עקבית. הוכחנו ש"\(\Phi^{\prime}\) אינה עקבית אם ורק אם קיימת תת-תורה סופית \(\Phi^{\prime}\subseteq\Phi\) שאינה עקבית", וזו טענה ששקולה לוגית למה שרצינו להוכיח.

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

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

משפט טיכונוף אומר שאם יש לנו מרחב מכפלה טופולוגי, \(X=\prod_{\lambda\in\Lambda}X_{\lambda}\) כאשר כל אחד מהאיברים במכפלה \(X_{\lambda}\) הוא קומפקטי, אז גם \(X\) קומפקטי. ההגדרה המקובלת למרחב קומפקטי היא "לכל כיסוי של המרחב על ידי קבוצות פתוחות יש תת-כיסוי סופי", כלומר אפשר להסתפק רק במספר סופי של קבוצות מאותו כיסוי כדי לכסות את כל המרחב. כשיש לנו מכפלה פשוטה, נאמר \(A\times B\), וכל אחד מהרכיבים קומפקטי, אפשר עוד איכשהו לעבוד עם ההגדרה הזו: מצטמצמים איכשהו להתעסקות קודם כל עם קבוצות מהצורה \(A\times\left\{ b\right\} \) לכל \(b\in B\) ובסופו של דברים מצליחים לאלתר תת-כיסוי סופי מתוך כל כיסוי. אם עשינו את זה למכפלה של שני מרחבים אפשר באינדוקציה לקבל את אותו דבר עבור מכפלה של \(n\) מרחבים לכל \(n\) טבעי, אבל זה נגמר בערך כאן. טיכונוף מטפל במספר כלשהו של מוכפלים, גם (ובעיקר) אינסופי, ואפילו לא בהכרח בן מניה. גישת הכיסויים לא עובדת טוב במיוחד במקרים הללו, והאופן שבו מוכיחים את המשפט הוא באמצעות הגדרה שקולה לקומפקטיות (שהיא גם ההגדרה היותר מעניינת עבורנו, כשאנחנו באים להשתמש בטיכונוף כדי להוכיח את משפט הקומפקטיות).

ההגדרה הולכת כך: קבוצה \(\mathcal{A}\) של תת-קבוצות של מרחב מסויים היא בעלת תכונת החיתוכים הסופיים אם לכל תת-קבוצה סופית של \(\mathcal{A}\), החיתוך של כל האיברים של תת-הקבוצה הזו לא ריק. מרחב הוא קומפקטי אם בהינתן קבוצה \(\mathcal{A}\) של קבוצות סגורות שמקיימת את תכונת החיתוכים הסופיים, החיתוך של כל הקבוצות בה לא ריק. אם כן, המטרה שלנו בהוכחת טיכונוף היא זו: ניקח קבוצה \(\mathcal{A}\) של תת-קבוצות סגורות של \(X\), ונבנה איכשהו איבר ב-\(\bigcap\mathcal{A}\).

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

בספרו המצויין Topology מציג Munkres את האינטואיציה למה שקורה בהמשך בצורה בהירה ומדוייקת ביותר. הוא מתחיל בדוגמה קונקרטית עבור מכפלה של שני מרחבים, \(X_{1},X_{2}\). האינטואיציה הזו זו: קודם כל נטיל את כל \(\mathcal{A}\) על \(X_{1}\), ונקבל אוסף של קבוצות ב-\(X_{1}\) שעדיין מקיים את תכונת החיתוכים הסופיים (למה?) ומהקומפקטיות של \(X_{1}\) נובע שיש נקודה בחיתוך של האוסף המוטל הזה, \(x_{1}\). בדומה יש נקודה \(x_{2}\) בחיתוך של \(\mathcal{A}\) כשהוא מוטל על \(X_{2}\). כעת ניקח את \(\left(x_{1},x_{2}\right)\) והרי לנו נקודה ב-\(\bigcap\mathcal{A}\) ב-\(X_{1}\times X_{2}\)… אה, לא. כאן מגיעה הבעיה: אף אחד לא ערב לנו ש-\(\left(x_{1},x_{2}\right)\) אכן שייכת לקבוצות של \(\mathcal{A}\).

מונקרס מביא את הדוגמה הקונקרטית הבאה: \(X_{1}=X_{2}=\left[0,1\right]\) (ולכן \(X_{1}\times X_{2}\) הוא ריבוע היחידה הסגור ב-\(\mathbb{R}^{2}\)). בתור \(\mathcal{A}\) הוא בוחר את כל האליפסות עם מוקדים ב-\(p=\left(\frac{1}{3},\frac{1}{3}\right)\) ו-\(q=\left(\frac{1}{2},\frac{2}{3}\right)\). לא אעתיק את הציורים מהספר שלו – יש גבול לפלגיאטים שאני מרשה לעצמי היום – אבל אם תחשבו על זה קצת או תציירו לעצמכם יתברר מייד שהחיתוך של כל האליפסות הללו כולל בדיוק את הקטע הישר שקצותיו הן \(p,q\).

כמו כן, הטלה של \(\mathcal{A}\) על \(X_{1}\) תניב אוסף של קטעים סגורים שכולם מכילים את \(\left[\frac{1}{3},\frac{1}{2}\right]\) והטלה של \(\mathcal{A}\) על \(X_{2}\) תניב אוסף של קטעים סגורים שכולם מכילים את \(\left[\frac{1}{3},\frac{2}{3}\right]\). אז אפשר לבחור \(x_{1}=\frac{1}{2}\) ו-\(x_{2}=\frac{1}{2}\), רק שלמרבה אסוננו \(\left(\frac{1}{2},\frac{1}{2}\right)\) בכלל לא נמצאת על הישר שמחבר את \(p,q\)…

כאן הקורא של מונקרס מתערב: "אהא!" הוא אומר. "ביצעת בחירה גרועה! אם אחרי הבחירה של \(x_{1}=\frac{1}{2}\) היית בוחר \(x_{2}=\frac{2}{3}\) היית מקבל נקודה בחיתוך של \(\mathcal{A}\)". הבעיה, כפי שמונקרס מציין, היא שהיה לנו יותר מדי חופש בחירה בבחירת הנקודות שלנו ב-\(X_{1}\) ו-\(X_{2}\). ובכן, האם זה לא נשמע מוכר לאלו מכם שראו את הוכחת משפט השלמות? מייד לאחר מכן מונקרס מציג את הפתרון: נרחיב את האוסף \(\mathcal{A}\) תוך שאנו משמרים את תכונת החיתוכים הסופיים שלו; ונרחיב אותו לקבוצה "גדולה ככל האפשר". בקבוצה הזו כבר לא יהיה לנו חופש בחירה כלל וניתן לקוות שהנקודה היחידה האפשרית שנקבל בשיטה שלעיל תהיה אכן בחיתוך של \(\mathcal{A}\). זה בדיוק הרעיון שהיה גם בהוכחת משפט השלמות. זו כמובן לא הפעם הראשונה ולא הפעם העשירית שאותו רעיון (מחוכם ולא טריוויאלי) עצמו צץ בתחומים שנראים לא קשורים האחד לשני, אבל בכל פעם שזה קורה, זה תענוג.

ההמשך כבר יותר מסובך מאשר במשפט השלמות, פשוט כי הסיטואציה יותר מסובכת. במשפט השלמות היה קל יחסית לבנות את ההרחבה של "\(\mathcal{A}\)", אבל במשפט טיכונוף הכרחי לגרור פנימה את הלמה של צורן, וגם אז העבודה לא נגמרת, אבל ההוכחה היא יחסית ישירה החל מהשלב הזה – עיקר הקושי הוא ברעיון הבסיסי שכבר הצגתי. מי שמעוניין במלוא הפרטים מוזמן לקרוא את מונקרס, או להמתין ליום שבו אכתוב פוסט (ראוי מאוד) שיוקדש להוכחה הזו.

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

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

בפוסט הקודם הצגתי את התחביר של תחשיב הפסוקים – האופן שבו בונים נוסחאות מאוסף של סימנים, על פי כללים מסויימים, והתוצאה הייתה קבוצה שקראתי לה 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).

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

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

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

בואו נתחיל עם אמירה של חזאים: "מחר ירד גשם או שמחר לא ירד גשם". זו אמירה מעצבנת, כי היא לא באמת אומרת לנו כלום, ועם זאת ברור לנו שהיא נכונה תמיד. לאמירות כאלו, שהן נכונות תמיד ולא משנה מה, קוראים טאוטולוגיות (יש למילה משמעות דומה בשפת היום יום ובספרות, אבל לא זהה; טאוטולוגיה "ספרותית" היא להגיד כמה פעמים את אותו הדבר, כמו למשל "החוק הראשון של מועדון הטאוטולוגיה הוא החוק הראשון של מועדון הטאוטולוגיה" של xkcd – אמירה שהיא מטבעה גם טאוטולוגיה מתמטית). הבה ונתבונן בטאוטולוגיה מתחום הספורט דווקא: "או שננצח במשחק או שלא ננצח בו" הוא ביטוי שגור בקרב מאמנים מסויימים. ואילו המתמטיקאי יכול להגיד "או ש-\(p\) ראשוני, או ש-\(p\) איננו ראשוני". בכל המקרים הללו הטאוטולוגיה היא בעצם אותה הטאוטולוגיה: זו טענה מהצורה "או שמשהו, או שלא משהו", כש"משהו" יכול להיות כל מה שנרצה. למעשה, זה בכלל לא משנה מהו אותו ה"משהו" – הנכונות של הטאוטולוגיה נובעת מהמבנה של המשפט, ולא מהתוכן שאנחנו יוצקים בו. בכתיבה מתמטית פורמלית, המשפט הזה יכתב בתור \(X\vee\neg X\): כאן \(X\) הוא משתנה שיכול לקבל ערך של "אמת" או "שקר", ו-\(\vee\) מייצג את "או", ו-\(\neg\) מייצג את "לא". קראו את הפסוק הזה בתור "איקס או לא איקס". הנה לנו דוגמה לפסוק בתחשיב הפסוקים.

הבה ונישאר בדוגמאות מתחום הספורט. "אם נבקיע יותר שערים מהקבוצה השניה, אז ננצח" הוא עוד פסוק לגיטימי: במתמטית כותבים אותו בתור \(X\to Y\), כלומר "איקס גורר וואי". דוגמה אחרת לאותו פסוק אבל מתחום אחר היא אמרתו של פסקל כי "אם היה אפה של קליאופטרה קצר יותר ההיסטוריה היתה כולה אחרת". כאן \(X\) הוא "אפה של קליאופטרה היה קצר יותר" ו-\(Y\) הוא "ההיסטוריה היתה כולה אחרת". כעת, כשמדובר על המשפט של ה"אם נבקיע יותר שערים" ברור לנו שהוא נכון; אבל בקשר למשפט של פסקל לא ממש ברור אם הוא נכון. אנחנו נזקקים לידע חיצוני כלשהו כדי לדעת את זה – האם באמת לאף של קליאופטרה הייתה השפעה קריטית על מרקוס אנטוניוס? למעשה, אין לנו ממש דרך לדעת. מכאן כבר ברור לנו ש-\(X\to Y\) הוא כנראה לא טאוטולוגיה: קיימת האפשרות שהפסוק הזה יהיה נכון או לא נכון, בהתאם למשמעות של \(X,Y\). זה קיים גם בדוגמת הכדורגל; אם חוקי הכדורגל היו שונים כך שמי שמבקיע יותר דווקא מפסיד, אז "אם נבקיע יותר שערים מהקבוצה השניה, אז ננצח" היה משפט שגוי. ברור לנו, אם כן, שהנכונות של \(X\to Y\) היא לא צורנית בלבד.

הפסוקים שתחשיב הפסוקים עוסק בהם הם בדיוק אמירות פשוטות מהצורה שהצגתי כאן – כאלו שמערבות "משהו"-ים שיכולים להיות נכונים או לא נכונים, ומחוברים זה לזה באמצעות קשרים לוגיים של "או" (\(\vee\)), "וגם" (\(\wedge\)), "אז" (\(\to\)) ו"לא" (\(\neg\)). פסוק בנוי בערך כמו ביטוי חשבוני עם נעלמים: בשביל להבין מי בא קודם משתמשים בסוגריים, כלומר \(\left(X\to Y\right)\vee\left(Y\to Z\right)\) הוא יצור שונה מ-\(X\to\left(Y\vee\left(Y\to Z\right)\right)\).

כמו בביטוי חשבוני רגיל עם נעלמים, אפשר להציב ערכים בנעלמים; במקרה שלנו הערכים הם "אמת" או "שקר", \(T\) או \(F\). מרגע שהצבנו ערכים במשתנים, אפשר לחשב את הערך של הפסוק – שוב, כמו שמחשבים את ערכו של ביטוי חשבוני. כך למשל \(X\vee Y\) מקבל ערך \(T\) אם לפחות אחד מהמשתנים קיבל ערך \(T\); \(X\wedge Y\) מקבל \(T\) רק אם שניהם קיבלו \(T\); ו-\(X\to Y\) מקבל \(T\) אלא אם \(X\) קיבל \(T\) ו-\(Y\) קיבל \(F\). מכיוון שלכל משתנה יש רק שני ערכים אפשריים, אפשר להגדיר קשר בקלות פשוט על ידי כתיבת הערך שהוא מחזיר עבור כל זוג קלטים אפשרי – לדבר כזה קוראים טבלת האמת של הקשר. קצת קומבינטוריקה: אם יש לנו קשר שפועל על שני משתנים, אז יש לו \(2^{2}\) קלטים אפשריים (\(\left(F,F\right),\left(T,F\right),\left(F,T\right),\left(T,T\right)\)) ולכן יש רק \(2^{\left(2^{2}\right)}=16\) קשרים שונים שפועלים על שני משתנים (קשר מוגדר באופן מוחלט על ידי ערכי האמת שהוא מחזיר לכל קלט אפשרי; יש 4 קלטים אפשריים ולכל אחד בוחרים אחד משני פלטים אפשריים ולכן יש \(2^{4}\) אפשרויות). זה לא כל כך הרבה; אפשר לשבת ולכתוב את כולם אם יש לכם מספיק זמן. הסיבה שבגללה מכל הקשרים הללו בחרנו לדבר דווקא על \(\vee,\wedge,\to\) היא לא מקרית; אלו כנראה הקשרים הכי נוחים להבנה והכי פשוטים לתיאור מילולי.

שאלה אחת שכדאי לטפל בה מראש היא – האם הקשרים הללו מגבילים את יכולת ההבעה שלנו? האם יש משפטים שלא ניתן למדל אם אין לנו אותם? למשל, משפט כמו "בגרף סופי וקשיר יש מעגל אוילרי אם ורק אם דרגת כל צומת זוגית" הוא בבסיסו טענת \(A\leftrightarrow B\), שמקבלת ערך "אמת" כל עוד הערכים של \(A,B\) זהים ואחרת מקבלת "שקר"; אבל אפשר לבנות אותה גם באופן שונה מהקשרים שכבר יש לנו: \(\left(A\to B\right)\wedge\left(B\to A\right)\). די קל לראות, על ידי בדיקה של כל המקרים, שגם זה פסוק שמקבל ערך "אמת" רק כאשר ערכי האמת של \(A,B\) שווים.

באופן כללי, בעזרת \(\wedge,\vee,\neg\) אפשר לכתוב פסוק עבור כל פונקציה \(f:\left\{ F,T\right\} ^{n}\to\left\{ F,T\right\} \), לא משנה על כמה משתנים היא. זה כבר די קסם – בעזרת כמה קשרים פשוטים על שני משתנים, אפשר לכתוב ביטוי עבור כל פונקציה על משתנים לוגיים, לא משנה כמה מסובכת. נסו להשוות את זה לעובדה שבעזרת ארבע פעולות החשבון הבסיסיות ממש אי אפשר לכתוב את רוב הפונקציות האפשריות מהרציונליים לעצמם (למה? ובכן, למי שמכיר עוצמות – יש \(2^{\aleph_{0}}\) פונקציות כאלו אבל רק \(\aleph_{0}\) נוסחאות שאפשר לכתוב עם פעולות החשבון, כל עוד דורשים שהן יהיו סופיות).

ובכן, איך הקסם עובד? אפשר לחשוב על \(f\) כעל אוסף של \(n\)-יות של ערכים לוגיים שבדיוק עליהם היא מקבלת ערך \(T\) (אם \(f\) מחזירה \(F\) לכל דבר, אז \(X\wedge\neg X\) הוא פסוק שמחשב אותה). בואו נניח ש-\(\left(a_{1},\dots,a_{n}\right)\) היא \(n\)-יה כזו של ערכים לוגיים (כלומר, \(a_{i}\in\left\{ T,F\right\} \)) ונגדיר פסוק \(\left(l_{1}\wedge\dots\wedge l_{n}\right)\) כך ש-\(l_{i}=X_{i}\) אם \(a_{i}=T\), ו-\(l_{i}=\neg X_{i}\) אם \(a_{i}=F\). קל לראות שהפסוק הזה מקבל ערך \(T\) אך ורק על ההשמה \(\left(a_{1},\dots,a_{n}\right)\) למשתנים \(X_{1},\dots,X_{n}\); וכעת נוסחה עבור \(f\) נקבל על ידי ביצוע \(\vee\) לכל הפסוקים הללו. למשל, עבור \(f\left(X_{1},X_{2},X_{3}\right)\) שמחזירה \(T\) אם בדיוק שניים מתוך שלושת המשתנים קיבלו \(T\) נקבל את הנוסחה \(\left(X_{1}\wedge X_{2}\wedge\neg X_{3}\right)\vee\left(X_{1}\wedge\neg X_{2}\wedge X_{3}\right)\vee\left(\neg X_{1}\wedge X_{2}\wedge X_{3}\right)\). נוסחה בצורה הזו (\(\mbox{\vee}\) של תת-פסוקים – "פסוקיות" – שכל אחד מהם הוא \(\wedge\) של משתנה או של \(\neg\) של משתנה) נקראת נוסחת DNF (מלשון Disjunctive normal form). מה שראינו הוא שלכל פונקציה לוגית יש DNF ולכן די בשלושת הקשרים שמשתתפים ב-DNF כדי לכתוב פסוק שמבטא כל פונקציה לוגית אפשרית. מכיוון שאפשר לקבל את \(\vee\) ואת \(\wedge\) באמצעות הקשרים \(\neg\) ו-\(\to\), אפשר להסתפק רק בשני קשרים אלו כדי לקבל כל פונקציה (ולעתים קרובות זה מה שעושים בספרי לוגיקה, כי יותר קל להוכיח משפטים כשיש פחות קשרים שצריך לדבר עליהם). למעשה, יש גם קשרים לוגיים שאיתם לבד אפשר לכתוב כל נוסחה: הקשר הידוע ביותר הוא NAND, שמסומן ב-\(\uparrow\) ומוגדר בתור \(\neg\left(X_{1}\wedge X_{2}\right)\) (כלומר, מקבל \(F\) רק כאשר \(X_{1}=X_{2}=T\)). זה תרגיל נחמד להוכיח שאכן אפשר לקבל ממנו את \(\neg\) ואת (למשל) \(\to\) ולכן די להשתמש רק בו. אז למה לא עושים את זה בדרך כלל? כי עדיין יותר פשוט להבין נוסחאות שכתובות עם \(\to,\neg\).

אם כבר הצגתי את DNF, כדאי להציג גם צורה נורמלית נוספת של פסוקים שדואלית לה – CNF (Conjunctive normal form). זו נוסחה שמורכבת מ-\(\wedge\) של פסוקיות שכל אחת מהן כוללת \(\vee\) של משתנים ושלילות של משתנים ("משתנה או שלילה של משתנה" נקרא בדרך כלל "ליטרל" כדי לפשט עניינים). לכל טבלת אמת קיים פסוק בצורת CNF שמממש אותה; אבל זה כבר לא מובן מאליו כמו DNF. נסו שניה לחשוב למה ותראו שזה בעייתי. הפתרון הוא תעלול קטן ונחמד: אם אנחנו רוצים לבנות פסוק עבור טבלת אמת כלשהי, נתחיל מפסוק \(\varphi\) בצורת DNF עבור טבלת האמת ההפוכה; עכשיו פסוק ה-CNF המתאים יהיה מה שמתקבל מ-\(\neg\varphi\) כשמפעילים עליו את כללי דה מורגן, שאציג כרגע.

יש שני כללי דה-מורגן: האחד הוא ש-\(\neg\left(X\vee Y\right)=\neg X\wedge\neg Y\) והשני הוא ש-\(\neg\left(X\wedge Y\right)=\neg X\vee\neg Y\) (כאן שוויון פירושו שקילות). למה זה נכון? ובכן, אפשר לבדוק את הנוסחאות הללו באופן ישיר על ידי הצבה של כל הערכים האפשריים ב-\(X,Y\), ואפשר גם לחשוב בהגיון שניה – להגיד "זה לא נכון שמתמטיקה היא גם משעממת וגם פדנטית" זה כמו להגיד "או שהמתמטיקה לא משעממת או שהמתמטיקה לא פדנטית. אולי שניהם".

פסוק DNF נראה כך: \(C_{1}\vee C_{2}\vee\dots\vee C_{n}\) כשכל \(C_{i}\) הוא מהצורה \(\left(l_{1}\wedge l_{2}\wedge\dots\wedge l_{k}\right)\). אחרי שנפעיל \(\neg\) עליו נקבל \(\neg C_{1}\wedge\dots\wedge\neg C_{n}\), ואחרי שנכניס את ה-\(\neg\) לתוך כל אחד מהסוגריים נקבל בהם \(\left(\neg l_{1}\vee\dots\vee\neg l_{k}\right)\). ייתכן שנקבל כך דברים כמו \(\neg\neg X\) שאותם אפשר כמובן להחליף ב-\(X\); סוף הסיפור. אם כן, כלל האצבע פשוט: רוצים CNF? קודם תמצאו DNF של ההפך, ואז תהפכו.

זה מסיים את הדיון בתחביר – באופן שבו ניתן לבנות סדרות של סימנים שתהיה להן משמעות עבורנו; בפרט, שהמבנה שלהן יהיה ברור לנו באופן חד משמעי. לנוסחאות כאלו קוראים Well-formed formulas, או WFF-ים; אני אקרא להן פשוט "פסוקים" או "נוסחאות" ואתייחס לסדרות אחרות של סימנים כאל ג'יבריש חסר חשיבות. נקודה חשובה אחת שקודם רפרפתי מעליה היא שבהינתן נוסחה, יש לה "קריאה יחידה" – דרך אחת בלבד לתאר אותה בתור עץ שבו העלים הם משתנים והצמתים הם הפעולות הלוגיות – כמו בביטוי חשבוני רגיל, שגם לו יש קריאה יחידה אם שמים סוגריים בצורה נבונה. די הופתעתי לגלות שיש ספרי לוגיקה רציניים (מנדלסון…) שפשוט מתעלמים מהעניין הזה לחלוטין. לתשומת לב כל מי שטוען שלוגיקאים הם פדנטיים.