משפטי אי השלמות של גדל

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

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

חזרה למשפטים

רקע

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

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

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

הגדרות

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

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

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

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

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

משפט אי-השלמות הראשון

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

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

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

מספרי גדל. אוסף כל הטקסטים הסופיים בשפה הוא בן מנייה, ולכן ניתן לסדר אותם ברשימה (למשל לפי אורך, ובאותו אורך לפי סדר מילוני) ולתת לכל משפט את מקומו ברשימה כמספר, הנקרא מספר גדל של המשפט, שאותו נסמן בסוגריים מרובעים. לדוגמא, אם [math]\displaystyle{ 3>5 }[/math] הוא המשפט השלישי ברשימה אזי [math]\displaystyle{ [\,3>5\,]=3 }[/math]. באופן דומה, נשתמש בסוגריים מסולסלים כדי לחזור מהמספר אל המשפט: [math]\displaystyle{ \{3\} }[/math] הוא המשפט [math]\displaystyle{ 3>5 }[/math]. חשוב שהמעבר ממשפט למספרו ובחזרה יהיה מכני, וברשימה כזו הוא אכן מכני.

למת האלכסון (Diagonal lemma). לכל פרדיקט [math]\displaystyle{ P(x) }[/math] במשתנה מספרי אחד, הניתן לכתיבה בשפה, קיים משפט [math]\displaystyle{ s }[/math] המקיים

[math]\displaystyle{ s\iff P([s]) }[/math]

כלומר, [math]\displaystyle{ s }[/math] "אומר על עצמו" שיש לו את התכונה [math]\displaystyle{ P }[/math].

הוכחה: נגדיר פונקציה [math]\displaystyle{ f:\N\to\N\cup\{0\} }[/math] באופן הבא:

אם [math]\displaystyle{ \{n\} }[/math] הוא נוסחא [math]\displaystyle{ Q(x) }[/math] במשתנה מספרי יחיד אזי [math]\displaystyle{ f(n):=[Q(n)] }[/math].

אחרת [math]\displaystyle{ f(n):=0 }[/math].

• שימו לב כי [math]\displaystyle{ Q(n) }[/math] הוא הצבת [math]\displaystyle{ n }[/math] בנוסחא עם משתנה, ולכן גם הוא נוסחא בשפה, ולכן יש לו מספר גדל.
• כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור: בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא עצמה.

דוגמא: נניח כי המשפט השלישי ברשימה הוא הנוסחא [math]\displaystyle{ Q(x) }[/math] שאומרת [math]\displaystyle{ x>2 }[/math]. במקרה זה [math]\displaystyle{ f(3)=[Q(3)]=[\,3>2\,] }[/math].

נגדיר כעת את הנוסחא [math]\displaystyle{ B(x)=P(f(x)) }[/math], ונסמן [math]\displaystyle{ s=B([B]) }[/math]. לפי ההגדרה, [math]\displaystyle{ s }[/math] הוא המשפט [math]\displaystyle{ P(f([B])) }[/math]; ולפי הגדרת [math]\displaystyle{ f }[/math], המספר [math]\displaystyle{ f([B]) }[/math] הוא בדיוק [math]\displaystyle{ [B([B])]=[s] }[/math]. לכן [math]\displaystyle{ s\iff P([s]) }[/math], כפי שרצינו. [math]\displaystyle{ \blacksquare }[/math]

• כאן מוסתר הצעד הקשה בעבודתו של גדל: כדי ש-[math]\displaystyle{ B(x)=P(f(x)) }[/math] תהיה נוסחא בשפה, צריך לדעת לכתוב את הפונקציה [math]\displaystyle{ f }[/math] (הצבת מספר בנוסחא) בשפת האריתמטיקה, באמצעות חיבור וכפל בלבד. גדל הראה שכל פונקציה שמחשב יכול לחשב ניתנת לכתיבה כך, ושאז גם השקילות שבלמה ניתנת להוכחה בתוך המערכת. את זה לא נוכיח כאן.

