מכסחי הכמתים

פורסם בתאריך 6 במאי 2013 על ידי gadial

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

מה זה? שניה לפני שאפציץ עם ההגדרות הפורמליות, אינטואיציה: הנוסחאות בלוגיקה מסדר ראשון נבנות מתוך כל מני רכיבים בסיסיים שמחוברים עם פעולות לוגיות כמו "וגם", "או", "שלילה", "גורר", וגם שני כמתים – "לכל" ו"קיים". הכמתים הללו אחראים לחלק לא מבוטל מהסיבוך שיש לתורות בלוגיקה מסדר ראשון. הנה דוגמה פשוטה, ואני מזהיר מראש שאני הולך לשקר בה קצת ולגלות איך שיקרתי רק בסוף: את הטענה "\(t\) הוא פתרון של המשוואה \(ax^{2}+bx+c=0\)" קל לבדוק אם נותנים לנו ליד את הערכים של \(t\) ושל \(a,b,c\). לעומת זאת, הטענה "קיים \(t\) שהוא פתרון של המשוואה \(ax^{2}+bx+c=0\)" היא כבר טענה מורכבת משמעותית יותר, שמצריכה אותנו להבין את המשוואה הזו.

איך "מבינים" משוואה כזו? קודם כל צריך להבין מה בכלל ההקשר של המשוואה. האם זו משוואה מעל המספרים הממשיים? מעל המרוכבים? מעל המספרים השלמים בלבד? מודולו 7? האם אנחנו ב-\(p\)-אדיים? על הירח? במאדים? בואו נניח שאנחנו מדברים על המשוואה מעל \(\mathbb{R}\), כדי שיהיה מעניין. פורמלית, האופן שבו כותבים את הטענה הלוגית שטוענת שקיים פתרון למשוואה הוא פשוט הנוסחה\(\exists x\left(ax^{2}+bx+c=0\right)\), והשאלה שלנו היא אם במודל של המספרים הממשיים (שבו פעולות החיבור והכפל הן הפעולות ה"רגילות" על ממשיים) הפסוק הזה הוא בעל ערך אמת. ואיך יודעים דבר כזה? הרי ברור שאי אפשר לעבור על כל המספרים הממשיים ולנסות אחד אחד להציב אותם במשוואה, יש הרבה יותר מדי מהם.

ובכן, קרוב לודאי שרובכם זוכרים משהו על משוואות ריבועיות ויודעים שהתשובה לשאלה תלויה איכשהו בערכים של \(a,b,c\), שהם "משתנים חופשיים" של הפסוק. עבור הצבות מסויימות של ערכים למשתנים יהיה פתרון למשוואה, ועבור הצבות אחרות – לא. איך יודעים? ובכן, נוסחת השורשים מלמדת אותנו שפתרונות המשוואה \(ax^{2}+bx+c=0\) הם \(\frac{-b\pm\sqrt{b^{2}-4ac}}{2a}\). הפתרונות הללו עשויים להיות מספרים מרוכבים ולא ממשיים טהורים; מתי זה עשוי לקרות אם \(a,b,c\) הם ממשיים טהורים? ובכן, רק אם \(b^{2}-4ac<0\) ואז הוצאת השורש תחזיר מספר מרוכב (או, למקרה שלא שמעתם על מספרים מרוכבים, היא פשוט תהיה "פעולה לא חוקית" ולכן לא יהיה פתרון – ממשי – למשוואה). אם \(b^{2}-4ac\ge0\) אז בודאות מוחלטת יש פתרון למשוואה (בגלל החשיבות של הביטוי \(b^{2}-4ac\) יש לו שם וסימון מיוחדים: דיסקרימיננטה, והוא מסומן ב-\(\Delta\)). זה אומר שהנוסחה \(\exists x\left(ax^{2}+bx+c=0\right)\) שקולה לוגית לנוסחה \(b^{2}-4ac\ge0\). למה הכוונה ב"שקולה לוגית"? בחרו ערכים קונקרטיים עבור \(a,b,c\); מובטח לנו שלשתי הנוסחאות יהיה אותו ערך אמת עבור הערכים הללו.

מה ההבדל בין שתי הנוסחאות? ובכן, \(b^{2}-4ac\ge0\) היא נוסחה פשוטה משמעותית יותר מ-\(\exists x\left(ax^{2}+bx+c=0\right)\) כי אין בה כמתים – כדי לבדוק אם היא נכונה או לא, פשוט מבצעים חישוב קצר שכולל את \(a,b,c\), ואת זה אפשר לעשות חיש קל, בזמן שעבור \(\exists x\left(ax^{2}+bx+c=0\right)\) לא הייתה לנו שום שיטה ישירה לדעת אם היא נכונה או לא. הצלחנו "לחסל" את הכמת שהופיע בנוסחה הזו ולהחליף אותה בנוסחה שקולה, פשוטה יותר, ובכך הפכנו בעייה שנראתה בלתי אפשרית מבחינה חישובית (לבדוק אם יש פתרון למשוואה) לבעיה טריוויאלית מבחינה חישובית. זה, על רגל אחת, כל הרעיון שמאחורי חיסול כמתים.

כמובן שמייד צצות כמה שאלות. הנוסחה \(b^{2}-4ac\ge0\) בכלל לא נראית דומה לנוסחה \(\exists x\left(ax^{2}+bx+c=0\right)\), אז איך הגענו אליה? האם יש שיטה כללית לחיסול כמתים? האם תמיד אפשר לבצע חיסול כמתים? כמה זה מסובך? התשובה היא שחיסול כמתים הוא עניין קשה. לעתים קרובות צריך ידע נוסף כדי לבצע אותו עבור מקרים קונקרטיים, וברוב המקרים אי אפשר לבצע אותו בכלל. אבל לפעמים כן אפשר לעשות אותו באופן כללי מאוד – להראות שעבור תורה מסויימת קיים חילוץ כמתים עבור כל הנוסחאות (תכף אסביר מה זה בדיוק אומר – זו לא הגדרה טריוויאלית) וכשהפלא הזה קורה, קורים דברים מגניבים למדי. גולת הכותרת שאני חותר אליה (אבל לא אגיע אליה בפוסט הזה) היא ההוכחה שאריתמטיקת פרסבורגר היא כריעה, וההוכחה עוברת דרך חילוץ כמתים. מה זו אריתמטיקת פרסבוגר? זו כמעט התורה שעליה חל משפט אי השלמות של גדל (שמוכיח שתורת המספרים אינה כריעה), רק בלי כפל. אסביר יותר כשאגיע לשם.

לפני שנעבור לפורמליזם, זמן להסביר איך שיקרתי לכם, ואני בטוח שחלקכם שמו לב לזה. נוסחת השורשים היא נכונה אך ורק כאשר \(a\ne0\). אם \(a=0\) אז \(ax^{2}+bx+c=0\) היא בכלל משוואה ממעלה ראשונה, והתנאי \(b^{2}-4ac\ge0\) תמיד מתקיים למרות שייתכן שלמשוואה לא יהיה פתרון. מתי ייתכן שאין לה פתרון? ובכן, באופן כללי למשוואה \(bx+c=0\) יש את הפתרון \(x=-\frac{c}{b}\), אז די בבירור יש לה פתרון תמיד, למעט המקרה שבו \(b=0\) אבל \(c\ne0\). לכן הנוסחה השקולה האמיתית ל-\(\exists x\left(ax^{2}+bx+c=0\right)\) היא לא \(b^{2}-4ac\ge0\) אלא \(\left(a\ne0\wedge b^{2}-4ac\ge0\right)\vee\left(a=0\wedge\left(b\ne0\vee c=0\right)\right)\), שהיא יותר גדולה ומסורבלת (ולכן לא הצגתי אותה מייד אלא שיקרתי) אבל גם כן חסרת כמתים.

ועכשיו בואו נעבור להגדרות. כפי שהדוגמה שנתתי רומזת, כשמדברים על חילוץ כמתים תמיד עושים את זה ביחס לתורה ספציפית. מה זו תורה? בואו נזכיר בקצרה. בלוגיקה מסדר ראשון תמיד יש לנו מילון שאנחנו עובדים ולפיו ואומר לנו מהם סימני היחסים, הפונקציות והקבועים שבהם אנחנו יכולים להשתמש. למשל, בדוגמה שלעיל, המילון כלל סימני פונקציה עבור חיבור וכפל (\(ax^{2}\), למשל, הוא קיצור של \(a\cdot x\cdot x\)) וסימן יחס עבור \(\ge\) (וגם עבור \(=\) אבל אני נוהג להניח ש-\(=\) מגיע עם כל תורה מסדר ראשון ומפורש תמיד כ"שווה"). בעזרת הסימונים של המילון והסימונים הלוגיים הסטנדרטיים (למשל \(\wedge\) עבור "וגם", או סימונים עבור משתנים) אפשר לבנות נוסחאות. תורה \(T\) היא בסך הכל אוסף של פסוקים, כש"פסוק" הוא נוסחה בלי משתנים חופשיים, ולכן משהו שעבור כל מבנה אפשרי יש לו ערך אמת או שקר. אה, מה זה מבנה? טוב, זו כבר חזרה די ארוכה… יש לי פוסט שמציג את הכל במסודר, ואפשר גם לקרוא בכל ספר לוגיקה סטנדרטי.

עכשיו, אם \(T\) היא תורה ו-\(\varphi\left(\overline{x}\right)\) היא נוסחה שאולי יש בה משתנים חופשיים (אני מסמן ב-\(\overline{x}\) "וקטור של משתנים חופשיים"), אנחנו משתמשים בסימון \(T\models\varphi\left(\overline{x}\right)\) ("\(\varphi\) נובעת לוגית מ-\(T\)") אם לכל מודל \(\mathcal{M}\) שמספק את \(T\), וכל וקטור של איברים \(\overline{a}\) שנלקחים מתוך \(D^{\mathcal{M}}\), \(\varphi\left(\overline{a}\right)\) מסתפקת (מקבלת את הערך True). עד כאן, הכל ברור. זה מוביל אותנו להגדרה האולטרה-חשובה הבאה: שתי נוסחאות \(\varphi,\psi\) הן שקולות מודולו התורה \(T\), אם \(T\models\varphi\leftrightarrow\psi\). כלומר, לכל מודל של \(T\) וכל השמה מתוך המודל למשתנים של \(\varphi,\psi\) (יכולים להיות להם משתנים משותפים וגם משתנים לא משותפים), או ששתי הנוסחאות מסתפקות, או ששתיהן אינן מסתפקות. חשוב מאוד להדגיש שזו אינה שקילות "אבסולוטית" אלא היא מאוד תלויה בתורה \(T\), שכן התורה היא מעין "מסננת" שקובעת אילו מודלים בכלל רלוונטיים לצורך השקילות של \(\varphi,\psi\). הנה דוגמה ממש מטופשת להבהרת הנקודה: הנוסחה \(\exists x\left(x^{2}=a\right)\) שקולה לנוסחה \(a=a\) (שהיא נוסחה שתמיד מקבלת את ערך האמת True) כאשר המודל הרלוונטי הוא המספרים המרוכבים עם הפרשנות ה"רגילה"; אבל במודל של המספרים הממשיים, הנוסחה אינה נכונה אם \(a\) הוא שלילי. לכן המודל הוא קריטי כאן.

והנה הגענו להגדרה. לתורה \(T\) יש חיסול כמתים אם לכל נוסחה \(\varphi\) בשפה של התורה קיימת נוסחה \(\psi\) שקולה מודולו \(T\) שהיא חסרת כמתים. אפשר לחדד טיפה את ההגדרה הזו ולהגדיר אוסף של "נוסחאות בסיסיות" שהן עצמן יכולות להכיל כמתים, וחיסול כמתים פירושו יהיה שאפשר לקבל מ-\(\varphi\) נוסחה שקולה שבנויה מתוך הנוסחאות הבסיסיות באמצעות פעולות בוליאניות בלבד (\(\wedge,\vee,\neg,\to,\leftrightarrow\)) ובלי כמתים. לא נצטרך את זה בהמשך, אז מבחינתי "חסר כמתים" זה אכן חסר כמתים. לגמרי.

בואו נתחיל עם קצת עבודה טכנית. ראשית, הסימנים הלוגיים \(\wedge,\vee,\neg,\to,\leftrightarrow\) הם נחמדים אבל רובם מיותרים: אפשר להסתפק ב-\(\wedge,\vee,\neg\) בלבד, כי \(\alpha\to\beta\equiv\left(\neg\alpha\vee\beta\right)\) ו-\(\alpha\leftrightarrow\beta\equiv\left(\alpha\to\beta\right)\wedge\left(\beta\to\alpha\right)\) (למעשה, אפשר גם לוותר על אחד מבין \(\vee,\wedge\) אבל אשתמש בשניהם בהמשך מטעמי נוחות). שנית, גם \(\forall\) מיותר כי \(\forall x\alpha\left(x\right)\equiv\neg\exists x\neg\alpha\left(x\right)\). לכן מלכתחילה נתעניין בפועל רק בנוסחאות שמורכבות מ-\(\neg,\wedge,\vee,\exists\) ורק עליהן נצטרך להוכיח דברים (מטעמי נוחות אני עדיין אשתמש בסימנים האחרים כשזה מקל עלי, מתוך הבנה שהם בסך הכל סימונים מקוצרים לנוסחאות לעיל).

עכשיו, בדוגמה שלמעלה עיקר האתגר היה לעבור מנוסחה עם כמת "קיים" יחיד לנוסחה בלי כמת כזה בכלל. מסתבר שזה גם האתגר באופן כללי – אם יודעים לטפל רק בכמת "קיים" אחד, אז יש חיסול כמתים. פורמלית, אשתמש במילה "ליטרל" כדי לתאר נוסחה אטומית (כזו שהיא יחס שמופעל על שמות עצם) או שלילה של נוסחה אטומית. אני טוען שאם עבור תורה \(T\) ניתן להמיר כל נוסחה מהצורה \(\exists x\left(\alpha_{1}\wedge\dots\wedge\alpha_{n}\right)\), כאשר כל \(\alpha\) הוא ליטרל, לנוסחה שקולה חסרת כמתים מודולו \(T\), אז ל-\(T\) יש חיסול כמתים. ההוכחה של הטענה היא באינדוקציה על מבנה כל הנוסחאות, ובואו נעשה אותה כדי לקבל תחושה עד כמה זה פשוט:

ראשית, אם \(\alpha\) היא נוסחה אטומית, אז אין בה כמתים, ולכן היא מהווה את חיסול הכמתים של עצמה (כמובן ש-\(T\models\alpha\leftrightarrow\alpha\)).

עכשיו, אם \(\alpha=\neg\beta\) כאשר ל-\(\beta\) כבר יש חיסול כמתים, כלומר יש \(\beta^{\prime}\) חסרת כמתים ששקולה ל-\(\beta^{\prime}\), אז \(\alpha^{\prime}=\neg\beta^{\prime}\) היא נוסחה שקולה חסרת כמתים עבור \(\alpha\). בדומה, השקול של נוסחה מהצורה \(\alpha\wedge\beta\) הוא הנוסחה \(\alpha^{\prime}\wedge\beta^{\prime}\) כך ש-\(\alpha^{\prime}\) ו-\(\beta^{\prime}\) הם השקולים של \(\alpha,\beta\).

