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

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

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

תהי ${\displaystyle T}$ תורה שלמה בשפה מסדר ראשון ${\displaystyle L}$, שניתן להגדיר בתוכה חלק גדול מספיק מהאריתמטיקה של הטבעיים, כך שניתן לתאר בתוכה את מספרי גדל.

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

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

נגדיר את פונקציית הלכסון:

${\displaystyle d(g(\varphi ))=g(\varphi [g(\varphi )])}$

הפונקציה שמקבלת מספר גדל של נוסחה ומחזירה את מספר גדל של הנוסחה המתקבלת מהצבת מספר גדל של הנוסחה המקורית במשתנה הראשון של הנוסחה המקורית (במידה והנוסחה המקורית היא חסרת משתנים נוסיף לה משתנה דמה). כיוון ש-${\displaystyle d}$ ניתנת להגדרה בתוך ${\displaystyle L}$ ניתן גם להגדיר את הנוסחה הבאה במסגרת ${\displaystyle L}$:

${\displaystyle \psi [g(A)]=\neg {\text{True}}[d(g(A))]}$

כעת נברר את ערך האמת של ${\displaystyle \psi [g(\psi )]}$:

${\displaystyle \psi [g(\psi )]\iff \neg {\text{True}}[d(g(\psi )]\iff \neg {\text{True}}[g(\psi [g(\psi )])]}$

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

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

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

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