משתמש:דניאל ב./גדל

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

תנאים

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

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

למעשה בהוכחה המקורית של גדל מופיע תנאי חזק יותר מעקביות. גדל דורש מהתורה שתהיה ω-עקבית (אומגה-עקבית).

• ω-עקביות - בהינתן טענה $\phi (n)$ על המספר הטבעי $n$. אם ניתן להוכיח את הטענות $\phi (1),\phi (2),\phi (3),\ldots$ וכן הלאה לכל n טבעי, אז לא ניתן להוכיח את הטענה $\neg \forall n(\phi (n))$. במילים אחרות, אם ניתן להוכיח טענה כלשהי באופן ספיציפי לכל מספר טבעי, אז לא ניתן להוכיח שקיים מספר טבעי שהטענה אינה מתקיימת לגביו.

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

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

• סימנים לקשרים הלוגיים, $\neg$ (לא) ו-$\lor$ (או), וכן סימן לכמת $\forall$ (לכל).
• סימן לקבוע 0 (אפס) וכן סימן לפונקציית העוקב S(n)‏ (הסימון S(0) הוא 1, S(S(0)) הוא 2 וכן הלאה).
• אינסוף סימני משתנים, $x_{1},x_{2},x_{3},\ldots$.
• סוגריים ימנים ושמאליים.

המשפט הראשון

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

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

מספור גדל

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

שם הסימן	סימן	מספר גדל
אפס	0	1
פונקציית העוקב	S	3
לא	$\neg$	5
או	$\lor$	7
לכל	$\forall$	9
סוגר שמאלי	)	11
סוגר ימני	(	13
המשתנה ה-n	$x_{n}$	$2n+13$

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

כעת לכל ביטוי $a$ בשפה, המורכב מרצף של הסימנים $a=a_{1}a_{2}\ldots a_{k}$, נצמיד מספר גדל ייחודי לו באופן הבא: נניח ש-$n_{1},n_{2},\ldots ,n_{k}$ היא סדרת מספרי גדל המתאימים לסימנים $a_{1},a_{2},\ldots ,a_{k}$ בהתאמה. מספר גדל של $a$ שיסומן $|a|$ הוא המספר $|a|=p_{1}^{n_{1}}\cdot p_{2}^{n_{2}}\cdots p_{k}^{n_{k}}$, כאשר $p_{1},p_{2},\ldots ,p_{k}$ היא סדרת k המספרים הראשוניים הראשונים. בזכות המשפט היסודי של האריתמטיקה ידוע לנו שלכל ביטוי בשפה יהיה מספר גדל יחיד הייחודי רק לו (לכל מספר, יש רק דרך אחת לפרקו לגורמים). בהינתן מספר גדל של ביטוי כלשהו, ניתן לפרק את המספר לגורמים ולחלץ מן הפירוק את רצף הסימנים המרכיב את הביטוי.

דוגמה: נמצא את מספר גדל של הביטוי $a=\forall (x_{3}$ (שהוא חסר פשר). סדרת מספרי גדל של הסימנים בביטוי היא $9,11,19$, ולכן מספר גדל של הביטוי כולו הוא:

$|a|=2^{9}\cdot 3^{11}\cdot 5^{19}=1,729,951,171,875,000,000,000$

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

מספור גדל מאפשר לנו לתרגם מטא-טענות אודות השפה והתורה לטענות אריתמטיות אודות מספרים טבעיים. כל יחס n-מקומי $R$ על ביטויי השפה, נזהה עם יחס אריתמטי n-מקומי אודות מספרים טבעיים $R'$. מתקיים $R(a_{1},\ldots ,a_{n})$ אם ורק אם מתקיים $R'(|a_{1}|,\ldots ,|a_{n}|)$. לדוגמה את יחס השוויון בין שני ביטויים, המוגדר $a=b$ אם ורק אם הם מורכבים מאותו רצף של סימנים, נזהה עם יחס השוויון בין המספרים $|a|=|b|$.

פונקציות רקורסיביות

השלב הבא בהוכחת גדל הוא טכני בעיקרו. גדל משתמש בכוח האריתמטי של התורה כדי לבנות יחס אריתמטי $PF(n,k)$ שניתן להגדרה במסגרת התורה. היחס מתקיים אם ורק אם הביטוי $a$ ש-$n$ הוא מספר גדל שלו, הוא הוכחה לטענה $b$ ש-$k$ הוא מספר גדל שלה.