נשאר לנו לטפל בנוסחה מהצורה \(\exists x\alpha\), כאשר ל-\(\alpha\) קיימת נוסחה שקולה \(\alpha^{\prime}\) חסרת כמתים (למרות – וזו נקודה מהותית – שב-\(\alpha\) יכולים להיות כמתים). אז \(\exists x\alpha\) שקול ל-\(\exists x\alpha^{\prime}\) (את זה כדאי להוכיח אם לא משוכנעים בכך). עכשיו, \(\alpha^{\prime}\) חסר כמתים, אז אפשר לכתוב אותו בצורה קנונית של פסוק בתחשיב הפסוקים: DNF. כלומר, לכתוב \(\alpha^{\prime}=\bigvee C_{i}\) כך שכל \(C_{i}\) הוא מהצורה \(\left(\alpha_{1}\wedge\dots\wedge\alpha_{n}\right)\) כאשר ה-\(\alpha\) הם ליטרלים (כאן קריטי שהם יהיו ליטרלים ולא "סתם" פסוקים אטומיים – בלי היכולת להשתמש בשלילה זה לא עובד). עכשיו, לא קשה לראות ש-\(\exists x\left(\bigvee C_{i}\right)\) שקול ל-\(\bigvee\exists xC_{i}\), וכל \(\exists xC_{i}\) הוא מהצורה \(\exists x\left(\alpha_{1}\wedge\dots\wedge\alpha_{n}\right)\) שעליה הנחנו שאנחנו יודעים למצוא נוסחה שקולה חסרת כמתים, כך שזה מסיים את ההוכחה. נקודה שיש לתת עליה את הדעת היא שפסוק ה-DNF ששקול ל-\(\alpha^{\prime}\) עשוי להיות גדול לאין שיעור יותר מ-\(\alpha^{\prime}\), וזה בעייתי מאוד למי שמתעניינים בסיבוכיות של הליך חיסול הכמתים (כי יש לזה השפעה ישירה על השאלה עד כמה נוכל להשתמש בחיסול כמתים בפועל) אבל אני לא אומר על זה כמעט כלום בינתיים.

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

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

\(\forall x\forall y\forall z\left(x<y\wedge y<z\to x<z\right)\) (טרנזיטיביות היחס \(<\))
\(\forall x\neg\left(x<x\right)\) (אי-רפלקסיביות היחס).
\(\forall x\forall y\left(x=y\vee x<y\vee y<x\right)\) (לינאריות היחס – אפשר להשוות כל שני איברים).
\(\forall x\forall y\left(x<y\to\exists z\left(x<z\wedge z<y\right)\right)\) (צפיפות היחס – אם \(x<y\) אז יש ביניהם איבר).
\(\forall x\exists y\exists z\left(y<x\wedge x<z\right)\) (אין נקודות קצה: לכל \(x\) קיים איבר גדול ממנו ואיבר קטן ממנו).

אילו מודלים אנחנו מכירים לתורה הזו? ובכן, יחס הסדר על המספרים הטבעיים הוא בוודאי לא טוב כי 0 היא נקודת קצה; גם על השלמים הוא לא טוב כי הוא לא צפוף (אין כלום בין 0 ו-1, למשל). דוגמה טובה אחת למודל של התורה הזו היא המספרים הרציונליים \(\mathbb{Q}\) עם יחס הסדר הרגיל, ודוגמה טובה אחרת היא המספרים הממשיים \(\mathbb{R}\) עם יחס הסדר הרגיל (לעומת זאת המרוכבים \(\mathbb{C}\) אינם דוגמה טובה כי אין עליהם יחס סדר לינארי טבעי).

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

אז מה אנחנו רוצים לעשות? לקחת נוסחה מהצורה \(\exists x\left(\alpha_{1}\wedge\dots\wedge\alpha_{n}\right)\) כאשר כל \(\alpha\) הוא ליטרל, ולהמיר אותה למשהו שקול מודולו \(T\) ללא כמתים. ראשית כל, מהו פסוק אטומי בשפה של התורה \(T\)? יש לנו רק שני סימני יחס ואין בכלל סימני קבועים או פונקציות, אז פסוק אטומי חייב להיות מאוד פשוט: או \(x<y\) או \(x=y\), עבור שני משתנים \(x,y\) כלשהם. לכן כל \(\alpha\) הוא מאחת מארבע צורות אפשריות: \(x<y\) או \(x=y\) או \(\neg\left(x<y\right)\) או \(\neg\left(x=y\right)\).

נתחיל מכך שאפשר להיפטר מהשלילות. שימו לב ש-\(\neg\left(x<y\right)\) שקול מודולו \(T\) ל-\(\left(x=y\vee y<x\right)\). כאן ה"מודולו \(T\)" קריטי, כי השקילות הזו נובעת מאקסיומה 3 של \(T\) ובלעדיה היא פשוט לא נכונה. בדומה, \(\neg\left(x=y\right)\) שקול מודולו \(T\) ל-\(\left(x<y\vee y<x\right)\), גם כן מאקסיומה 3. שימו לב שכאן כבר השתמשנו באופן חזק בפרטים הספציפיים הן של השפה שלנו, והן של התורה \(T\).

הבעיה היא שאמנם נפטרנו מהשלילות, אבל במחיר של החלפת ה-\(\alpha\)-ות שלנו, שהיו נוסחאות אטומיות או שלילות שלהן, בנוסחאות שכוללות \(\vee\)-ים. פורמלית, קיבלנו CNF שהוא מונוטוני, כלומר אין בו ליטרלים שליליים (השם "מונוטוני" מגיע מכך שאם ניקח השמה מסויימת לפסוק ונחליף בה 0 ל-1, הערך של הפסוק יכול רק להשתנות מ-0 ל-1 ולא ההפך). מה שנחמד ב-CNF-ים כאלו הוא שניתן להמיר אותם ב-DNF-ים מונוטוניים (איך? ובכן, לכל השמה שמספקת את הפסוק בונים פסוקית DNF מהצורה \(\left(x_{1}\wedge\dots\wedge x_{n}\right)\) כאשר \(x_{1},\dots,x_{n}\) הם בדיוק המשתנים שמקבלים 1 בהשמה המספקת – בדקו שזה עובד!). לכן נקבל בסופו של דבר \(\bigvee\) של נוסחאות מהצורה \(\exists x\left(\alpha_{1}\wedge\dots\wedge\alpha_{n}\right)\) כאשר הפעם מובטח לנו שכל הליטרלים \(\alpha\) הם ללא שלילה, כלומר או מהצורה \(x<y\) או מהצורה \(x=y\). כל שנותר לעשות הוא לחסל את הכמת בנוסחאות כאלו.

עכשיו, אם \(\alpha_{1}\) שפשוט לא מכילה את המשתנה \(x\), אז הנוסחה \(\exists x\left(\alpha_{1}\wedge\dots\wedge\alpha_{n}\right)\) שקולה לנוסחה \(\exists x\left(\alpha_{2}\wedge\dots\wedge\alpha_{n}\right)\wedge\alpha_{1}\), ובאופן דומה אפשר יהיה להוציא מהסוגריים כל \(\alpha\) שלא מכילה את \(x\). בואו נעבור לדבר על \(\alpha\)-ות שכן כוללות את \(x\). ראשית בואו נטפל בכאלו שהן שוויון. אם \(\alpha\) כלשהי היא מהצורה \(x=x\) אז היא תמיד נכונה, בלי תלות ב-\(x\), ואפשר פשוט להסיר אותה (אם כל הנוסחה "נעלמת" בגלל הסרות כאלו אפשר להחליף אותה בנוסחה \(z=z\) עבור משתנה \(z\) כלשהו שלא יהיה מכומת). מה עוד אפשרי? \(x=y\) עבור משתנה \(y\) כלשהו שאיננו \(x\), כלומר איננו מכומת. זה מקרה משמח במיוחד, כי פירוש הדבר הוא שאפשר למחוק את \(x\) מכל ה-\(\alpha\)-ות ולהחליף אותו ב-\(y\) וחסל.

הנה דוגמה: נניח שיש לנו את הנוסחה \(\exists x\left(\left(x=y\right)\wedge\left(x<z\right)\wedge\left(z<w\right)\right)\); אפשר להחליף אותה בנוסחה \(\left(y=y\right)\wedge\left(y<z\right)\wedge\left(z<w\right)\) ולקבל משהו חסר כמתים ששקול לנוסחה המקורית, ואז סיימנו. לכן נשאר רק לטפל במקרים של \(\alpha\)-ות שהן יחס סדר (התעלול הזה, של "אם המשתנה המכומת שווה למשתנה לא מכומת אז הגיע חזון אחרית הימים" הוא כן משהו סטנדרטי שחוזר על עצמו גם בחיסולי כמתים אחרים).

אז סיימנו עם ליטרלים של \(=\), ונשאר לטפל באלו של \(<\), כלומר ליטרלים מהצורה \(x<y\) או \(z<x\), או \(x<x\), אבל מכיוון שהליטרל האחרון אף פעם לא מסתפק במודל \(T\) (בגלל אקסיומה 2), אם הוא מופיע אפשר להחליף את כל הנוסחה פשוט ב-\(z<z\) (שהוא תמיד False) וחסל. אם כן, אפשר לפצל את הליטרלים שלנו לשתי קבוצות – אלו של "משהו קטן מ-\(x\)" ואלו של "משהו גדול מ-\(x\)". כלומר, הנוסחה שלנו היא \(\exists x\left(\bigwedge_{i}\left(z_{i}<x\right)\wedge\bigwedge_{j}\left(x<y_{j}\right)\right)\). עצרו לשניה וחשבו איך אפשר לחסל את הכמת בנוסחה הזו. זה כבר קל מספיק כדי שאפשר יהיה לראות את זה בעיניים.

התשובה היא זו:

\(\bigwedge_{i,j}\left(z_{i}<y_{j}\right)\). כלומר, לכל זוג של משתנה \(z_{i}\) ומשתנה \(y_{j}\) שהופיעו בנוסחה המקורית, אנו כותבים את אי השוויון \(z_{i}<y_{j}\). למה הנוסחה הזו שקולה לנוסחה המקורית? או, כאן אנחנו משתמשים באופן חזק בתכונות של הסדר. כיוון אחד הוא טריוויאלי: אם \(\exists x\left(\bigwedge_{i}\left(z_{i}<x\right)\wedge\bigwedge_{j}\left(x<y_{j}\right)\right)\) הסתפקה, ברור שגם \(\bigwedge_{i,j}\left(z_{i}<y_{j}\right)\) תסתפקת בגלל טרנזיטיביות יחס הסדר (אקסיומה 1), אבל בכיוון השני הייתה עשויה להיות בעיה, בתיאוריה, אם ה-\(z_{i}\) הגדול ביותר היה "צמוד" ל-\(y_{j}\) הקטן ביותר. למשל, אם המודל שלנו היה הטבעיים, \(z_{i}=5\) ו-\(y_{j}=6\). אלא שהמודל של הטבעיים הוא בלתי אפשרי שכן הסדר הוא צפוף (אקסיומה 4), ולכן תמיד אפשר יהיה למצוא \(x\) בין ה-\(z_{i}\) הגדול ביותר וה-\(y_{j}\) הקטן ביותר.

רגע, רגע, רגע! איפה השתמשנו באקסיומה 5, שאומרות שאין נקודות קצה? היא הכרחית לגמרי, אבל באופן קצת עקיף ומחוכם. נניח שהנוסחה שאנחנו רוצים לחסל בה את הכמת היא פשוטה: \(\exists x\left(x<y\right)\), כלומר אין לנו כאן ליטרלים משני הסוגים (גם \(x<y\) וגם \(z<x\)). במה אנחנו אמורים להחליף אותה? ובכן, ב-\(\bigwedge\) "ריק", שהוא פשוט True (אז אפשר לשים את הנוסחה \(z=z\)). אבל זה נכון רק אם \(\exists x\left(x<y\right)\) היא אכן True; וזה כך רק אם אין בסדר שלנו נקודות קצה, כי אם \(y\) היא נקודת הקצה השמאלית – האיבר הקטן ביותר בסדר – אז \(x\) שמקיים \(x<y\) לא קיים. אם כן, כל חמש האקסיומות נחוצות לנו כאן. זה לא מוכיח, כמובן, שאי אפשר לקבל חיסול כמתים אם אני מסיר את אחת מהאקסיומות; רק ששיטת ההוכחה שבה השתמשתי כאן לא תעבוד.

עכשיו, בואו נקטוף את הפירות. יש שתי מסקנות מיידיות שנובעות מכך שיש חיסול כמתים עבור \(T\): האחד הוא ש-\(T\) היא שלמה, והשני הוא ש-\(T\) היא כריעה. נתחיל משלמות. שלמות פירושה שכל פסוק \(\varphi\) מקיים ש-\(T\models\varphi\) או ש-\(T\models\neg\varphi\). עכשיו, אם יש לנו פסוק \(\varphi\) (כלומר, אין בו משתנים חופשיים), אז אחרי חיסול כמתים נקבל ממנו נוסחה \(\psi\) בלי כמתים, ושהמופעים היחידים של משתנים בה הם מהצורה \(z=z\) או \(z<z\) (שהם פשוט דרך עקומה לציין את הנוסחאות הקבועות True ו-False). כלומר, ערך האמת של \(\psi\) בכלל לא תלוי במודל, ולכן \(T\models\psi\) או \(T\models\neg\psi\) (או שכל המודלים של \(T\) מספקים את \(\psi\), או שכולם מספקים את \(\neg\psi\)), ומכיוון ש-\(\psi\) שקול ל-\(\varphi\) מודולו \(T\) קיבלנו את מה שרצינו ולכן \(T\) שלמה. זה די נחמד לראות תורה שלמה שהיא גם לא טריוויאלית לחלוטין; בפעם הבאה שמישהו יגיד לכם שמשפטי אי השלמות של גדל מוכיחים שכל תורה מתמטית היא לא שלמה, תדעו מה לענות לו!

נעבור לכריעות. לומר ש-\(T\) כריעה פירושו שלכל פסוק \(\varphi\) ניתן לקבוע אלגוריתמית אם הוא יכיח מ-\(T\) או לא, מה ששקול לכך שהוא נובע לוגית מ-\(T\) (בגלל משפט השלמות של גדל). כאן האלגוריתם די מובן מאליו: נתון \(\varphi\)? בנו ממנו את הנוסחה \(\psi\) חסרת הכמתים השקולה ותבדקו אם היא True או False. סוף הסיפור. את הליך הבניה תיארתי קודם – הוא היה קונסטרוקטיבי למהדרין (אבל כלל כמה שלבים לא יעילים של מציאת DNF של דברים – זה חשוב כשנכנסים לשאלות של סיבוכיות, אבל אני לא עושה את זה הפעם).

מה צפוי לנו בהמשך? ובכן, עוד חיסולי כמתים, אבל לתורות חדשות ומרגשות!

לוגיקה מסדר ראשון – כמה תוצאות של משפט השלמות

פורסם בתאריך 21 במרץ 2013 על ידי gadial

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

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

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

בואו נדבר על אקסיומות פיאנו. לא יהיה לי צורך בכך ולכן אני לא באמת אציג אותן כאן במפורש – זה ראוי לפוסט נפרד – אבל אסביר בקצרה מהן. אקסיומות פיאנו הן נסיון למדל את המספרים הטבעיים – כלומר, לתת תורה מסדר ראשון (אוסף של אקסיומות) כך שהמספרים הטבעיים הם מודל שלהם. המילון של אקסיומות פיאנו כולל את סימן הקבוע \(0\) ואת סימן הפונקציה \(S\), שבפרשנות הסטנדרטית של האקסיומות (כלומר, זו שנמצאת לנו בראש כשאנו מגדירים את האקסיומות) תתפרש להיות פונקציית העוקב, כלומר \(S\left(n\right)=n+1\). כמו כן יש לנו את סימן היחס \(<\) שבפרשנות הסטנדרטית יתפרש להיות יחס הסדר הרגיל. יש גם סימני חיבור וכפל אבל לא נזדקק להם אז לא אציג אותם. גם לא אציג את האקסיומות עצמן במפורש – אשמור את זה לפוסט ייעודי עליהן.

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

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

