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

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

1. \( \alpha\to\gamma \) (הנחה).
2. \( \forall x\left(\alpha\to\gamma\right) \) (GEN על 1 עם משתנה שאינו מופיע חופשי ב-\( \Phi \))
3. \( \forall x\left(\alpha\to\gamma\right)\to\left(\alpha\to\forall x\gamma\right) \) (תבנית אקסיומה 5).
4. \( \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 \) כך שמתקיימות שתי התכונות הבאות:

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

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

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 \).

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

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

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

1. \( x=y\to\left(x=x\to y=x\right) \) (אקסיומת שוויון מס' 3 עם \( \varphi=\left(x=x\right) \) ו-\( \psi=\left(y=x\right) \)).
2. \( \forall x\forall y\left(x=y\right)\to\left(x=x\to y=x\right) \) (Gen על 1).
3. \( \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)
4. \( c=d\to\left(c=c\to d=c\right) \) (MP על 2,3).
5. \( c=d \) (יכיח מ-\( \Phi \)).
6. \( c=c\to d=c \) (MP על 4,5).
7. \( c=c \) (יכיח מ-\( \Phi \)).
8. \( 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 \). אם אתם תוהים למה הוא יכיח, הנה הוכחה פורמלית:

1. \( \forall x\neg\varphi\left(x\right)\to\neg\varphi\left(c\right) \) (תבנית אקסיומה 4).
2. \( \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).
3. \( \neg\neg\varphi\left(c\right)\to\neg\forall x\neg\varphi\left(x\right) \) (MP על 1,2).
4. \( \neg\neg\varphi\left(c\right)\to\exists x\varphi\left(x\right) \) (סתם שינוי סימון שיהיה קריא).
5. \( \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) \)).
6. \( \varphi\left(c\right)\to\exists x\varphi\left(x\right) \) (MP על 4,5).

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

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