הצגת המקור של הדף "משפט האי-גדירות של טרסקי"

ב[[לוגיקה מתמטית]], '''משפט האי-גדירות של [[אלפרד טרסקי|טרסקי]]''' הוא [[משפט (מתמטיקה)|משפט]] הטוען שאין דרך להגדיר בתוך [[תורה (לוגיקה מתמטית)|תורה]] נתונה, מספיק עשירה, את אוסף המשפטים שנכונים בה. באופן לא פורמלי, המשפט אומר כי אם ניתן לנסח במסגרת תורה מסוימת חלק מספיק גדול מתוך ה[[אריתמטיקה]] של המספרים הטבעיים, ובפרט ניתן לקודד כל [[נוסחה]] באמצעות [[מספר טבעי]], אז לא קיימת נוסחה עם משתנה חופשי <math>x</math> שמשמעותה "המשפט המיוצג על ידי המספר <math>x</math> הוא נכון". 

משפט זה התגלה באופן בלתי תלוי על ידי [[קורט גדל]], במסגרת עבודתו על [[משפטי האי-שלמות של גדל|משפטי האי-שלמות]] ועל ידי טרסקי בשנת [[1936]].

==ניסוח מדויק==
תהי <math>T</math> תורה שלמה ב[[שפה מסדר ראשון]] <math>L</math>, שניתן להגדיר בתוכה חלק גדול מספיק מהאריתמטיקה של הטבעיים, כך שניתן לתאר בתוכה את מספרי גדל.

אזי אין נוסחה True בשפה <math>L</math> כך שלכל משפט <math>A</math> מתקיים: <math>\text{True}[g(A)]\iff A</math> (כאשר <math>g(A)</math> הוא מספר גדל המתאים לנוסחה <math>A</math>).

==הוכחה==
ה[[הוכחה בדרך השלילה]], ומכילה רעיונות דומים לרעיונות של הוכחת משפטי האי-שלמות. 

נגדיר את פונקציית הלכסון:
:<math>d(g(\varphi))=g(\varphi[g(\varphi)])</math>
הפונקציה שמקבלת מספר גדל של נוסחה ומחזירה את מספר גדל של הנוסחה המתקבלת מהצבת מספר גדל של הנוסחה המקורית במשתנה הראשון של הנוסחה המקורית (במידה והנוסחה המקורית היא חסרת משתנים נוסיף לה משתנה דמה). 
כיוון ש-<math>d</math> ניתנת להגדרה בתוך <math>L</math> ניתן גם להגדיר את הנוסחה הבאה במסגרת <math>L</math>:
:<math>\psi[g(A)]=\neg\text{True}[d(g(A))]</math>
כעת נברר את ערך האמת של <math>\psi[g(\psi)]</math>:
:<math>\psi[g(\psi)]\iff\neg\text{True}[d(g(\psi)]\iff\neg\text{True}[g(\psi[g(\psi)])]</math>
כלומר נוסחה זו נכונה [[אם ורק אם]] True תטען כי היא שגויה ולהפך, בסתירה להגדרת הנוסחה True.

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

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

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

[[קטגוריה:משפטים בלוגיקה|אי-גדירות של טרסקי]]
[[קטגוריה:משפטי אי היתכנות]]