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

מתוך ויקיפדיה, האנציקלופדיה החופשית
קפיצה אל: ניווט, חיפוש

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

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

ניסוח מדויק[עריכת קוד מקור | עריכה]

נניח כי T היא תורה שלמה בשפה מסדר ראשון L, שניתן להגדיר בתוכה חלק גדול מספיק מהאריתמטיקה של הטבעיים, כך שניתן לתאר בתוכה את מספרי גדל, אז אין נוסחה True בשפה L כך שלכל משפט A מתקיים: True[g(A)] \iff A (כאשר g(A)‎ הוא מספר גדל המתאים לנוסחה A).

הוכחה[עריכת קוד מקור | עריכה]

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

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

d(g(\varphi)) = g(\varphi[g(\varphi)])

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

\psi[g(A)] = \neg True [ d(g(A))]

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

\psi[g(\psi)] \iff \neg True[ d(g(\psi) ] \iff \neg True[ g(\psi [g(\psi)]) ]

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

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

הערות[עריכת קוד מקור | עריכה]

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

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