מה שאני רוצה לעשות עכשיו הוא להוכיח שיש לאקסיומות פיאנו מודל לא סטנדרטי שכזה, ואעשה את זה באמצעות משפט הקומפקטיות. ספציפית, אני רוצה להוסיף מודל שבו יהיה "מספר" שגדול מכל מספר טבעי. לצורך כך, שימו לב קודם כל לכך שאני יכול לייצג כל מספר טבעי באמצעות שם עצם: הקבוע \(0\) מייצג את המספר אפס, שם העצם \(S\left(0\right)\) מייצג את 1, \(S\left(S\left(0\right)\right)\) מייצג את 2, וכן הלאה. במקום להסתרבל ולכתוב \(S^{n}\left(0\right)\) פשוט אכתוב \(n\) כדי לייצג את שם העצם עבור המספר הטבעי \(n\).

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

כאן משפט הקומפקטיות נחלץ לעזרתנו. כדי להוכיח שלמערכת המורחבת יש מודל, מספיק להראות שלכל תת קבוצה סופית שלה יש מודל. תת קבוצה סופית שכזו כוללת פסוקים אלו ואחרים מתוך אקסיומות פיאנו שלא מעניינים אותנו, ובנוסף לכך היא כוללת מספר סופי של פסוקים מהצורה \(c>n\). בואו נסמן ב-\(N\) את הערך המקסימלי של \(n\) שמופיע באחד מהפסוקים הללו; עכשיו אני יכול לתת מודל לתת-הקבוצה הסופית. המודל הזה יהיה פשוט המספרים הטבעיים, \(\mathbb{N}\), עם הפרשנות הרגילה לסימן הקבוע 0 ולסימני הפונקציות והיחסים השונים; הדבר היחיד שאני צריך לומר במפורש הוא איך יפורש סימן הקבוע \(c\); אני פשוט אתאים לו את המספר הטבעי \(N+1\). מכיוון שהמספר הזה גדול מכל \(n\) שמקיים \(n\le N\), הרי שכל פסוק מהצורה \(c>n\) ששייך לתת-הקבוצה הסופית של הפסוקים שלנו אכן מתקיים במודל שהצעתי. קיבלתי שלכל תת-קבוצה סופית של האקסיומות קיים מודל, ולכן קיים מודל לכולן (לא שברור למישהו איך הוא נראה…). סוף הסיפור.

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

בואו ונעשה תעלול דומה, אבל באופן קצת יותר חיובי, עבור המספרים הממשיים. בואו ניקח מילון פסיכי – לכל מספר ממשי \(r\in\mathbb{R}\) יהיה בו סימן קבוע \(c_{r}\), ולכל יחס אפשרי על הממשיים יהיה בו סימן עבור היחס הזה. בנוסף בואו ניקח בתור אקסיומות את כל הפסוקים מעל המילון הזה שנכונים בממשיים. במובן מסויים קיבלנו תורה ש"מתארת באופן מושלם" את הממשיים. אבל האם היא חומקת ממשפט הקומפקטיות? שוב, לא; נוסיף לה סימן קבוע חדש \(c\) ואת הפסוקים \(c_{r}<c\) לכל \(r\in\mathbb{R}\), ומשפט הקומפקטיות שוב יראה שיש לתורה הזו מודל שבו יש מספר שגדול מכל מספר ממשי.

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

הרעיון הזה הוא השלב הראשון בדרך אל מה שנקרא אנליזה לא סטנדרטית – תחום שבו בונים את החדו"א מחדש בעזרת אינפיניטסימלים שכאלה (הנה הגדרה אלטרנטיבית לגבול: \(\lim_{x\to x_{0}}f\left(x\right)=L\) אם כאשר \(\left|x-x_{0}\right|\) הוא אינפיניטסימלי, כך גם \(\left|f\left(x\right)-L\right|\)), אבל כשעושים את זה ברצינות צריך לגשת לנושא בצורה קונסטרוקטיבית יותר ואני לא הולך לעשות את זה כרגע. עצם העובדה שמשפט הקומפקטיות הופך את הוכחת ההיתכנות של אנליזה לא סטנדרטית לטריוויאלית זו תוצאה מספיק מלהיבה עבורי לפוסט הזה.

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

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

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

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

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

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

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

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

פורסם בתאריך 26 בפברואר 2013 על ידי gadial

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

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

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

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

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

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

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

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

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

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

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

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

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

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

פורסם בתאריך 25 בפברואר 2013 על ידי gadial

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

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

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

אם כן, מה עושים? למרבה המזל, יש לנו תבנית אקסיומה שנבחרה בדיוק כדי להתמודד עם הסיטואציה הזו – תבנית אקסיומה מס' 5, \(\forall x\left(\varphi\to\psi\right)\to\left(\varphi\to\forall x\psi\right)\). הדרישה של תבנית האקסיומה הזו היא ש-\(x\) לא יהיה משתנה חופשי ב-\(\varphi\). במקרה שלנו \(\varphi\) הוא \(\alpha\), והרי \(\beta\) מתקבל על ידי הוכחה מ-\(\Phi\cup\left\{ \alpha\right\} \) ודרשתי במפורש שאם GEN יופעל, אז זה יהיה רק עם משתנה שאינו מופיע חופשי ב-\(\Phi\cup\left\{ \alpha\right\} \), ומכאן ש-\(x\) אינו חופשי ב-\(\alpha\). לכן אפשר לכתוב את ההוכחה הפורמלית הבאה:

\(\alpha\to\gamma\) (הנחה).
\(\forall x\left(\alpha\to\gamma\right)\) (GEN על 1 עם משתנה שאינו מופיע חופשי ב-\(\Phi\))
\(\forall x\left(\alpha\to\gamma\right)\to\left(\alpha\to\forall x\gamma\right)\) (תבנית אקסיומה 5).
\(\alpha\to\forall x\gamma\) (MP על 2,3).

וקיבלנו בדיוק את \(\alpha\to\beta\) כפי שרצינו. זה מסיים את ההעברה של המשפטים מתחשיב הפסוקים ללוגיקה מסדר ראשון ומאפשר לנו להתמקד בעיקר.

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

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

מה שנרצה לעשות הוא להרחיב את אוסף הקבועים של \(\tau\) ואת \(\Phi\) כך שהם יקיימו את התכונה הבאה: ש-\(\Phi\) המורחבת תוכל להוכיח שלכל נוסחה \(\varphi\left(x\right)\) עם משתנה חופשי יחיד \(x\), אם \(\exists x\varphi\left(x\right)\) מתקיים אז קיים קבוע ש"מוכיח" את זה, כלומר יש קבוע \(c\) כך ש-\(\varphi\left(c\right)\) מתקיים. פורמלית אנו אומרים שקבוצת סימני קבועים \(C\) היא קבוצת עדים עבור \(\Phi\) אם לכל נוסחה \(\varphi\left(x\right)\) עם משתנה חופשי יחיד קיים \(c\in C\) כך שמתקיים

\(\Phi\vdash\exists x\varphi\left(x\right)\to\varphi\left(c\right)\)

כאן \(\varphi\left(c\right)\) פירושו מה שמקבלים כאשר מציבים ב-\(\varphi\) את הקבוע \(c\) במקום \(x\).

אז כמו בתחשיב הפסוקים, יש לנו שני שלבים: שלב ההרחבה של \(\Phi\) ו-\(\tau\), ושלב ההוכחה שלתורה המורחבת יש מודל. מכיוון שמודל לתורה המורחבת מעל המילון המורחב הוא עדיין מודל גם לתורה המקורית מעל המילון המקורי, זה יסיים את ההוכחה.

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

\(\Phi\) עקבית מקסימלית, במובן זה שהוספת כל פסוק ל-\(\Phi\) יהפוך את \(\Phi\) ללא-עקבית.
קיימת קבוצת עדים \(C\) עבור \(\Phi\), כלומר לכל נוסחה \(\varphi\left(x\right)\) עם משתנה חופשי יחיד \(x\) קיים קבוע \(c\in C\) כך ש-\(\Phi\vdash\exists x\varphi\left(x\right)\to\varphi\left(c\right)\).

בואו נבנה ל-\(\Phi\) מודל \(\mathcal{M}\). מודל כולל עולם שהוא קבוצה של איברים, ופרשנויות לסימני היחס, הפונקציות והקבועים של \(\tau\). הרעיון האינטואיטיבי הוא לעשות את הדבר הבא: להגדיר את העולם להיות שווה לקבוצת הקבועים של \(\tau\), כלומר לקחת את האובייקט הסינטקטי של סימני קבועים, ולהגדיר את המודל באמצעותו. אחר כך, בהינתן סימן יחס \(R\left(x,y\right)\) (נניח לצורך הדוגמה שהוא דו-מקומי) להגדיר יחס \(R^{\mathcal{M}}\left(x,y\right)\) במודל על ידי כך שלכל שני איברים \(c,d\) של העולם, \(\left(c,d\right)\in R^{\mathcal{M}}\) אם ורק אם הפסוק \(R\left(c,d\right)\) יכיח מתוך \(\Phi\). זה הרעיון, והוא פשוט ומבריק ויפהפה. כמובן שהפרטים הטכניים קצת מסתבכים עכשיו.

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

אז נניח שאנחנו עובדים בלוגיקה עם סימן השוויון. הנה הבעיה – הביטו לרגע בפסוק \(c=d\) כאשר \(c,d\) הם שני איברים של \(C\). נניח שהוא יכיח מתוך \(\Phi\) (וזה בהחלט יכול לקרות). פירוש הדבר הוא שאסור לנו להגדיר את \(c,d\) בתור איברים שונים בעולם של \(\mathcal{M}\), כי אז הפסוק \(c=d\) לא יהיה ספיק במודל הזה (ומכיוון שמערכת ההוכחה שלנו נאותה, ינבע מכך ש-\(\mathcal{M}\) אינו מודל של \(\Phi\)). הבעיה הזו מכריחה אותנו להגדיר את העולם של \(\mathcal{M}\) באופן קצת יותר מחוכם. מה שנעשה הוא להגדיר יחס שקילות על אברי \(C\), כך ש-\(c\equiv d\) אם ורק אם \(\Phi\vdash c=d\). כלומר, אנחנו אומרים שכל הקבועים של \(C\) ש-\(\Phi\) "מוכיחה שהם שווים" יהיו שקולים האחד לשני.

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

\(x=x\)
\(x=y\to t=s\) כאשר \(s\) מתקבל מ-\(t\) על ידי החלפת מופע אחד או יותר של \(x\) ב-\(y\).
\(x=y\to\left[\varphi\to\psi\right]\) כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי החלפת מופע אחד או יותר של \(x\) ב-\(y\).

בואו נתחיל. ראשית, אם \(c\in C\) כלשהו צריך להראות ש-\(\Phi\vdash c=c\). הנה הוכחה פורמלית:

