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

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

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

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

1. \( \alpha\to\left(\beta\to\alpha\right) \)
2. \( \left[\alpha\to\left(\gamma\to\beta\right)\right]\to\left[\left(\alpha\to\gamma\right)\to\left(\alpha\to\beta\right)\right] \)
3. \( \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 \) אלא רק במופעים החופשיים שלו.

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

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

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

5. \( \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 \) מייצגים נוסחאות):

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

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