האמת אינה ניתנת להגדרה (משפט טרסקי). מתוך למת האלכסון נובע שלא ניתן להגדיר בשפה את קבוצת המשפטים האמיתיים. הרי אם הייתה נוסחא [math]\displaystyle{ T(x) }[/math] שאומרת "[math]\displaystyle{ \{x\} }[/math] הוא משפט אמיתי", היינו יכולים להגדיר

[math]\displaystyle{ P(x)= }[/math] "[math]\displaystyle{ \{x\} }[/math] אינו משפט אמיתי".

לפי הלמה קיים משפט [math]\displaystyle{ s }[/math] השקול ל"[math]\displaystyle{ s }[/math] אינו אמיתי": אם הוא אמת הוא אינו אמת, ואם הוא אינו אמת הוא אמת. זהו פרדוקס השקרן ("משפט זה אינו אמיתי") בלבוש מתמטי, והסתירה מראה שנוסחא כזו [math]\displaystyle{ T(x) }[/math] לא קיימת.

יכולת הוכחה כן ניתנת להגדרה. לעומת זאת, "[math]\displaystyle{ x }[/math] הוא מספר הגדל של הוכחה של המשפט [math]\displaystyle{ \{y\} }[/math]" היא טענה שניתן לבדוק באופן מכני: עוברים על ההוכחה שורה אחר שורה ובודקים שכל שורה היא אקסיומה (כאן משתמשים בכך שהמערכת ראויה) או נובעת מקודמותיה. לכן, לפי אותה תוצאה של גדל שהוזכרה למעלה, ניתן לכתוב טענה זו כנוסחא בשפה, ואיתה גם את הנוסחא

[math]\displaystyle{ P(x)= }[/math] "לא קיימת הוכחה של [math]\displaystyle{ \{x\} }[/math]" (כלומר "[math]\displaystyle{ \{x\} }[/math] אינו ניתן להוכחה").

סיום ההוכחה. לפי למת האלכסון קיים משפט [math]\displaystyle{ G }[/math] השקול ל"[math]\displaystyle{ G }[/math] אינו ניתן להוכחה".

• אם [math]\displaystyle{ G }[/math] שקר, אזי [math]\displaystyle{ G }[/math] ניתן להוכחה, ומנאותות המערכת [math]\displaystyle{ G }[/math] אמת — סתירה. לכן [math]\displaystyle{ G }[/math] אמת, ולכן (זה בדיוק מה ש-[math]\displaystyle{ G }[/math] אומר) [math]\displaystyle{ G }[/math] אינו ניתן להוכחה.
• גם [math]\displaystyle{ \neg G }[/math] אינו ניתן להוכחה, שהרי הוא שקר, והמערכת מוכיחה רק אמיתות.

מצאנו משפט (אמיתי!) שאינו ניתן להוכחה ואינו ניתן להפרכה, ולכן המערכת אינה שלמה. [math]\displaystyle{ \blacksquare }[/math]

הערה: עקביות במקום נאותות. המשפט כפי שנוסח למעלה דורש רק עקביות. החצי הקל: אם [math]\displaystyle{ G }[/math] היה ניתן להוכחה, הייתה הוכחה קונקרטית עם מספר גדל קונקרטי [math]\displaystyle{ n }[/math]; הטענה "[math]\displaystyle{ n }[/math] הוא הוכחה של [math]\displaystyle{ G }[/math]" היא חישוב סופי, והאקסיומות הבסיסיות של האריתמטיקה מספיקות כדי לאמת כל חישוב סופי, ולכן המערכת מוכיחה "[math]\displaystyle{ G }[/math] ניתן להוכחה", כלומר [math]\displaystyle{ \neg G }[/math]. יחד עם [math]\displaystyle{ G }[/math] זו סתירה, ולכן במערכת עקבית [math]\displaystyle{ G }[/math] אינו ניתן להוכחה. להראות מעקביות בלבד שגם [math]\displaystyle{ \neg G }[/math] אינו ניתן להוכחה קשה יותר: גדל עצמו (1931) הניח תנאי חזק יותר ("ω-עקביות"), ורוסר (1936) הראה כיצד להסתפק בעקביות על ידי בחירה מחוכמת יותר של [math]\displaystyle{ G }[/math].