\(x=x\) (אקסיומת שוויון מס' 1)
\(x=x\to c=c\) (אקסיומת שוויון מס' 2 עם \(t=s=c\))
\(c=c\) (MP על 1,2).

עכשיו, אם \(c,d\in C\) הם איברים כלשהם כך ש-\(\Phi\vdash c=d\) צריך להוכיח שגם \(\Phi\vdash d=c\):

\(x=y\to\left(x=x\to y=x\right)\) (אקסיומת שוויון מס' 3 עם \(\varphi=\left(x=x\right)\) ו-\(\psi=\left(y=x\right)\)).
\(\forall x\forall y\left(x=y\right)\to\left(x=x\to y=x\right)\) (Gen על 1).
\(\left[\forall x\forall y\left(x=y\right)\to\left(x=x\to y=x\right)\right]\to\left[\left(c=d\right)\to\left(c=c\to d=c\right)\right]\) (תבנית אקסיומה 4)
\(c=d\to\left(c=c\to d=c\right)\) (MP על 2,3).
\(c=d\) (יכיח מ-\(\Phi\)).
\(c=c\to d=c\) (MP על 4,5).
\(c=c\) (יכיח מ-\(\Phi\)).
\(d=c\) (MP על 6,7).

זה היה מבעית למדי, מה שמעלה את החשש שהוכחת טרנזיטיביות תהיה גרועה עוד יותר. נניח ש-\(c,d,e\in C\) מקיימים \(\Phi\vdash c=d\) וגם \(\Phi\vdash d=e\), אז צריך להוכיח ש-\(\Phi\vdash c=e\). כפי שאולי הבנתם מההוכחה הקודמת, מספיק להוכיח ש-\(x=y\to\left(y=z\to x=z\right)\) כדי לסיים, אבל זו הרי בדיוק אקסיומת שוויון מס' 3 עם \(\varphi=\left(x=z\right)\) ו-\(\psi=\left(y=z\right)\), כך שאחסוך מכם את המשך ההוכחה המפלצתית. זה מוכיח לנו שהיחס שהגדרתי לעיל הוא אכן יחס שקילות, ולכן אפשר לדבר על מחלקות השקילות שלו. כזכור, אם \(c\in C\) הוא איבר כלשהו, אז מסמנים \(\left[c\right]=\left\{ d\in C\ |\ c\equiv d\right\} \). הקבוצה \(\left[c\right]\) נקראת מחלקת השקילות של \(c\) ולא קשה לראות ש-\(C\) מתפרקת לאיחוד זר של מחלקות שקילות של איברים בה.

כעת אפשר להתחיל את הגדרת המודל \(\mathcal{M}\). ראשית נגדיר את העולם שלו: \(D^{\mathcal{M}}=\left\{ \left[c\right]\ |\ c\in C\right\} \). כעת נותר לתת פרשנויות לסימני היחס, הקבועים והפונקציות.

נתחיל מסימני היחס. יהא \(R\left(x_{1},\dots,x_{n}\right)\in\tau\) סימן יחס \(n\)-מקומי. נגדיר יחס \(R^{\mathcal{M}}\subseteq\left(D^{\mathcal{M}}\right)^{n}\) באופן הבא: לכל \(c_{1},\dots,c_{n}\in C\), \(\left(\left[c_{1}\right],\dots,\left[c_{n}\right]\right)\in R^{\mathcal{M}}\) אם ורק אם \(\Phi\vdash R\left(c_{1},\dots,c_{n}\right)\). זו הגדרה שנראית הגיונית, אבל כמו כל הגדרה שמערבת מחלקות שקילות, יש סכנה שהיא לא מוגדרת היטב. למה הכוונה? ייתכן שיש \(d_{1},\dots,d_{n}\in C\) כך ש-\(\left[c_{i}\right]=\left[d_{i}\right]\) (כלומר, מחלקת השקילות של \(c_{i}\) ו-\(d_{i}\) זהות, לכל \(1\le i\le n\)) ועם זאת \(\Phi\vdash R\left(c_{1},\dots,c_{n}\right)\) אבל \(\Phi\not\vdash R\left(d_{1},\dots,d_{n}\right)\), מה שאומר שההחלטה אם \(\left(\left[c_{1}\right],\dots,\left[c_{n}\right]\right)\in R^{\mathcal{M}}\) אינה תלויה במחלקות השקילות בלבד אלא ממש בנציגים שאנחנו בוחרים להן, ואסור לנו לעשות את זה – אנחנו חייבים לקבוע באופן חד משמעי עבור כל מחלקת שקילות מה יקרה איתה.

במקרה שלנו אין בעיה אמיתית שכזו. נניח ש-\(\Phi\vdash R\left(c_{1},\dots,c_{n}\right)\) וכמו כן ש-\(c_{1}\equiv d_{1}\), כלומר \(\Phi\vdash c_{1}=d_{1}\). אז מהאקסיומה \(x=y\to R\left(x,c_{2},\dots,c_{n}\right)=R\left(y,c_{2},\dots,c_{n}\right)\) אפשר לקבל חיש קל ש-\(\Phi\vdash R\left(d_{1},\dots,c_{n}\right)\) וכך להחליף בהדרגתיות את כל ה-\(c\)-ים ב-\(d\)-ים. עם זאת, חשוב היה לי להדגיש שזו נקודה שיש לשים לב אליה במהלך ההגדרה, וזה חלק מהסיבוך הנוסף שנגרם לנו מכך שהלוגיקה מסדר ראשון שלנו כוללת שוויון.

נעבור לקבועים. מפתה להגיד שלכל סימן קבוע \(c\in\tau\), נגדיר את הפרשנות שלו להיות \(c^{\mathcal{M}}=\left[c\right]\), וזה אכן הרעיון הכללי, אבל זה לא מספיק. הבעיה היא שאולי יש סימני קבועים שבכלל לא שייכים ל-\(C\). הפואנטה היא שגם במקרה זה, הפרשנות שנותנים לסימנים הללו חייבת להיות זהה לפרשנות שנותנים לפחות לאחד מהקבועים. למה? או, זו הזדמנות לראות את עניין ה"\(C\) היא קבוצת עדים" בפעולה.

נניח ש-\(d\in\tau\) הוא סימן קבוע כלשהו. אז אנחנו יודעים שהפסוק הבא הוא אמת לוגית: \(\exists x\left(x=d\right)\). עכשיו, \(\Phi\) היא קבוצה עקבית מקסימלית, מה שאומר (ואת זה אנחנו יודעים עוד מתחשיב הפסוקים) שלכל פסוק היא מוכיחה אותו או את שלילתו (אחרת היה אפשר להוסיף את הפסוק אליה ולקבל קבוצה גדולה יותר שעדיין עקבית). בגלל נאותות מערכת ההוכחה לא ייתכן שהיא תוכיח דבר שהוא סתירה לוגית, ולכן \(\Phi\vdash\exists x\left(x=d\right)\), ומכיוון ש-\(C\) היא קבוצת עדים, אז קיים \(c\in C\) כך ש-\(\Phi\vdash\exists x\left(x=d\right)\to\left(c=d\right)\), ומשילוב שני אלו נקבל ש-\(\Phi\vdash c=d\), וקיבלנו את מה שצריכה להיות הפרשנות של \(d\): \(d^{\mathcal{M}}=\left[c\right]\). גם כאן, התהליך היה מוגדר היטב: אם במקום \(c\) היינו מוצאים עד אחר, היינו מקבלים גם עבורו שהוא שווה ל-\(d\) ומהטרנזיטיביות שכבר ראינו של השוויון היינו מקבלים ש-\(\Phi\) מוכיחה את הפסוק שאומר ששני העדים שווים ולכן מחלקת השקילות שלהם שווה.

בפונקציות מטפלים באופן דומה. אם \(f\left(x_{1},\dots,x_{n}\right)\in\tau\) הוא סימן פונקציה \(n\) מקומי, ואנחנו צריכים להגדיר את \(f^{\mathcal{M}}\left(\left[c_{1}\right],\dots,\left[c_{n}\right]\right)\) אז נתבונן בפסוק \(\exists x\left(f\left(c_{1},\dots,c_{n}\right)=x\right)\), ניקח עד \(c\) עבורו ונגדיר \(f^{\mathcal{M}}\left(\left[c_{1}\right],\dots,\left[c_{n}\right]\right)=\left[c\right]\). גם פה צריך להוכיח שהכל מוגדר היטב אבל נדמה לי שכבר הבנתם את הרעיון. זה מסיים את הגדרת המודל \(\mathcal{M}\).

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

\(t_{1}=t_{2}\in\Phi\)

כאשר \(t_{1},t_{2}\) שמות עצם שאינם כוללים משתנים. אנחנו רוצים לחשב את הערך של שני שמות העצם הללו במודל ולראות שהוא זהה. לא ממש ברור איך לעשות את זה באופן ישיר, אבל קל לעשות את זה באופן עקיף: נסתכל על הפסוק \(\exists x\left(t_{1}=x\right)\) ונקבל, כרגיל, שיש \(c\in C\) כך ש-\(t_{1}=c\in\Phi\). בדומה נקבל ש-\(t_{2}=d\in\Phi\) עבור \(d\in C\) כלשהו, וכבר ראינו שאפשר להוכיח טרנזיטיביות, כלומר ש-\(c=d\in\Phi\) ולכן \(\left[c\right]=\left[d\right]\) וזהו הערך שהמודל מעניק לשני שמות העצם \(t_{1},t_{2}\) כך שבמקרה הזה טיפלנו.

כעת, הסוג הנוסף של פסוק בסיסי הוא פסוק מהצורה

\(R\left(t_{1},\dots,t_{n}\right)\in\Phi\)

כאשר \(R\) סימן יחס כלשהו ו-\(t_{1},\dots,t_{n}\) שמות עצם כלשהם שאינם כוללים משתנים. כמקודם, מוצאים \(c_{1},\dots,c_{n}\) כך ש-\(t_{i}=c_{i}\in\Phi\) ומכאן נוכל להוכיח ש-\(R\left(c_{1},\dots,c_{n}\right)\in\Phi\), מה שיגרור ש-\(\left(\left[c_{1}\right],\dots,\left[c_{n}\right]\right)\in R^{\mathcal{M}}\), מה שמסיים את המקרה הזה. כדאי לשים לב שבגלל ש-\(\Phi\) עקבית מקסימלית הרי שבשני המקרים הוכחנו יותר מאשר את מה שרצינו – הוכחנו גם שאם \(t_{1}=t_{2}\notin\Phi\) אז הערכים שהמודל מעניק לשמות העצם הללו שונים (אחרת אפשר היה להוסיף את \(t_{1}=t_{2}\) ל-\(\Phi\) מבלי לפגוע בעקביות) וכך גם עבור ה-\(R\)-ים. זה יועיל לנו בהמשך.

כעת אפשר להמשיך באינדוקציה על מבנה יתר הפסוקים הקיימים. לכל פסוק \(\varphi\) נרצה להראות ש-\(\mathcal{M}\models\varphi\) אם ורק אם \(\varphi\in\Phi\). נתחיל עם פסוקים מהצורה \(\neg\varphi\) כאשר \(\varphi\) הוא פסוק שעליו כבר הוכחנו את הטענה. אז מכיוון ש-\(\Phi\) עקבית מקסימלית, \(\neg\varphi\in\Phi\) אם ורק אם \(\varphi\notin\Phi\) אם ורק אם \(\mathcal{M}\not\models\varphi\), אם ורק אם \(\mathcal{M}\models\varphi\). זה היה קל.

עבור פסוק מהצורה \(\varphi\to\psi\) הנימוק ארוך יותר אבל לא באמת מסובך יותר. מכיוון שלמשהו כמו \(\varphi\to\psi\) יש רק השמה לא מספקת אחת, יהיה קל יותר להוכיח ש-\(\varphi\to\psi\notin\Phi\) אם ורק אם \(\mathcal{M}\models\varphi\) וגם \(\mathcal{M}\not\models\psi\). אם כן, \(\varphi\to\psi\notin\Phi\) אם ורק אם \(\neg\left(\varphi\to\psi\right)\in\Phi\). כעת, תעלול: הבה ונסתכל על הפסוקים \(\neg\left(\varphi\to\psi\right)\to\varphi\) ו-\(\neg\left(\varphi\to\psi\right)\to\neg\psi\). בדיקה ישירה תראה לנו שהם טאוטולוגיות, ולכן יכיחים מ-\(\Phi\) בלי הנחות כלל, רק על ידי אקסיומות 1-3 ו-MP. לכן נקבל ש-\(\Phi\vdash\varphi\) ו-\(\Phi\vdash\neg\psi\), מה שקורה אם ורק אם \(\mathcal{M}\models\varphi\) וגם \(\mathcal{M}\not\models\psi\), כנדרש.

מה נותרו? כמתים. יהיה יותר פשוט רעיונית לטפל ב-\(\exists\); הטיפול ב-\(\forall\) יהיה זהה מכיוון ש-\(\exists x\varphi\left(x\right)\) שקול לפסוק \(\neg\forall x\neg\varphi\left(x\right)\).

אם כן, נוכיח ש-\(\exists x\varphi\left(x\right)\in\Phi\) אם ורק אם \(\mathcal{M}\models\exists x\varphi\left(x\right)\). הבעיה היא ש-\(\varphi\left(x\right)\) הוא לא פסוק, כי \(x\) חופשי בו, ולכן אי אפשר להשתמש עליו בהנחת האינדוקציה והכל קורס, אלמלא היה לנו את התכונה המוזרה והכל כך לא ברורה במבט ראשון של "עד להוכחה". בגלל ש-\(C\) היא קבוצת עדים, אז קיים קבוע \(c\) כך ש-\(\Phi\vdash\exists x\varphi\left(x\right)\to\varphi\left(c\right)\), ולכן \(\varphi\left(c\right)\in\Phi\) ו-\(\varphi\left(c\right)\) הוא פסוק כך שהנחת האינדוקציה פועלת עליו, ו-\(\mathcal{M}\models\varphi\left(c\right)\), כלומר \(\mathcal{M}\models\exists x\varphi\left(x\right)\) (פורמלית: אם \(z\) היא השמה כלשהי, אז \(\mathcal{M}\models_{z\left[x\leftarrow\left[c\right]\right]}\varphi\left(x\right)\) ולכן \(\mathcal{M}\models_{z}\exists x\varphi\left(x\right)\)). הטיעון עובד באותו האופן בכיוון השני עד שמגיעים לכך ש-\(\varphi\left(c\right)\in\Phi\) ורוצים להסיק מכך ש-\(\exists x\varphi\left(x\right)\in\Phi\); את זה עושים באמצעות הפסוק \(\varphi\left(c\right)\to\exists x\varphi\left(x\right)\) שיכיח מ-\(\Phi\). אם אתם תוהים למה הוא יכיח, הנה הוכחה פורמלית:

\(\forall x\neg\varphi\left(x\right)\to\neg\varphi\left(c\right)\) (תבנית אקסיומה 4).
\(\left[\forall x\neg\varphi\left(x\right)\to\neg\varphi\left(c\right)\right]\to\left[\neg\neg\varphi\left(c\right)\to\neg\forall x\neg\varphi\left(x\right)\right]\) (תבנית אקסיומה 3).
\(\neg\neg\varphi\left(c\right)\to\neg\forall x\neg\varphi\left(x\right)\) (MP על 1,2).
\(\neg\neg\varphi\left(c\right)\to\exists x\varphi\left(x\right)\) (סתם שינוי סימון שיהיה קריא).
\(\left[\neg\neg\varphi\left(c\right)\to\exists x\varphi\left(x\right)\right]\to\left[\varphi\left(c\right)\to\exists x\varphi\left(x\right)\right]\) (טאוטולוגיה של תחשיב הפסוקים: \(\left(\neg\neg A\to B\right)\to\left(A\to B\right)\)).
\(\varphi\left(c\right)\to\exists x\varphi\left(x\right)\) (MP על 4,5).

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

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

מערכת הוכחה ללוגיקה מסדר ראשון

פורסם בתאריך 23 בפברואר 2013 על ידי gadial

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

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

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

\(\alpha\to\left(\beta\to\alpha\right)\)
\(\left[\alpha\to\left(\gamma\to\beta\right)\right]\to\left[\left(\alpha\to\gamma\right)\to\left(\alpha\to\beta\right)\right]\)
\(\left(\neg\alpha\to\neg\beta\right)\to\left(\beta\to\alpha\right)\)

אלו "תבניות" כי במקום \(\alpha,\beta,\gamma\) אפשר להציב פסוקים כלשהם. באותו האופן התבניות הללו יהיו שייכות גם למערכת ההוכחה של לוגיקה מסדר ראשון, כאשר במקום \(\alpha,\beta,\gamma\) מציבים נוסחאות כלשהן בלוגיקה מסדר ראשון. תבנית כזו היא בעלת התכונה הסמנטית שלא חשוב מה נציב בה – בכל מבנה ובכל השמה, הפסוק שמתקבל מההצבות הללו יהיה בעל ערך אמת, ואפילו אם הנוסחאות שמציבים הן מורכבות וכללות כמתים ופונקציות ואקשן. הסיבה פשוטה: אם מחשבים את ערך האמת של הפסוק שמתקבל מההשמות, בסופו של דבר נקבל שכל מה שהצבנו במקום \(\alpha\) מתורגם לאחד משניים: או \(\mbox{T}\) או \(\mbox{F}\), וכך גם עבור \(\beta,\gamma\), מה שאומר שלא משנה איזו נוסחה מורכבת אפשר להציב במקום \(\alpha,\beta,\gamma\), עדיין תחת מבנה והשמה נתונים הם מתנהגים כמו משתנים בתחשיב הפסוקים, ולכן תבנית אקסיומה שהייתה טאוטולוגיה בתחשיב הפסוקים נותרת כזו גם כעת.

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

\(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\)

זו נוסחה שמשתמשת בסימן יחס חד-מקומי \(R\), ויש בה משתנה קשור אחד \(x\) ומשתנה חופשי אחד \(y\). בכל מבנה \(\mathcal{M}\) ערך האמת של הרישא של הפסוק – \(\forall x\left(R\left(x\right)\right)\) – נקבע באופן יחיד, והוא יהיה \(\mbox{T}\) אם ורק אם \(R^{\mathcal{M}}=D^{\mathcal{M}}\), כלומר אם היחס \(R\) מתפרש ב-\(\mathcal{M}\) בתור "כל העולם". כעת, אם הערך של \(\forall x\left(R\left(x\right)\right)\) הוא \(\mbox{F}\) אז הנוסחה כולה היא תמיד בעל ערך אמת \(\mbox{T}\); ואילו אם ערך האמת שלו הוא \(\mbox{T}\) אז \(R^{\mathcal{M}}=D^{\mathcal{M}}\) ולכן לכל השמה אפשרית, לא משנה איזה ערך היא נותנת ל-\(y\), יתקיים ש-\(R\left(y\right)\) הוא \(\mbox{T}\) ולכן שוב הנוסחה כולה תהיה \(\mbox{T}\). במילים אחרות, הנוסחה \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\)היא בעלת ערך האמת \(\mbox{T}\) בכל מבנה ובכל השמה אפשריים. לנוסחה בעלת התכונה הזו אני קורא אמת לוגית, ובכוונה אני לא קורא לה "טאוטולוגיה" כמו בתחשיב הפסוקים. במילה "טאוטולוגיה" בלוגיקה מסדר ראשון אני משתמש כדי לתאר את מה שמתקבל מלקיחת טאוטולוגיה בתחשיב הפסוקים ואז הצבת נוסחאות בתור המשתנים, ואילו \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\) בבירור לא יכול להתקבל בצורה הזו. הדרך היחידה שבה הוא יכול להתקבל היא על ידי הצבה בפסוק \(X\to Y\), אבל הפסוק הזה כלל אינו טאוטולוגיה.

זה מראה לנו שהסיבות לכך ש-\(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\) היא אמת לוגית הן עמוקות יותר מאשר הסיבות לכך שנוסחה כמו \(\forall x\left(R\left(x\right)\right)\to\left(R\left(y\right)\to\forall x\left(R\left(x\right)\right)\right)\) היא אמת לוגית; השניה מתקבלת מהצבה בפסוק \(X\to\left(Y\to X\right)\) שהוא כן טאוטולוגיה של תחשיב הפסוקים, ולכן ערך האמת שלה נובע במובן מסויים רק מתכונות הקשרים (\(\to\) במקרה הזה), בעוד שערך האמת הלוגית של \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\) נובע גם מתכונות הכמתים (שימו לב: אם נחליף את \(\forall\) ב-\(\exists\) נקבל משהו שאינו אמת לוגית). אני מקווה שזה עוזר להבין למה מה שעשינו בתחשיב הפסוקים רחוק מלהיות מספיק גם בתחשיב היחסים.

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

\(\forall x\left(\exists y\left(x+y>c\right)\right)\to \left(\exists y\left(z+y>c\right)\right)\)

