חזרה ל[[משפטי אי השלימות של גדל (Gödel)]]
==הוכחת משפט אי השלימות האי-שלימות הראשון של גדל==אוסף כל המשפטים בתאוריה הוא בן מנייה. על כן ניתן לתת לכל משפט בתאוריה מספר (הנקרא '''מספר גדל''') שאותו נסמן בסוגריים מרובעים.<br>לדוגמא: אם <math>''3 > 5''</math> הוא המשפט השלישי בתאוריה אזי <math>[''3>5'']=3</math>.<br>באופן דומה, נשתמש בסוגריים מסולסלים על מנת לחזור מהמספר אל המשפט. בדוגמא: <math>\{3\}=\,''\!3>5''</math>.
מכיוון שאוסף כל המשפטים בתאורייה הוא בן מנייה ניתן לתת לכל משפט בתאוריה מספר ===הלמה של טרסקי (הנקרא '''מספר גדל'''Diagonal lemma), נסמן מספר זה בסוגריים מרובעים. לדוגמא: אם ===לכל פרדיקט עם משתנה מספרי אחד <math>''3 > 5''P(x)</math> הוא המשפט השלישי בתאורייה אזי קיים בתאוריה משפט <math>[''3 > 5'']=3s</math>. באופן דומה, נשתמש בסוגריים מסולסלים על מנת לחזור מהמספר אל המשפט. בדוגמאעבורו:: <math>s\{3\}=''3 > 5''iff P([s])</math>.
===הלמה של טרצקי (Diagonal lemma)===
::--לכל פרדיקט עם משתנה מספרי אחד <math>P(x)</math> קיים בתאוריה משפט s כך ש:
::::::s אם"ם <math>P([s])</math>
===הוכחה===
נגדיר פונקציה <math>f:\mathbb{N}\rightarrowto\mathbb{N}\cup\{0\}</math> באופן הבא:::אם <math>\{n\}=Q(x)</math> הוא נוסחא עם משתנה במשתנה מספרי יחיד <math>P(x)=\{n\}</math> אזי <math>f(n):=[PQ(n)]</math>.::אחרת, <math>f(n):=0</math>.*שימו לב שכי <math>PQ(n)</math> הוא הצבת <math>n </math> בנוסחא עם משתנה, ולכן גם מהווה נוחסחא נוסחא בתאוריה ולכן יש לו מספר גדל.
*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.
דוגמא:
נניח והמשפט כי המשפט השלישי בתאוריה הוא נוסחא מספרית <math>PQ(x)=\,''\!x>2''</math>. במקרה זה <math>f(3)=[PQ(3)]=[''3>2'']</math>. נגדיר כעת את הנוסחא הבאה <math>B(x)=P(f(x))</math>.
'''טענה''':
<math>B([B])\iff P([B([B])])</math> לכל <math>x</math>.
נגדיר כעת את הנוסחא הבאה ====הוכחה====כיוון אחד: נניח <math>B(x[B])=\forall z:</math>. לכן <math>P(z=f(x[B])\rightarrow )</math>. נשים לב כי <math>f([B])=[B([B])]</math>. נובע כי <math>P(z[B([B])])</math>כפי שרצינו.
כיוון שני:'''טענה''': נניח <math>P([B([B])\iff P])</math>. מהעובדה כי <math>f([B])=[B([B])]</math> נובע כי <math>P(f([B]))</math> לכן לפי ההגדרה <math>B([B])</math> לכל x.
'''הוכחה''':
נניח <math>B([B])</math>. לכן עבור <math>\forall z:(z=f([B])\rightarrow P(z))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. בפרט, עבור <math>z=[B([B])]</math> נובע כי <math>P([B([B])])</math> כפי שרצינו.
'''מסקנה''': המשפט <math>s=B([B])</math> מקיים:
:<math>s\iff P([s])</math>
כפי שרצינו.
מצד שני, נניח <math>P([B([B])])</math>===סיום הוכחת משפט האי-שלימות הראשון של גדל בעזרת הלמה של טרסקי===שימו לב כי מתוך הלמה של טרסקי לא ניתן להגדיר את קבוצת כל המשפטים שהם 'אמת'. הרי אם <math>z\neq[B([B])]</math> היתה קבוצה כזו, אזי שקר גורר כל דבר ובפרט את ניתן היה להגדיר נוסחא מספרית:<math>=P(zx)</math>. אם "<math>z=[B([B])]</math> אזי <math>z=[B([B])]\rightarrow P(z){x\}</math> שכן אמת גוררת אינו שייך לקבוצת המשפטים שהם 'אמת'". לפי הלמה קיים משפט השקול לכך שאינו בקבוצת האמת, ולכן סה"כאם הוא אמת הוא אינו אמת, הגרירה נכונה לכל <math>z</math> ולכן <math>Bואם הוא אינו אמת הוא אמת. ([B]זו סתירה הדומה לפרדוקס של ראסל.)</math>.
לעומת זאת, מכיוון שאוסף כל הטקסטים בשפה הוא בן מנייה, בפרט אוסף ההוכחות הוא בין מנייה, ולכן ניתן להגדיר את קבוצת כל המשפטים שניתן להוכיח (הם פשוט השורה האחרונה של כל הוכחה תקינה). נגדיר את הנוסחא
:<math>=P(x)</math> "<math>\{x\}</math> אינו שייך לקבוצת המשפטים הניתנים להוכחה".
כעת לפי הלמה של טרסקי יש משפט השקול לכך שהוא אינו בקבוצת המשפטים הניתנים להוכחה. אם הוא היה שקר, סימן שהוא ניתן להוכחה ולכן הוא אמת וזו סתירה. אם הוא אמת, לעומת זאת, אין סתירה אך הוא אינו ניתן להוכחה.
'''מסקנה''': מכאן המשפט <math>s=Bנובע באופן ישיר: או שהתאוריה אינה שלימה ([B]קיים משפט שלא ניתן להוכיחו או להפריכו)</math> מקיים <math>s \iff Pאו שהיא אינה עקבית ([s]היא מכילה סתירה)</math> כפי שרצינו.