משפט אי-השלמות השני

--מערכת אקסיומטית ראויה היא עקבית אם"ם לא ניתן להוכיח בה שהיא עקבית (על ידי הוכחה בתוך המערכת).

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

הוכחה. נזכר בהוכחת המשפט הראשון: קיים משפט (נסמן אותו [math]\displaystyle{ G }[/math] על מנת לכבד את גדל, גדל - כבוד) השקול למשפט "[math]\displaystyle{ G }[/math] אינו ניתן להוכחה", וראינו (בהערה שבסוף ההוכחה) שאם המערכת עקבית אז [math]\displaystyle{ G }[/math] אכן אינו ניתן להוכחה.

"המערכת עקבית" הוא בעצמו משפט בשפה: "לא קיימת הוכחה של [math]\displaystyle{ 0=1 }[/math]". נסמן אותו [math]\displaystyle{ \mathrm{Con} }[/math]; ראינו למעלה ש"קיימת הוכחה של..." ניתן לכתיבה בשפה.

נב"ש שהמערכת עקבית ובכל זאת ניתן להוכיח בה את [math]\displaystyle{ \mathrm{Con} }[/math]. הטיעון "אם המערכת עקבית אז [math]\displaystyle{ G }[/math] אינו ניתן להוכחה" הוא טיעון סופי ומכני על הוכחות, ולכן ניתן לבצע אותו גם בתוך המערכת: המערכת מוכיחה "[math]\displaystyle{ \mathrm{Con} }[/math] גורר ש-[math]\displaystyle{ G }[/math] אינו ניתן להוכחה". יחד עם ההוכחה של [math]\displaystyle{ \mathrm{Con} }[/math] מתקבלת הוכחה של "[math]\displaystyle{ G }[/math] אינו ניתן להוכחה", וזהו בדיוק המשפט [math]\displaystyle{ G }[/math]. הוכחנו את [math]\displaystyle{ G }[/math], בסתירה לכך ש-[math]\displaystyle{ G }[/math] אינו ניתן להוכחה. [math]\displaystyle{ \blacksquare }[/math]

מצד שני, אם המערכת אינה עקבית — כלומר מכילה סתירה — אזי ניתן להוכיח בה כל דבר, ובפרט את [math]\displaystyle{ \mathrm{Con} }[/math]. זהו הכיוון השני של אם"ם.

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

מה המשפטים לא אומרים

• לא כל מערכת אקסיומות היא לא-שלמה. המשפטים דורשים שהמערכת תכיל את האריתמטיקה: חיבור וגם כפל. אריתמטיקת פרסבורגר (המספרים הטבעיים עם חיבור בלבד) היא שלמה, ויש אפילו אלגוריתם שמכריע כל משפט בה; כך גם הגאומטריה האוקלידית באקסיומות של טרסקי. הכפל הוא שמאפשר לקודד בשפה את "x הוא הוכחה של y".
• אין כאן "אמיתות שאי אפשר לדעת". המשפט [math]\displaystyle{ G }[/math] אמיתי, ואנחנו יודעים זאת (בהנחה שהמערכת עקבית), פשוט לא מתוך המערכת. במערכת חזקה יותר, למשל כשמוסיפים את [math]\displaystyle{ \mathrm{Con} }[/math] כאקסיומה, [math]\displaystyle{ G }[/math] ניתן להוכחה; אבל למערכת החדשה יש [math]\displaystyle{ G }[/math] משלה. המגבלה היא תמיד על מערכת קבועה אחת, לא על המתמטיקה.
• המתמטיקה לא "מפוקפקת". המשפט השני אומר שאריתמטיקת פאנו אינה מוכיחה את עקביות עצמה, לא שהיא אינה עקבית. את העקביות שלה אפשר להוכיח במערכת רחבה יותר (למשל בתורת הקבוצות, או בהוכחה של גנצן מ-1936), שבתורה אינה מוכיחה את עקביות עצמה, וכן הלאה.