כאן המשתנים \(x,y\) הם קשורים ואילו \(z\) הוא המשתנה החופשי; \(c\) הוא סימן קבוע, \(+\)הוא סימן פונקציה ו-\(>\) הוא סימן יחס. לא קשה לראות שגם הנוסחה הזו היא אמת לוגית. מה הדמיון בינה ובין הנוסחה הקודמת שהצגתי? בשתיהן יש "לכל \(x\) משהו עבור \(x\) גורר משהו עבור \(y\)". שם ה"משהו" היה \(R\left(x\right)\) וכאן ה"משהו" הוא \(\exists y\left(x+y>c\right)\) . באופן כללי "משהו" כזה יכול להיות כל נוסחה, אפילו נוסחאות שבהן \(x\) בכלל לא מופיע. אז לכאורה הצורה של האקסיומה צריכה להיות \(\forall x\varphi\to\varphi\), אבל הצורה הזו לא כללית מספיק. היא מסוגלת ליצור משהו כמו \(\forall x\left(R\left(x\right)\right)\to R\left(x\right)\), אבל הוא לא מסוגלת ליצור משהו כמו \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\).

אם כן, אולי אפשר לומר שהצורה של האקסיומה תהיה \(\forall x\varphi\to\psi\), כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי שינוי השם של המשתנה \(x\). זה כבר יותר בכיוון, אבל הנה נוסחה שהיא אמת לוגית ולא יכולה להתקבל כך:

\(\forall x\left(x\ge0\right)\to\left(1\ge0\right)\)

כאן \(0,1\) הם סימני קבועים של השפה ו-\(\ge\) הוא סימן יחס. כאן כבר לא סתם שינינו את השם של \(x\) אלא ממש החלפנו אותו בקבוע. ואפשר היה לעשות גם משהו כזה:

\(\forall x\left(x\ge0\right)\to\left(\left(1+z\right)^{2}\ge0\right)\)

כאשר כאן העלאה בריבוע היא סימן פונקציה, וגם חיבור הוא סימן פונקציה. מה שקרה הוא שהחלפנו את \(x\) בשם עצם: \(\left(1+z\right)^{2}\). אם כן, אפשר לומר שהצורה של האקסיומה תהיה \(\forall x\varphi\to\psi\) כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי החלפת כל מופע של \(x\) בשם עצם ספציפי כלשהו \(t\). זה בהחלט בכיוון, אבל זה כבר כללי יותר מדי. אם נעשה את זה, אנחנו עלולים לקבל נוסחאות שאינן אמיתות לוגיות. הנה דוגמה. ניקח את \(\varphi\) להיות \(\exists y\left(y>x\right)\) ואת \(t\) להיות \(y\) ונקבל:

\(\forall x\left(\exists y\left(y>x\right)\right)\to\exists y\left(y>y\right)\)

וזה בבירור לא פסוק שהוא אמת לוגית, כי קחו בתור מודל את המספרים הטבעיים – לכל מספר טבעי \(x\) קיים מספר גדול ממנו \(y\), אבל אין אף מספר טבעי שגדול מעצמו. מה השתבש? הבעיה היא שאנחנו משתמשים ב-\(y\) בתפקיד כפול: בתוך \(\varphi\) הוא משתנה מכומת, בעוד ש-\(x\) הוא משתנה חופשי בתוך \(\varphi\). בכך שאנחנו מציבים את \(y\) במקום \(x\) אנחנו הופכים משהו שלפני שניה היה חופשי (ולכן לא מושפע מהכמת \(\exists y\)) למשהו קשור (שכן מושפע מהכמת הזה). זה סוג שינוי שאנחנו חייבים למנוע. זה מוביל אותנו להגדרה שהיא קצת קשה לעיכול אם לא רואים לה קודם מוטיבציה: שם עצם \(t\) הוא חופשי להצבה במקום \(x\) בפסוק \(\varphi\) אם \(t\) לא מכיל אף משתנה \(y\) כך שיש מופע חופשי של \(x\) ב-\(\varphi\) שנופל תחת כמת עבור \(y\). זו הגדרה מסובכת מבחינה מילולית, אבל העיקרון ברור – אנחנו לא רוצים להחליף את \(x\) במשהו, ואז לגלות שבתוך המשהו היה משתנה שפתאום הופך להיות מכומת.

עוד נקודה שצריך לשים לב אליה היא ש-\(\varphi\) עשוי להכיל גם מופעים לא חופשיים של \(x\), ובהם אסור להציב. זה מקרה קצה מוזר למדי אבל עדיין יש להתחשב בו. הנה דוגמה: ניקח בתור \(\varphi\) את \(\exists x\left(x>0\right)\) ובתור \(t\) את הקבוע \(0\), ונקבל:

\(\forall x\left(\exists x\left(x>0\right)\right)\to\left(\exists x\left(0>0\right)\right)\)

שהוא כמובן לא נכון. הבעיה כאן היא הפוכה ביחס לבעיה הקודמת: קודם הפכנו מישהו לא מכומת למכומת, ואילו כאן אנחנו משתמשים בהצבה לתוך \(x\) כדי "להימלט" מהכמת \(\exists x\). הפתרון הוא פשוט למדי: לא מציבים את \(t\) בתוך מופעים מכומתים של \(x\) ב-\(\varphi\) אלא רק במופעים החופשיים שלו.

עכשיו אפשר סוף סוף לנסח את תבנית האקסיומה במפורש. התבנית היא:

\(\forall x\varphi\to\psi\)

כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי הצבה בכל מופע חופשי של \(x\) ב-\(\varphi\) שם עצם \(t\) כלשהו שהוא חופשי להצבה במקום \(x\) ב-\(\varphi\).

צריך כמובן להוכיח שכל נוסחה כזו היא אכן אמת לוגית, מה שניתן לעשות באופן ישיר למדי הישר מהגדרות הסמנטיקה של לוגיקה מסדר ראשון ואוותר על כך כאן (ההוכחה דומה למה שעשיתי לעיל עבור \(\varphi=R\left(x\right)\)).

בואו נעבור להתבונן על נוסחה אחרת שעדיין אין לנו יכולת להוכיח במערכת שלנו:

\(\forall x\left(R\left(y\right)\to S\left(x\right)\right)\to\left(R\left(y\right)\to\forall xS\left(x\right)\right)\)

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

הפורמליזציה של תבנית האקסיומה הזו פשוטה:

\(\forall x\left(\varphi\to\psi\right)\to\left(\varphi\to\forall x\psi\right)\)

כאשר הדרישה היא ש-\(x\) איננו משתנה חופשי ב-\(\varphi\). קל לראות שהדרישה הזו הכרחית כדי שהתבנית תגדיר נוסחאות אמיתיות לוגיות; בואו נביט על \(\forall x\left(x>0\to x>0\right)\to\left(x>0\to\forall x\left(x>0\right)\right)\) שהוא בבירור לא אמת לוגית – אגף ימין שלו בבירור מתקיים אבל אגף שמאל אומר שאם \(x\) ספציפי הוא גדול מאפס אז נובע מכך שכל \(x\) הוא גדול מאפס וזה בוודאי לא נכון.

האם באמת היה צריך להוסיף את תבנית האקסיומה החדשה הזו? האם אי אפשר לקבל אותה מהדברים הקיימים? לא ממש. התבנית הקודמת שהצגתי יודעת להסיר \(\forall\); היא לא יודעת להזיז אותו. זה מרמז גם על מה שעדיין חסר לנו – דרך לייצר \(\forall\). לצורך כך אוסיף כלל היסק חדש שנקרא \(\mbox{Gen}\) (מלשון Generalization – הכללה). הכלל מקבל פסוק \(\varphi\) ומייצר ממנו את \(\forall x\varphi\) עבור משתנה כלשהו \(x\), וניתן להשתמש בו גם כאשר \(x\) כן מופיע חופשי ב-\(\alpha\). עם זאת, יש עליו סייג קטן: אם \(\Phi\) היא קבוצת ההנחות שבה אנחנו משתמשים בהוכחה שלנו, אסור להשתש ב-Gen עבור אף משתנה \(x\) שמופיע חופשי בהנחה כלשהי ב-\(\Phi\). אצלנו ממילא אנחנו הולכים לדבר רק על קבוצת הנחות שהן פסוקים, כלומר נוסחאות בלי משתנים חופשיים, כך שהסייג הזה לא יהיה רלוונטי לנו ונוכל להשתמש ב-Gen בחופשיות.

תחת הסייג הזה פשוט למדי להוכיח ש-Gen עובד: נניח ש-\(\Phi\models\varphi\), כלומר כל מבנה \(\mathcal{M}\) והשמה \(z\) מקיימים שאם \(\mathcal{M}\models_{z}\Phi\) אז \(\mathcal{M}\models_{z}\varphi\). כדי להראות ש-\(\mathcal{M}\models_{z}\forall x\varphi\) צריך להראות שמתקיים \(\mathcal{M}\models_{z\left[x\leftarrow a\right]}\varphi\) לכל \(a\in D^{\mathcal{M}}\). כעת, מכיוון ש-\(x\) לא מופיע חופשי באף הנחה ב-\(\Phi\) הרי ש-\(\mathcal{M}\models_{z\left[x\leftarrow a\right]}\Phi\) (השינוי של הערך ש-\(x\) מקבל בהשמה \(z\) לא משפיע על ערך האמת ש-\(z\) נתנה לפסוקי \(\Phi\)) ולכן \(\mathcal{M}\models_{z\left[x\leftarrow a\right]}\varphi\).

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

\(x=x\)

די ברור שאפשר להוסיף אותה כתבנית אקסיומה, אבל זה עדיין לא מספיק. צריך עוד תבנית אקסיומה שתגיד לנו שאם שני משתנים הם שווים בערכם, אז כל שני שמות עצם שזהים פרט לאותם משתנים גם כן שווים בערכם, וכל שתי נוסחאות שזהות פרט לאותם משתנים הן שקולות. פורמלית, אז אלו האקסיומות שקשורות לשוויון (\(x,y\) מייצגים משתנים, \(t,s\) מייצגים שמות עצם, \(\varphi,\psi\) מייצגים נוסחאות):

\(x=x\)
\(x=y\to t=s\) כאשר \(s\) מתקבל מ-\(t\) על ידי החלפת מופע אחד או יותר של \(x\) ב-\(y\).
\(x=y\to\left[\varphi\to\psi\right]\) כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי החלפת מופע אחד או יותר של \(x\) ב-\(y\).

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

פרדוקס בוחן הפתע

פורסם בתאריך 16 בדצמבר 2012 על ידי gadial

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

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

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

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

"אף פעם" הסכים השד מהשביעית.

"אף פעם!" הסכים קהל הסטודנטים באושר.

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

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

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

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

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

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

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

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

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

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

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

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

בגישה המתמטית שאני מציג כאן, המושג של "ידע" מזוהה עם "יכיחות". לכן אני צריך איזה שהוא סימון כדי לתאר "יכיח": אני אשתמש ב-\(\mbox{Pr}\left[\varphi\right]\) (מלשון "Provable") כדי לומר "הפסוק \(\varphi\) יכיח". בנוסף, אשתמש במשתנה \(D\) כדי לתאר את היום שבו בוחן הפתע מתקיים. עם הסימונים הללו, אפשר לנסות ולתאר את מה שגוסונובסקי אומר לתלמידים כך (קראו את זה בתור "המבחן יהיה באחד מהימים \(1,2,3,4,5\) וגם לכל יום \(n\), אם המבחן לא התקיים עד אליו, לא ניתן להוכיח מכך שהוא יתקיים ביום \(n\)"):

\(S\equiv\left(D\in\left\{ 1,2,3,4,5\right\} \right)\wedge\bigwedge_{n=1}^{5}\left(D\ge n\to\neg\mbox{Pr}\left[D\ge n\to D=n\right]\right)\)

ה-\(S\equiv\) בהתחלה אומר שזה השם שאני נותן לפסוק שמימין ל-\(\equiv\); זה יהיה חשוב בהמשך.

האם הפסוק הזה ממדל טוב את דבריו של גוסונובסקי? לא ממש. בואו ננסה לחשוב איך התלמידים יוכיחו בעזרתו ש-\(D\ne5\): הם יניחו בשלילה ש-\(D=5\) (ולכן בפרט \(D\ge5\)) ולכן כדי להגיע לסתירה די להם להראות ש-\(\mbox{Pr}\left[D\ge5\to D=5\right]\). הבעיה היא שאי אפשר להוכיח את הטענה הזו בלי ידע נוסף – במקרה הזה, ש-\(D\in\left\{ 1,2,3,4,5\right\} \).

"אבל רגע!" אולי אתם אומרים, "הרי הידע הזה הוא בדיוק מה שהיה בחלק השמאלי של הפסוק!". זה כמובן נכון, אבל הפסוק הזה הוא לא אחת מהאקסיומות שעליהן הסימון \(\mbox{Pr}\left[D\ge n\to D=n\right]\) מדבר כשהוא מדבר על קיום הוכחה אלא אם אנחנו בוחרים להניח את זה במובלע, ואנחנו לא. האקסיומות היחידות שאנחנו מניחים במובלע הן האקסיומות הרגילות של לוגיקה מסדר ראשון. אם אנחנו רוצים עוד אקסיומות, בואו נציין אותן במפורש: נסמן ב-\(\mbox{Pr}_{A}\left[\varphi\right]\) את הטענה "\(\varphi\) יכיח מ-\(A\)".

אם כן, מה שטבעי לעשות הוא להגדיר

\(A\equiv\left(D\in\left\{ 1,2,3,4,5\right\} \right)\)

ועכשיו להגדיר

\(S\equiv\left(D\in\left\{ 1,2,3,4,5\right\} \right)\wedge\bigwedge_{n=1}^{5}\left(D\ge n\to\neg\mbox{Pr}_{A}\left[D\ge n\to D=n\right]\right)\)

הניסוח הזה קולע לא רע למטרה. בואו נראה שהתלמידים מסוגלים להוכיח איתו ש-\(D\ne5\). כדי לעשות את זה, התלמידים יניחו בשלילה ש-\(D=5\), ואז יוכיחו שמתקיים \(\mbox{Pr}_{A}\left[D\ge5\to D=5\right]\) על ידי כך ש-\(A\) נותן לנו ש-\(D\le5\) ולכן אם \(D\ge5\) אז \(D=5\), שזו דרך אחרת לכתוב \(D\ge5\to D=5\).

רק שעכשיו התלמידים בברוך. השלב הבא הוא להוכיח ש-\(D\ne4\), ואז זה הם לא יכולים לעשות מתוך \(A\). בואו ניזכר שניה איך הטיעון אמור ללכת עכשיו: התלמידים יניחו בשלילה ש-\(D=4\). עכשיו הם רק צריכים להראות שמתקיים \(\mbox{Pr}_{A}\left[D\ge4\to D=4\right]\). ההוכחה תלך ככה: בגלל שאנחנו יודעים ש-\(D\le4\)… רגע, רגע, רגע! מה זה "אנחנו יודעים"? מי יודע? אם כל מה שההוכחה יכולה להשתמש בו הוא \(A\), אז ההוכחה לא יודעת ש-\(D\ne5\), ובלי הידע הזה לא ניתן להוכיח ש-\(D\le4\) וההוכחה הולכת לכל הרוחות.

כדי להסיק את \(D\ne5\) בתוך ההוכחה של \(D\ge4\to D=4\), ההוכחה הזו צריכה לקבל כאקסיומה בדיוק את הכלי שהיה לסטודנטים כשהם הוכיחו ש-\(D\ne5\), והכלי הזה הוא הנוסחה \(S\) עצמה. זה לב העניין. אנחנו רואים שהמעגליות הזו היא קריטית עבור הטיעון של התלמידים. במילים אחרות, הניסוח הנכון של \(S\) הוא זה:

