מכסחי הכמתים

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

1. \( \forall x\forall y\forall z\left(x<y\wedge y<z\to x<z\right) \) (טרנזיטיביות היחס \( < \))
2. \( \forall x\neg\left(x<x\right) \) (אי-רפלקסיביות היחס).
3. \( \forall x\forall y\left(x=y\vee x<y\vee y<x\right) \) (לינאריות היחס - אפשר להשוות כל שני איברים).
4. \( \forall x\forall y\left(x<y\to\exists z\left(x<z\wedge z<y\right)\right) \) (צפיפות היחס - אם \( x<y \) אז יש ביניהם איבר).
5. \( \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 של דברים - זה חשוב כשנכנסים לשאלות של סיבוכיות, אבל אני לא עושה את זה הפעם).

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