\(S\equiv\left(D\in\left\{ 1,2,3,4,5\right\} \right)\wedge\bigwedge_{n=1}^{5}\left(D\ge n\to\neg\mbox{Pr}_{S}\left[D\ge n\to D=n\right]\right)\)

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

בניסוח הזה של הפרדוקס אפשר להוכיח פורמלית שניתן להוכיח מתוך \(S\) את זה ש-\(D\notin\left\{ 1,2,3,4,5\right\} \), ובמילים אחרות – ש-\(S\) סותר את עצמו. זה פותר במובן מסויים את הפרדוקס; כעת ברור מה הניסוח של הטענה של גוסונובסקי שממנו התלמידים מסוגלים להסיק את המסקנה שלהם, וגם די ברור שכשגוסונובסקי אומר "יהיה בוחן פתע", האינטואיציה הראשונה שלנו לא מבינה את דבריו בתור משהו מורכב כמו \(S\) ולכן אנחנו לא רואים כאן בעיה. גם כאן זו נקודה שאפשר לעצור בה, אבל אני רוצה להמשיך עוד קצת, למאמר חדש יחסית מ-2010 של רן רז ושירה קריצ'מן ממכון וייצמן שלוקח את הרעיון קצת יותר רחוק.

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

\(S\equiv\left(D\in\left\{ 1,2,3,4,5\right\} \right)\wedge\bigwedge_{n=1}^{5}\left[D\ge n\to\left(\neg\mbox{Pr}_{S}\left[D\ge n\to D=n\right]\vee\bigvee_{k\ne n}\mbox{Pr}_{S}\left[D\ge n\to D=k\right]\right)\right]\)

החלק הפנימי אומר הפעם "אם המבחן לא התקיים עד יום \(n\), אז או שאי אפשר להוכיח שהוא יתקיים ביום \(n\), או שיש \(k\ne n\) שגם עבורו אפשר להוכיח שהמבחן יתקיים ביום \(k\)".

כעת, נניח שהתלמידים רוצים להוכיח ש-\(D\ne5\). הם מניחים בשלילה ש-\(D=5\), וכמו קודם הם מוכיחים ש-\(\mbox{Pr}_{S}\left[D\ge5\to D=5\right]\). לרוע מזלם, הפעם זה לא מספיק כדי להסיק ש-\(D\ne5\); חייבים גם להוכיח שעבור \(1\le k\le4\) מתקיים \(\neg\mbox{Pr}_{S}\left[D\ge5\to D=4\right]\).

"רגע אחד!" אולי אתם אומרים. "אבל מה ההגיון בטענה כמו \(D\ge5\to D=4\)? הרי ברור שהיא לא נכונה!" זה כמובן נכון; אבל למה שזה יאמר שהתלמידים לא יהיו מסוגלים להוכיח את זה? הם יהיו מסוגלים להוכיח את זה, בתנאי שמערכת ההוכחה שלהם לא עקבית. זה מעלה את השאלה – מהי בכלל מערכת ההוכחה של התלמידים?

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

איך זה מתקשר לבעיה של התלמידים? שהם יכולים להוכיח ש-\(D\ne5\), מתוך ZF, רק אם הם ישללו את זה שאפשר להוכיח בה \(D\ge5\to D=4\), כלומר רק אם הם ישללו את זה ש-ZF יכולה להוכיח סתירה, כלומר רק אם הם יכולים להוכיח ש-ZF עקבית. אבל זה בדיוק מה שמשפט אי השלמות השני של גדל מראה שאי אפשר לעשות.

הטיעון הוא למעשה קצת יותר עדין מזה. אם התלמידים מניחים ש-ZF עקבית, כמו שכל מתמטיקאי עושה, אז מההנחה הזו ינבע שאי אפשר להוכיח את \(D\ge5\to D=4\) ולכן התלמידים יצליחו להוכיח ש-\(D\ne5\) (בהנחה ש-ZF עקבית; אבל אם ZF לא עקבית על אחת כמה וכמה אפשר להוכיח ש-\(D\ne5\)). הבעיה תהיה בצעד הבא: כדי להוכיח ש-\(D\ne4\) התלמידים צריכים להוכיח ש-\(\mbox{Pr}_{S}\left[D\ge4\to D=4\right]\), אבל זה לא נכון: אי אפשר להוכיח את \(D\ge4\to D=4\) רק מתוך \(S\) כי בשביל ההוכחה הזו צריך קודם כל להוכיח ש-\(D\ne5\) ובשביל זה צריך להניח ש-\(\mbox{ZF}\) עקבית. במילים אחרות, צריך להחליף את \(S\) ב-\(S\wedge\mbox{CON}\left(\mbox{ZF}\right)\). אבל אם נעשה את זה, נקבל מערכת חדשה, שגם את העקביות שלה אי אפשר להוכיח… אני מקווה שאתם מבינים את העיקרון.

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

הבעיה העשירית של הילברט – פונקציות דיופנטיות וחיות אחרות (רקורסיביות)

פורסם בתאריך 4 בספטמבר 2012 על ידי gadial

אנו ממשיכים בדרך שלנו אל ההוכחה שלא קיים אלגוריתם שפותר את הבעיה העשירית של הילברט. אני מניח שקראתם את פוסט המבוא ולכן קופץ ישר לעניינים הפעם. המושג המרכזי בפוסט הקודם היה קבוצה דיופנטית. זוהי קבוצה \(S=\left\{ \left(a_{1},\dots,a_{n}\right)\right\} \) של \(n\)-יות של מספרים טבעיים חיוביים, כך שקיים פולינום \(p\left(x_{1},\dots,x_{n},y_{1},\dots,y_{m}\right)\) בעל התכונה הבאה: למשוואה הדיופנטית \(q\left(y_{1},\dots,y_{m}\right)=0\), עבור \(q\left(y_{1},\dots,y_{m}\right)=p\left(a_{1},\dots,a_{n},y_{1},\dots,y_{m}\right)\) יש פתרון בשלמים חיוביים אם ורק אם \(\left(a_{1},\dots,a_{n}\right)\in S\). אפשר גם לעשות ההפך – להתחיל מפולינום \(p\left(x_{1},\dots,x_{n},y_{1},\dots,y_{m}\right)\) ולסמן קבוצה \(S_{p}\) שכוללת את כל ה-\(n\)-יות שכאשר מציבים אותם במקום ה-\(x\)-ים, מקבלים משוואה דיופנטית עם פתרון בשלמים חיוביים.

אם לא הבנתם כלום ממה שכתבתי כרגע, נסו לקרוא שוב את המבוא.

בפוסט הקודם ראינו שאפשר להגדיר יחסים מוכרים באופן הזה, למשל את יחס החלוקה (שהוא קבוצת הזוגות \(\left(a,b\right)\) כך ש-\(a|b\), כלומר \(a\) מחלק את \(b\), כלומר קיים \(c\) שלם כך ש-\(b=ac\)). בואו נראה לצורך החימום עוד דוגמה – היחס "קטן-שווה", הידוע גם כ-\(a\le b\). נגדיר אותו באופן הבא:

\(x\le y\iff\exists z\left(x+z-1=y\right)\)

רגע, מה? מה הולך כאן? מה אלו הסימונים הללו? אני עובר לשיטה שבה מרטין דיוויס משתמש במאמר שלו כי היא אלגנטית וקצרה יותר. כאן הפולינום שלי הוא \(p\left(x,y,z\right)=x+z-1-y\), והמשתנים שבהם צריך להציב ערכים הם \(x,y\) ואז לראות אם למשוואה הדיופנטית שנותרה לנו, שיש בה רק את המשתנה \(z\), יש פתרון. די ברור בסימון של דיוויס מי המשתנים ששייכים לקבוצה הראשונה (אלו שבאגף שמאל של החצים) ומי המשתנים שבקבוצה השניה (אלו שיש סימן \(\exists\) – "קיים" לפניהם) והיכן הפולינום עצמו (מה שבסוגריים, עד כדי העברת אגפים אם יש צורך). אז אני מקווה שאנחנו מיודדים עם הסימון הזה כעת וגם מבינים למה הפולינום שלעיל אכן מגדיר את \(x\le y\).

עכשיו, תרגיל – מה השתנה כאן?

\(x<y\iff\exists z\left(x+z=y\right)\)

ולמה?

עכשיו בואו נעבור למשהו קצת יותר מתוחכם. ראינו כבר שיש פולינום \(p_{1}\) שמגדיר את הקבוצה \(S_{p_{1}}=\left\{ \left(a,b\right)\ |\ a|b\right\} \). ראינו גם שיש פולינום \(p_{2}\) שמגדיר את הקבוצה \(S_{p_{2}}=\left\{ \left(a,b\right)\ |\ a\le b\right\} \). האם יש פולינום שמגדיר את הקבוצה \(S=\left\{ \left(a,b\right)\ |\ a\le b\wedge a|b\right\} \) (\(\wedge\) הוא הסימן של "וגם"; ו-\(\vee\) הוא הסימן של "או"), כלומר הקבוצה \(S_{p_{1}}\cap S_{p_{2}}\)? התשובה חיובית: הפולינום \(p_{1}^{2}+p_{2}^{2}\). למה? כי אחרי הצבת ערכים בו, נשאר עם משוואה דיופנטית שהדרך היחידה שלה להתאפס היא שגם \(p_{1}^{2}\) יתאפס וגם \(p_{2}^{2}\) יתאפס (כי אם אחד מהם לא מתאפס, אז אחרי העלאה בריבוע הוא חיובי ולכן הסכום יהיה גדול מאפס). את העניין הזה אפשר כמובן להכליל לחיתוך על מספר סופי כלשהו של נחתכים. המסקנה: מחלקת הקבוצות הדיופנטיות סגורה לחיתוכים סופיים. ומה עם איחודים סופיים? גם אותם אפשר לקבל. הקבוצה \(S_{p_{1}}\cup S_{p_{2}}\) מוגדרת על ידי הפולינום \(p_{1}p_{2}\) – הוכיחו זאת לעצמכם.

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

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

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

נתחיל מהכיוון הקל. נניח שיש לנו קבוצה \(S\) שמוגדרת על ידי \(p\left(y_{1},\dots,y_{n}\right)\) בדרך ה"חדשה" שתיארתי – \(S\) היא קבוצת הערכים החיוביים ש-\(p\) יכול להחזיר. אנחנו רוצים למצוא פולינום \(q\) כך ש-\(S=S_{q}\), כאשר \(S_{q}\) מוגדרת בשיטה הישנה (ערכים שאחרי שמציבים אותם ב-\(q\) מקבלים משוואה דיופנטית פתירה). מה נגדיר? פשוט מאוד: \(q\left(x,y_{1},\dots,y_{n}\right)=x-p\left(y_{1},\dots,y_{n}\right)\). ברור שכאשר \(a\in S\) אז \(q\left(a,y_{1},\dots,y_{m}\right)\), שמגדיר את המשוואה \(a=p\left(y_{1},\dots,y_{n}\right)\) יהיה פתיר; וכמובן שאם \(a=p\left(y_{1},\dots,y_{n}\right)\) פתירה אז \(a\in S\), ממש על פי הגדרה.

האתגר הוא הכיוון השני. נניח ש-\(S_{q}\) מוגדרת על ידי \(q\) בצורה ה"ישנה"; איך נמצא פולינום \(p\) שמגדיר אותה בצורה ה"חדשה"? ובכן, נניח ש-\(a\in S\). אז \(q\left(a,y_{1},\dots,y_{m}\right)\) פתיר – אפשר לקבל ממנו אפס. לכן \(p\left(y_{1},\dots,y_{m}\right)=a-q\left(a,y_{1},\dots,y_{m}\right)\) הולך להחזיר \(a\) כאשר מציבים בו בדיוק את הערכים של ה-\(y\)-ים שמאפסים את \(q\left(a,y_{1},\dots,y_{m}\right)\). אבל זה לא מספיק טוב, כי עבור ערכים שונים של ה-\(y\)-ים \(q\) לא בהכרח יתאפס ואז \(a-q\left(a,y_{1},\dots,y_{m}\right)\) יהיה מספר לא קשור. רק מה, צריך לזכור שמותר ל-\(p\) להחזיר מספרים לא קשורים, בתנאי שהם שליליים (או אפס) אז בואו נוודא שנחזיר מספר שלילי, פשוט על ידי כוח גס: \(p\left(y_{1},\dots,y_{m}\right)=a\left(1-q^{2}\left(a,y_{1},\dots,y_{m}\right)\right)\). הבהירו לעצמכם למה הפולינום הזה עושה את העבודה.

אבל רגע, עוד לא סיימנו! הפולינום שלנו עושה את העבודה עבור ערך ספציפי של \(a\), ואנחנו רוצים שהוא יעבוד לכל \(a\). זו לא בעיה, כמובן: הפולינום ה"נכון" הוא \(p\left(x,y_{1},\dots,y_{m}\right)=x\left(1-q^{2}\left(x,y_{1},\dots,y_{m}\right)\right)\), ועכשיו באמת סיימנו את הוכחת המשפט.

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

הבנו קבוצות דיופנטיות? יפה. אז בואו נעבור לסוג מיוחד של קבוצה – פונקציה. פונקציה היא יחס – קבוצה של איברים מהצורה \(\left(x_{1},\dots,x_{n},y\right)\) – עם התכונה המיוחדת שלכל \(x_{1},\dots,x_{n}\) קיים \(y\) כך ש-\(\left(x_{1},\dots,x_{n},y\right)\) שייך לקבוצה, ואותו \(y\) הוא יחיד. חשבו על \(\left(x_{1},\dots,x_{n}\right)\) בתור "קלט" ועל \(y\) בתור "פלט" של הפונקציה. לרוב מסמנים פונקציה ב-\(f\), ואז במקום לומר ש-\(\left(x_{1},\dots,x_{n},y\right)\) שייך לפונקציה, כותבים \(f\left(x_{1},\dots,x_{n}\right)=y\). רובכם בוודאי יודעים את זה (אבל זכרו שלא כל מי שמכיר פונקציות גם מכיר את הגדרתן הפורמלית, התורת-קבוצתית).

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

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

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

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

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

הפונקציות הרקורסיביות הבסיסיות הן:

הפונקציה הקבועה \(c\left(x\right)=1\).
פונקציית העוקב \(s\left(x\right)=x+1\)
פונקצית ההטלה, \(U_{i}^{n}\left(x_{1},\dots,x_{n}\right)=x_{i}\) (המוגדרת לכל \(n,i\)).

טוב, עבור פונקציות הבסיס הללו לא קשה לראות שהן דיופנטיות. הפונקציה הראשונה מוגדרת על ידי:

\(y=c\left(x\right)\iff\left(y=1\right)\)

השניה מוגדרת על ידי:

\(y=s\left(x\right)\iff\left(y=x+1\right)\)

והשלישית מוגדרת על ידי:

\(y=U_{i}^{n}\left(x_{1},\dots,x_{n}\right)\iff\left(y=x_{i}\right)\)

טוב, זה היה מטופש למדי. איפה האתגר? בהמשך.

הפעולה הראשונה שממנה בונים פונקציות רקורסיביות חדשות מתוך הקיימות היא הרכבה. היא מוגדרת כך: אם \(g_{1},\dots,g_{m}\) הן פונקציות רקורסיביות על המשתנים \(x_{1},\dots,x_{n}\) ואילו \(f\) היא פונקציה רקורסיבית על \(m\) משתנים, אז הפונקציה \(h\left(x_{1},\dots,x_{n}\right)=f\left(g_{1}\left(x_{1},\dots,x_{n}\right),\dots,g_{m}\left(x_{1},\dots,x_{n}\right)\right)\) גם היא רקורסיבית. מה שאנחנו רוצים להראות הוא שאותו הדבר קורה עם פונקציות דיופנטיות, כלומר שאם \(g_{1},\dots,g_{m},f\) כולן דיופנטיות, כך גם \(h\).

למרבה המזל, את זה קל להראות כבר עם מעט התכונות שראינו של פונקציות דיופנטיות:

\(y=h\left(x_{1},\dots,x_{n}\right)\iff\exists t_{1},\dots,t_{m}\left(y=f\left(t_{1},\dots,t_{m}\right)\wedge t_{1}=g_{1}\left(x_{1},\dots,x_{n}\right)\wedge\dots\wedge t_{m}=g_{m}\left(x_{1},\dots,x_{n}\right)\right)\)

מה בעצם עשינו כאן? אגף ימין מגדיר פולינום גדול, שמקבל בתור משתנים את \(x_{1},\dots,x_{n}\) וגם את המשתנים \(t_{1},\dots,t_{m}\). עכשיו הוא לוקח את הפולינום שמגדיר את \(f\) (כשהמשתנים בו מתאימים ל-\(t_{1},\dots,t_{m}\) ו-\(y\)), את הפולינום שמגדיר את \(g_{1}\) (כשהמשתנים בו מתאימים ל-\(x_{1},\dots,x_{n}\) ו-\(t_{1}\)), את הפולינום שמגדיר את \(g_{2}\) (כבר הבנתם…?) וכן הלאה עד \(g_{m}\), ואז מחבר את הריבועים של כולם (זו מהות ה-\(\wedge\) שעושים על כולם).

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

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

רקורסיה פרימיטיבית מוגדרת כך: בהינתן פונקציה רקורסיבית \(f\) על \(n\) משתנים ("תנאי ההתחלה"), ופונקציה רקורסיבית \(g\) על \(n+2\) משתנים ("צעד הרקורסיה"), אנחנו מגדירים פונקציה חדשה, \(h\), על \(n+1\) משתנים (שעליהם כדאי לחשוב כך: \(n\) המשתנים הראשונים הם "פרמטרים" קבועים ואילו המשתנה האחרון הוא מה שעליו מוגדרת הרקורסיה), באופן הבא:

\(h\left(x_{1},\dots,x_{n},1\right)=f\left(x_{1},\dots,x_{n}\right)\)

\(h\left(x_{1},\dots,x_{n},t+1\right)=g\left(t,h\left(x_{1},\dots,x_{n},t\right),x_{1},\dots,x_{n}\right)\)

מה קורה כאן? הערך של \(h\) ב"התחלה", כשהמשתנה האחרון הוא 1, נקבע על ידי הפרמטרים ופונקצית תנאי ההתחלה. בהמשך, הערך של \(h\) עבור ערך כלשהו של המשתנה האחרון נקבע על ידי \(g\), כשהיא מביאה בחשבון את הערך הקודם של המשתנה האחרון, הערך ש-\(h\) החזירה על הערך הקודם הזה, והפרמטרים. זה נראה קצת מפחיד אבל זה לא באמת נורא.

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

\(y=h\left(x_{1},\dots,x_{n},z\right)\iff\exists t_{1},t_{2},\dots,t_{z}(t_{1}=f\left(x_{1},\dots,x_{n}\right)\wedge\)

\(\wedge t_{2}=g\left(1,t_{1},x_{1},\dots,x_{n}\right)\wedge t_{3}=g\left(2,t_{2},x_{1},\dots,x_{n}\right)\wedge\dots\)

\(\wedge t_{z}=g\left(z-1,t_{z-1},x_{1},\dots,x_{n}\right)\wedge y=t_{z})\)

מה הולך כאן? אנחנו אומרים ש-\(y=h\left(x_{1},\dots,x_{n},z\right)\) רק אם קיימת סדרה \(t_{1},\dots,t_{z}\) שהאיבר הראשון בה הוא \(f\left(x_{1},\dots,x_{n}\right)\) – הערך ההתחלתי הנכון, בהינתן הפרמטרים – וכל איבר בה נובע מקודמו על ידי \(g\), וכמו כן האיבר האחרון הוא \(y\). מבחינה רעיונית הכל נכון; הבעיה היא סינטקטית – הפסוק שכתבתי כאן לא מתאים ל"שפה" שהצגתי עד כה, מה שאומר שעל פניו לא ברור אם אפשר איכשהו לתרגם אותו חזרה לפולינום שמגדיר פונקציה דיופנטית. בעיה מהותית אחת היא שאורך הפסוק אינו קבוע! הוא תלוי ב-\(z\), כי ככל ש-\(z\) יותר גדול, יש יותר משתנים \(t_{1},\dots,t_{z}\). אם עבור ערכים שונים של \(z\) יש פסוקים שונים, זה אומר שגם יהיו פולינומים שונים, אבל אנחנו צריכים פולינום יחיד שמטפל בכל \(z\). לכן הבניה הזו לא מוצלחת ונזדקק לפיתוח של כלי טכני חדש – פונקציה דיופנטית שמסוגלת לקודד סדרות שרירותיות – על מנת להציע בניה טובה יותר, וגם זה לא יספיק לנו. אבל על כך נדבר בהמשך.

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

אם כן, פונקציות שניתנות ליצירה באמצעות כללי היצירה הנוכחיים מתוך פונקציות הבסיס נקראות פונקציות פרימיטיביות רקורסיביות, וקיימות פונקציות ניתנות לחישוב שאינן פרימיטיביות רקורסיביות. הכלל שפותר את הבעיה הזו הוא כלל שמאפשר לבצע "חיפוש בלתי חסום": אם נתונות פונקציות רקורסיביות \(f,g\) על \(n+1\) משתנים, אז מוגדרת באמצעותן פונקציה רקורסיבית \(h\) על \(n\) משתנים באופן הבא:

\(h\left(x_{1},\dots,x_{n}\right)=\min_{y}\left(f\left(x_{1},\dots,x_{n},y\right)=g\left(x_{1},\dots,x_{n},y\right)\right)\)

כמקודם, חשבו על \(x_{1},\dots,x_{n}\) בתור "פרמטרים". אחרי שקבענו אותם, אנחנו יכולים לחפש את ה-\(y\) המינימלי שעבורו \(f\) תהיה שווה ל-\(g\), וזה הערך ש-\(h\) תחזיר על אותם פרמטרים. אלא שכאן מייד צצה השאלה הפשוטה – מה קורה אם בכלל לא קיים \(y\) כזה? התשובה היא שבמקרה זה \(h\) תהיה לא מוגדרת על הקלט. מרגע שהכנסו את הכלל החדש הזה, שנקרא כלל המינימיזציה לתמונה, גרמנו לכך שקבוצת הפונקציות הרקורסיביות תכלול גם פונקציות חלקיות, כאלו שלא מוגדרות לכל הקלטים (ולמעשה, אפילו הפונקציה שאינה מוגדרת לאף קלט היא רקורסיבית; פשוט קחו את \(f\) להיות הפונקציה שמחזירה תמיד 1 ואת \(g\) להיות הפונקציה שמחזירה תמיד 2). מה שמעניין כאן הוא שפונקציית אקרמן שהזכרתי לעיל כן מוגדרת לכל קלט, כלומר כלל המינימיזציה הכרחי כדי שנוכל "לתפוס" את כל הפונקציות הניתנות לחישוב שמוגדרות לכל קלט; זה לא שהוספנו אותו רק כדי להיות מסוגלים לטפל בפונקציות חלקיות.

טוב, אז הבנו בערך מה זה הכלל הזה; איך אפשר להראות שאם \(f,g\) דיופנטיות, כך גם \(h\)?

שוב, מבחינה רעיונית הפסוק שמגדיר את התכונה הזו אינו מסובך:

\(y=h\left(x_{1},\dots,x_{n}\right)\iff f\left(x_{1},\dots,x_{n},y\right)=g\left(x_{1},\dots,x_{n},y\right)\wedge\)

\(\wedge\forall t\left(t<y\to f\left(x_{1},\dots,x_{n},y\right)\ne g\left(x_{1},\dots,x_{n},y\right)\right)\)

אבל שימו לב לשימוש ב-\(\forall\) ("לכל") כאן. אני כבר יכול לומר שאין שום סיכוי שבשפה שלנו נוכל להשתמש ב-\(\forall\) בצורה חופשית ועדיין לקוות שאפשר יהיה לתרגם את הסיפור חזרה לפונקציה דיופנטית. מה שכן נוכל לעשות – וזה לב ליבה של המטרה הטכנית שלנו – הוא להשתמש ב-\(\forall\) חסום, כלומר במקום לומר "לכל \(t\)", לומר "לכל \(t\) שקטן מ-\(y\)", שזה בדיוק מה שאנחנו צריכים כאן, בעצם.

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

לוגיקה מסדר ראשון

פורסם בתאריך 17 ביוני 2012 על ידי gadial

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

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

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

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

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

בתחשיב הפסוקים בנינו את הפסוקים מתוך "אטומים" שהיו משתנים שיכלו לקבל ערכי \(\mbox{T,F}\) בלבד, וחיברנו אותם זה לזה עם "וגם/או/לא/גורר", וזהו זה. כוח ההבעה שלנו היה מוגבל למדי. הבה ונמחיש זאת עם שתי דוגמאות. הראשונה היא קלאסית, ונוגעת לשרשרת המשפטים הבאה שמשוייכת לאריסטו:

כל בני האדם הם בני תמותה.
סוקרטס הוא בן אדם.
מכאן שסוקרטס הוא בן תמותה.

אינטואיטיבית ברור לנו שההיסק פה "נכון". איך מפרמלים אותו בתחשיב הפסוקים? הרי בתחשיב הפסוקים אין לנו דרך לדבר על "כל" ועל תכונות כמו "מישהו הוא בן אדם/בן תמותה". אפשר היה אולי לחשוב שטענה 1 היא מהצורה \(A\to B\) כאשר \(A\) הוא "בן אדם" ו-\(B\) הוא "בן תמותה", אבל איך זה מתחבר אל סוקרטס? האם טענה 2 היא \(A\)? לא, שהרי \(A\) היא הטענה "בן אדם". היא לא הטענה "סוקרטס הוא בן אדם". אולי צריך להוסיף עוד משתנה עבור "סוקרטס"? ואז טענה 2 היא \(C\to A\)? ואז נסיק איכשהו מצמד הפסוקים \(A\to B\) ו-\(C\to A\) ש-\(C\to B\). זה נשמע לא רע במיוחד, אבל זה אומר שצריך להתאים משתנה מיוחד לכל בן אדם אפשרי. ומה עם זאפוד ביבלברוקס? הוא לא בן אדם. בואו נתאים לו משתנה \(Z\). האם אנחנו צריכים פסוק \(\neg\left(Z\to A\right)\) עבור זאפוד? ומה יקרה אם זאפוד וסוקרטס יופיעו באותו משפט? מה המשמעות של \(\left(C\to A\right)\wedge\neg\left(Z\to A\right)\)? היינו רוצים לומר שהמשפט הזה אומר "סוקרטס הוא בן אדם וזאפוד לא" אבל לשם כך המשתנה \(A\) צריך לקבל גם \(\mbox{T}\) וגם \(\mbox{F}\) בו זמנית (\(\mbox{T}\) לחלק השמאלי של המשפט ו-\(\mbox{F}\) לימני). או לחילופין, צריך יהיה להציב \(\mbox{F}\) או בסוקרטס או בזאפוד, אבל…

טוב, זה די מיש-מש. למרות שאולי אפשר לחלץ מזה משהו, זה כאב ראש לחשוב איך לנסח אפילו משפטים פשוטים בצורה הזו. בואו נעבור עכשיו למשפט קצת יותר מורכב – הגדרת הגבול בחדו"א. אומרים ש-\(\lim_{x\to x_{0}}f\left(x\right)=L\) אם לכל \(\varepsilon>0\) קיים \(\delta>0\) כך שלכל \(x\), אם \(\left|x-x_{0}\right|<\delta\) אז \(\left|f\left(x\right)-L\right|<\varepsilon\). איך אפשר לנסח את שרשרת ה"לכל-קיים-לכל" בעזרת תחשיב הפסוקים? אין לי מושג. ואיך אפשר לנסח את ההפעלה של ערך מוחלט בתוך ההגדרה? לא יודע. ואיך אפשר לנסח את "קטן מ-"? האם צריך שני משתנים שונים, אחד עבור \(\left|x-x_{0}\right|<\delta\) ואחד עבור \(\left|f\left(x\right)-L\right|<\varepsilon\)? הרי התחושה שלנו היא שהמופע של הערך המוחלט, והמופע של ה-\(<\) בשני המקרים הוא מופע של אותו דבר. אנחנו רוצים לחלץ את הרכיבים הדומים, לא להסתיר אותם מאחורי משתנים שונים.

בקיצור, אנחנו עוברים לדבר על לוגיקה מסדר ראשון כדי לשפר את יכולת ההבעה שלנו. לצורך כך אנחנו מרחיבים את התחביר באופן משמעותי. יש לנו, כמקודם, משתנים: \(x_{1},x_{2},x_{3},\dots\). יש לנו את הסימנים הלוגיים של תחשיב הפסוקים, כלומר \(\to,\neg,\wedge,\vee\), ואפשר גם להוסיף \(\leftrightarrow\) כדי לשפר את הקריאות. צריך גם סוגריים ופסיק, כלומר הסימנים \()\) ו-\((\) ו-\(,\) (למה פסיק? עוד מעט נגיע לזה). אבל שני השחקנים החדשים שמקבלים מקום של כבוד הם הסימנים עבור "לכל" ו"קיים": \(\forall\) ו-\(\exists\), שהם מעין A הפוכה (עבור All, "לכל") ו-E הפוכה (עבור Exists, "קיים").

אילו עוד דברים אנחנו צריכים? ובכן, אם ננסה לדבר על תורת הקבוצות נצטרך כנראה סימן עבור יחס השייכות \(\in\) ועבור הקבוצה הריקה \(\emptyset\); אם נדבר על תורת החבורות נצטרך סימן עבור הפעולה הבינארית של החבורה \(\cdot\) ועבור האיבר האדיש לכפל \(e\). אם נדבר על המספרים הטבעיים נצטרך סימן ל-\(0\) וסימן ל"עוקב של מספר", נאמר \(S\) (כך ש-\(S\left(0\right)\) הוא בעצם 1 וכדומה), וכמובן שאת יחס הסדר \(<\) ואת פעולות החיבור \(+\) והכפל \(\times\). ואם נרצה לדבר על גרפים נצטרך עוד סימן יחס שמתאר שיש קשת בין שני צמתים – למשל, \(E\left(v,u\right)\) מתאר זאת. וכו' וכו' וכו'. אנחנו רואים שאנחנו צריכים המון סימנים, אבל שהסימנים הללו הם תלויי שימוש; אנחנו לא חייבים את \(\in\) תמיד אלא רק כשאנחנו רוצים לתאר קבוצות; ואין צורך בסימן \(+\) בתורת החבורות, וכו' וכו'. לכן מטעמי חסכנות אנחנו מרשים להשתמש רק בתת-קבוצה של הסימנים האפשריים. פורמלית, אנחנו מגדירים מילון שהוא אוסף של סימנים שבאים לתאר קבועים, יחסים ופונקציות, כך שכל מילון מגדיר שפה אחרת מסדר ראשון. יש את השפה של תורת החבורות, שהמילון שלה הוא \(\left\langle e,\cdot\right\rangle \); השפה של המספרים הטבעיים עם המילון \(\left\langle 0,S,+,\times\right\rangle \); השפה של תורת הקבוצות עם \(\left\langle \emptyset,\in\right\rangle \) וכן הלאה. כאן \(0,\emptyset\) הם דוגמאות לקבועים, בעוד ש-\(\in\) הוא דוגמא ליחס ו-\(S,+,\times\) הם דוגמאות לפונקציות.

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

יש סימן יחס מיוחד שטרם דיברתי עליו – שוויון, \(=\). יש ספרים שלא מכניסים אותו אוטומטית לשפות, ויש ספרים שכן. אני מעדיף את הגישה שמכניסה אותו אוטומטית למרות שהיא טיפה מגבילה אותנו. אם כן, \(=\) יהיה שייך לקבוצת הסימנים שתמיד יכולים לשמש כחלק מהרכבת פסוקים בשפה – הקבוצה \(\left\{ \to,\neg,\wedge,\vee,\leftrightarrow,),(,,,\exists,\forall,=\right\} \). לסימנים הללו קוראים סימנים לוגיים.

באופן כללי מסמנים פונקציות כמשהו כזה: \(f\left(x_{1},x_{2}\right)\) הוא דוגמה לסימן פונקציה ש"מופעלת" על שני משתנים, \(x_{1},x_{2}\). גם יחסים מתוארים כך -\(R\left(x_{1},x_{2}\right)\) הוא דוגמה. שימו לב מה יש לנו כאן: קודם כל את סימן הפונקציה/יחס; אחר כך סוגר שמאלי (הסוגר הזה הוא חלק מהסימנים הלוגיים!), אחר כך שם של משתנה, אחר כך הסימן "פסיק", אז עוד משתנה, ואז סוגר ימני.

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

שם עצם מוגדר בתור סימן של משתנה (למשל, \(x\)) או סימן של קבוע (למשל, \(c\)) או "הפעלה" של סימן פונקציה על שמות עצם, למשל \(f\left(x,c\right)\) או \(g\left(f\left(x,x,x\right),g\left(c_{1},c_{2}\right)\right)\).

נוסחאות מוגדרות בצורה טיפה יותר מורכבת – ראשית יש נוסחאות אטומיות, שהן תמיד "הפעלה" של סימן יחס כלשהו על שמות עצם כלשהם, למשל \(R\left(f\left(x_{1},x_{2}\right),c\right)\) או \(x_{1}=g\left(x_{2}\right)\) וכדומה. שנית, אם \(\varphi,\psi\) הן נוסחאות, כך גם \(\neg\varphi\) ו-\(\left(\varphi\to\psi\right)\) ו-\(\left(\varphi\leftrightarrow\psi\right)\) ו-\(\left(\varphi\wedge\psi\right)\) ו-\(\left(\varphi\vee\psi\right)\) (זה דומה לתחשיב הפסוקים, עם נוסחאות אטומיות במקום משתנים). לבסוף, לכל משתנה \(x\) ונוסחה \(\varphi\), גם \(\forall x\left(\varphi\right)\) ו-\(\exists v\left(\varphi\right)\) היא נוסחה. זה משלים את הגדרת התחביר (אבל ברצינות, אם אתם רוצים ללמוד את העניין עד הסוף, תצטרכו ספר אמיתי בשביל זה).

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

\(\forall x\forall y\forall z\left(\left(x\cdot y\right)\cdot z=x\cdot\left(y\cdot z\right)\right)\) ("אסוציאטיביות").
\(\forall x\left(x\cdot e=e\cdot x=x\right)\) ("אדיש כפלי").
\(\forall x\exists y\left(x\cdot y=y\cdot x=e\right)\) ("הופכי כפלי").

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

עכשיו בואו נעבור לסמנטיקה.

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

מבנה \(\mathcal{M}\), אם כן, כולל:

קבוצה לא ריקה \(D^{\mathcal{M}}\) – זה "העולם" שממנו ילקחו הערכים שהמשתנים יכולים לקבל.
לכל סימן קבוע \(c\) במילון, איבר \(c^{\mathcal{M}}\in D^{\mathcal{M}}\) – הפרשנות ש-\(c\) מקבל במודל \(\mathcal{M}\).
לכל סימן יחס \(R\) במילון על \(n\) מקומות, יחס \(R^{\mathcal{M}}\subseteq\left(D^{\mathcal{M}}\right)^{n}\).
לכל סימן פונקציה \(f\) במילון על \(n\) מקומות, פונקציה \(f^{\mathcal{M}}:\left(D^{\mathcal{M}}\right)^{n}\to D^{\mathcal{M}}\).

ושוב, אדגיש את ההבדל שיש פה בין הסמנטיקה והתחביר. \(c,R,f\) הם סימנים – אותיות ותו לא, חסרי פשר לכשעצמם ונתונים לפרשנויות רבות; לעומת זאת, \(c^{\mathcal{M}}\) הוא איבר של קבוצה, ו-\(R^{\mathcal{M}}\) הוא יחס על קבוצה ו-\(f^{\mathcal{M}}\) היא פונקציה על קבוצה. יש להם משמעות עמוקה יותר מאשר אוסף פיקסלים.

בואו נחזור אל תורת החבורות שלנו וניתן דוגמאות לשני מבנים אפשריים עבורה. מבנה אחד הוא זה: \(\mathcal{M}=\left(\mathbb{Z},0,+\right)\). כלומר, \(D^{\mathcal{M}}=\mathbb{Z}\) – המספרים השלמים; \(e^{\mathcal{M}}=0\) – כלומר, הפרשנות שלנו לסימן הקבוע \(e\) הוא המספר \(0\in\mathbb{Z}\), ו-\(\cdot^{\mathcal{M}}=+\), כלומר הפרשנות שלנו לסימן הפונקציה \(\cdot\) הוא פעולת החיבור.

מבנה אחר לגמרי הוא זה שבו \(D^{\mathcal{M}}=\mbox{GL}_{n}\left(\mathbb{C}\right)\) – אוסף המטריצות מסדר \(n\times n\) מעל המרוכבים שהדטרמיננטה שלהן שונה מאפס. במבנה הזה \(\cdot\) הוא הפעולה של כפל מטריצות, ו-\(e\) היא מטריצת היחידה (המטריצה שכולה אפסים פרט לאלכסון הראשי שכולו 1). אם אתם לא מכירים את הדוגמה הזו, לא נורא; זה לא קריטי להמשך.

עכשיו, אחרי שהגדרנו מבנה, אפשר להגדיר גם השמה – זו פשוט פונקציה \(s:\left\{ x_{1},x_{2},x_{3},\dots\right\} \to D^{\mathcal{M}}\) שמתאימה לכל משתנה \(x\) איבר כלשהו מתוך \(D^{\mathcal{M}}\). ברגע שבו הגדרנו השמה \(s\), ערך האמת של כל נוסחה נקבע, באופן הבא:

ראשית, אפשר לחשב לכל שם עצם את האיבר שהוא מתאים לו.
שנית, לכל נוסחה אטומית אפשר לחשב אם ערכה הוא \(\mbox{T}\) או \(\mbox{F}\).
כעת קל לחשב מתוך ערכי ה-\(\mbox{T}\) וה-\(\mbox{F}\) הללו ערך אמת לכל הנוסחה כמו בתחשיב הפסוקים.
…למעט במקרה שבו יש לנו כמתים, ואז יש לנו רמה נוספת של סיבוך.

בואו נעבור על זה שלב שלב. ראשית, מרגע שהגדרנו את \(s\) על המשתנים, אפשר להגדיר פונקציה \(\overline{s}\) שהיא הרחבה של \(s\) על כל שמות העצם, באופן הבא: \(\overline{s}\left(x\right)=s\left(x\right)\) לכל משתנה; \(\overline{s}\left(c\right)=c^{\mathcal{M}}\) לכל סימן קבוע \(c\); ו-\(\overline{s}\left(f\left(t_{1},\dots,t_{n}\right)\right)=f^{\mathcal{M}}\left(\overline{s}\left(t_{1}\right),\dots,\overline{s}\left(t_{n}\right)\right)\) לכל סימן פונקציה \(f\).

כאן כדאי לעצור ולוודא שמבינים את הגדרה למעלה. למשל, באגף שמאל של השוויון האחרון יש לנו את הפונקציה \(\overline{s}\) שמופעלת על שם עצם יחיד – \(f\left(t_{1},\dots,t_{n}\right)\). האופן שבו היא פועלת הוא קודם כל לחשב, באופן רקורסיבי, מה ההשמה המורחבת נותנת לכל אחד משמות העצם \(t_{1},\dots,t_{n}\) שהם הרכיבים של שם העצם הזה; לאחר מכן היא לוקחת את הפונקציה \(f^{\mathcal{M}}\) – הפרשנות של סימן הפונקציה \(f\) במבנה \(\mathcal{M}\) – ומפעילה אותה על הערכים שהיא כבר חישבה. התוצאה היא איבר ב-\(D^{\mathcal{M}}\), וזה הערך ש-\(\overline{s}\) נותנת לשם העצם.

למשל, נתבונן בשם העצם \(\left(x\cdot y\right)\cdot e\) שמנוסחת בשפה של תורת החבורות. נניח שהמודל שלנו הוא \(\mathcal{M}=\left(\mathbb{Z},0,+\right)\) שכבר הזכרתי; מה יהיה \(\overline{s}\left(\left(x\cdot y\right)\cdot e\right)\)? מההגדרה שלי ניתן לראות שהוא יהיה \(s\left(x\right)+s\left(y\right)+0\), ולכן אם למשל \(s\left(x\right)=2\) ו-\(s\left(y\right)=3\) נקבל \(\overline{s}\left(\left(x\cdot y\right)\cdot e\right)=5\).

השלב הבא הוא לטפל בנוסחאות האטומיות. נוסחה אטומית כללית נראית כך: \(R\left(t_{1},\dots,t_{n}\right)\) כאשר \(R\) הוא סימן יחס כלשהו. לנוסחה הזו ניתן ערך \(\mbox{T}\) אם מתקיים \(R^{\mathcal{M}}\left(\overline{s}\left(t_{1}\right),\dots,\overline{s}\left(t_{n}\right)\right)\), כלומר אם ביחס \(R^{\mathcal{M}}\), שהוא הפרשנות של סימן היחס \(R\) במבנה \(\mathcal{M}\), האיברים \(\overline{s}\left(t_{1}\right),\dots,\overline{s}\left(t_{n}\right)\) של \(D^{\mathcal{M}}\) אכן נמצאים זה עם זה. שימו לב שזה תלוי הן בערך ש-\(\overline{s}\) מעניקה לשמות העצם, והן בפרשנות של \(R\) ב-\(\mathcal{M}\). היוצא מן הכלל היחיד הוא יחס השוויון, שבו אין "פרשנות" – הוא תמיד מייצג שוויון, כלומר \(t_{1}=t_{2}\) מקבל ערך \(\mbox{T}\) אם ורק אם \(\overline{s}\left(t_{1}\right)=\overline{s}\left(t_{2}\right)\). כאמור, הדרישה הזו מגבילה אותנו במובן מסויים אבל זה לא קריטי כרגע.

כיצד מחשבים ערך אמת כעת עבור פסוקים שבנוים מקשרים אני מקווה שאתם כבר יודעים. למשל, \(\varphi\wedge\psi\) מקבל \(\mbox{T}\) רק אם שני רכיביו קיבלו \(\mbox{T}\) וכדומה.

הסימון הפורמלי לכל זה הוא הסימון הבא: \(\mathcal{M}\models_{s}\varphi\) פירושו "בפרשנות של השפה שנותן המבנה \(\mathcal{M}\), ובהשמה \(s\), הפסוק \(\varphi\) מקבל ערך \(\mbox{T}\)". הסימון הזה הכרחי כדי שיהיה נוח להסביר איך נותנים ערכי אמת עבור פסוקים שמכילים כמתים; לפני כן אצטרך להציג עוד סימון. נניח ש-\(x\) הוא משתנה כלשהו ו-\(a\in D^{\mathcal{M}}\) איבר כלשהו במבנה, וש-\(s\) היא השמה למשתנים. אז אפשר להגדיר השמה אחרת, שאסמן \(s\left[x\leftarrow a\right]\), שהיא זהה ל-\(s\) על כל משתנה אפשרי פרט ל-\(x\), ועל המשתנה הזה היא מחזירה \(a\).

כעת: \(\mathcal{M}\models_{s}\forall x\left(\varphi\right)\) אם לכל \(a\in D^{\mathcal{M}}\) מתקיים \(\mathcal{M}\models_{s\left[x\leftarrow a\right]}\varphi\); ו-\(\mathcal{M}\models_{s}\exists x\left(\varphi\right)\) אם קיים \(a\in D^{\mathcal{M}}\) כך ש-\(\mathcal{M}\models_{s\left[x\leftarrow a\right]}\varphi\). זו ההגדרה הכי קשה כאן; עצרו ונסו לוודא שאתם מבינים מה הולך פה. שימו לב לכך שחישוב ערך האמת של \(\forall x\left(\varphi\right)\) ו-\(\exists x\left(\varphi\right)\) תחת ההשמה \(s\) בעצם מתעלם מהערך ש-\(s\) נותנת ל-\(x\); תחת זאת הוא משחק עם כל ערך אפשרי ורואה מה קורה. זה לא אומר ש-\(s\) לא חשובה; רק שהערך הספציפי שהיא נותנת ל-\(x\) לא רלוונטי.

עם ההגדרה הזו, סיימנו; אנחנו מבינים איך בהינתן מודל והשמה נותנים ערך אמת לכל הנוסחאות. עם זאת, לרוב הנוסחאות שיעניינו אותנו הן נוסחאות שאפשר לדעת מה יהיה ערך האמת שלהן ישר מתוך \(\mathcal{M}\), בלי שהוא יהיה תלוי בהשמה זו או אחרת. לצורך כך אני נזקק להגדרה אחת אחרונה: משתנה בנוסחה כלשהי הוא קשור אם הוא מופיע בטווח של כמת שמתאים לו. למשל, \(\forall x\left(x=y\right)\) היא דוגמה לנוסחה שבה המשתנה \(x\) הוא קשור (כי הוא נופל בתוך הטווח של הכמת \(\forall x\) – בתוך הסוגריים שמייד אחריו). לעומת זאת \(y\) אינו קשור; למשתנה שכזה קוראים חופשי.

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

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

כעת, שימו לב לכך שהמבנה \(\mathcal{M}=\left(\mathbb{Z},0,+\right)\) הוא מודל של תורת החבורות, כלומר של קבוצת שלושת הפסוקים שקראתי לה "תורת החבורות". לעומת זאת, \(\mathcal{M}=\left(\mathbb{Z},1,+\right)\) הוא אמנם מבנה חוקי למהדרין, אבל הוא איננו מודל של תורת החבורות שכן הוא לא מספק את הפסוק \(\forall x\left(x\cdot e=e\cdot x=x\right)\) (בדקו זאת!). זה מתאים לידע שלנו, לפיו \(\left(\mathbb{Z},1,+\right)\) אינה חבורה. למעשה, די ברור שהמודלים של "תורת החבורות" שלנו הם בדיוק המבנים שאנחנו קוראים להם "חבורות"!

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

תחשיב הפסוקים – משפט הקומפקטיות ואיך משפט השלמות דומה למשפט טיכונוף

פורסם בתאריך 24 באפריל 2012 על ידי gadial

להגיב

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

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

פורסם בתאריך 8 באפריל 2012 על ידי gadial

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

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

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

\(\left(\neg\psi\to\neg\varphi\right)\to\left(\varphi\to\psi\right)\) (תבנית אקסיומה 3).
\(\neg\varphi\to\left(\neg\psi\to\neg\varphi\right)\) (תבנית אקסיומה 1).
\(\neg\varphi\) (ניתן להוכחה מ-\(\Phi\)).
\(\neg\psi\to\neg\varphi\) (\(\mbox{MP}\) על 2,3).
\(\varphi\to\psi\) (\(\mbox{MP}\) על 1,4).
\(\varphi\) (ניתן להוכחה מ-\(\Phi\)).
\(\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\). זה מסיים את הוכחת משפט השלמות.

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

לא מדויק

"There’s no sense in being precise when you don’t even know what you’re talking about" (ג'ון פון נוימן)

ארכיון הקטגוריה: לוגיקה