 |
|
 |
||
|
||||
 |
אם תורה Z מכילה משפט C שאומר שהיא עקבית יש בה תמיד אכסיומה או משפט יכיח שעומד בסתירה למשפט אחר בתוכה? |
 |
 |
 |
|
|
|
||
|
||||
|
בסייגים מסויימים, זה נכון. אם תורה <העונה על תנאים מסויימים> מוכיחה את העקביות של עצמה, אז היא לא עקבית, כלומר מוכיחה משהו שעומד בסתירה למשהו אחר שהיא מוכיחה. זה נובע ישירות ("contrapositively") מהמשפט השני של גדל. כתבת "תורה Z *מכילה* משפט C", ולא ברור לי אם התכוונת לכך ש-C הוא משפט יכיח-פורמלית בתורה, או שהוא כלול ב-Z כאקסיומה; המסקנה ש-Z אינה עקבית נכונה בשני המקרים, אבל כדאי רק לציין שזו משימה מאוד טריקית לייצר אקסיומה כזו שתביא גם את עצמה בחשבון. כלומר, אפשר להוסיף לתורה T את האקסיומה "T עקבית", אבל התורה המתקבלת Z כבר איננה T, והאקסיומה שהוספנו עדיין אומרת רק ש-T עקבית, לא ש-Z כולה היא כזו. |
|
|
|
|
|
|
||
|
||||
|
תודה איך מיצגים את המשפט תורה T עקבית בצורה אריטמטית ? |
|
|
|
|
|
|
||
|
||||
|
סליחה, ניסוח מחורבן, איך מבטאים עקביות ב-*שפה* קבילה ? | |
|
|
|
|
|
||
|
||||
|
אם T מערכת אקסיומטית כמתואר במאמר, אז הוכחה ב-T היא פשוט שרשרת של נוסחאות שכל אחת מהן היא או אקסיומה או או מסקנה פורמלית מהנוסחאות הקודמות. שרשרת כזו אפשר לקודד כמספר - כמו שקבצים במחשב מקודדים כמספרים. בגלל מה שכינינו אפקטיביות, יש נוסחה אריתמטית האומרת "X הוא מספר של נוסחה המהווה אקסיומה", ויש נוסחה אחרת האומרת "X הוא מספר של מסקנה פורמלית תקינה משרשרת הטענות שמספרה הוא Y". זה אולי נראה מבלבל, אבל זה באמת פשוט. נניח שיש במערכת את האקסיומה "0=0" ונניח שהקידוד המספרי המתאים למחרוזת הזו הוא המספר 137,111,137 (מאה-שלושים-ושבעה מיליון, מאה ואחת-עשרה אלף מאה שלושים ושבע). אז הנוסחה המתארת את "X הוא אקסיומה" יכולה להתחיל כך: X = 137,111,137 or X = ... כעת אפשר לרשום את הנוסחה הבאה C: "לא קיים Y המקודד שרשרת טענות כך שהקוד של הנוסחה 1=0 הוא מסקנה תקינה משרשרת זו". אם במערכת יש אקסיומה, או שניתן להוכיח, שאפס *שונה* מאחד (וכך הוא, למשל, ב-PA, או בכל תורה אריתמטית סבירה), הרי שהוכחה שאפס *שווה* לאחד תעיד על חוסר עקביות. לכן, C מבטאת את עקביותה של המערכת: היא אומרת שאין במערכת גזירה של הטענה 1=0.(למה קטונת מאפס? זו שאלה מצויינת). |
|
|
|
|
|
|
||
|
||||
|
לא הבנתי משהו. הנוסחה המתוארת את "X הוא אקסיומה" יכולה להיות בעלת אורך אינסופי? כי הרי יש אינסוף אקסיומות, ולכן אם תכתוב נוסחה בסגנון "X שווה 1 או X שווה 2 או..." לא תגמור אף פעם. | |
|
|
|
|
|
||
|
||||
|
בגלל זה דרשנו שאוסף האקסיומות יהיה אפקטיבי: יש אלגוריתם סופי (= נוסחה סופית) המכריע אם נוסחה נתונה היא אקסיומה. גם אם יש אינסוף אקסיומות, יש תכנית מחשב קצרה ופשוטה המזהה אותן. למשל, ב-PA יש אינסוף אקסיומות: 1. אם הטענה x=x נכונה כש-x=0, ואם נכונות הטענה הזו כש-x=n גוררת את נכונותה כש=x=n+1, אז הטענה x=x נכונה לכל מספר טבעי. 2. אם הטענה x=x+1 נכונה כש-x=0, ואם נכונות הטענה הזו כש-x=n גוררת את נכונותה כש=x=n+1, אז הטענה x=x+1 נכונה לכל מספר טבעי. 3. אם הטענה "2x הוא קטן מארבע או שהוא סכום של שני ראשוניים" נכונה כש-x=0, ואם נכונות הטענה הזו כש-x=n גוררת את נכונותה כש=x=n+1, אז הטענה "2x הוא קטן מארבע או שהוא סכום של שני ראשוניים" נכונה לכל מספר טבעי. ... כולן זהות, פרט לנוסחה P בעלת משתנה חופשי x המופיעה בהן. לא קשה לכתוב תכנית שתדע לומר אם מחרוזת מסויימת היא אחת האקסיומות בסכימה הזו, ואח"כ אפשר לכתוב *נוסחה* שתהיה נכונה ל-X אם"ם X הוא הקוד של אקסיומה כזו. |
|
|
|
|
|
|
||
|
||||
|
לא. דרישת האפקטיביות היא בדיוק שניתן לכתוב נוסחה סופית שאומרת "X הוא אקסיומה" ו"X הוא היסק תקף". | |
|
|
|
|
|
||
|
||||
|
כמובן שפסוק C לא שקול לעקביות המערכת, אלא רק תנאי הכרחי לה. פסוק העקביות יהיה "לא קיים Y המקודד שרשרת טענות כך שהקוד של הנוסחה 1=0 הוא מסקנה תקינה משרשרת זו, וגם לא קיים Y המקודד שרשרת טענות כך שהקוד של הנוסחה ... היא מסקנה תקינה משרשרת זו, וגם ..." אבל, איך ניתן לייצג את "פונקצית הגרירה" (שאומרת האם ניתן להסיק מסקנה X מטענות Y, או לא) באמצעות המושגים הבסיסיים של אקסיומות פאנו? |
|
|
|
|
|
|
||
|
||||
|
לא, הפסוק C שהבאתי שקול לגמרי לעקביות המערכת. אם היא לא עקבית, היא מוכיחה (בקלות) את 0=1, לא צריך אלטרנטיבות. "פונקציית הגרירה" היא לא יותר מיישום של אחת מבין משהו כמו תשע אלטרנטיבות למניפולציה פורמלית על מחרוזת. אין קושי רב לתרגם את המניפולציות הללו לנוסחאות. אתה רוצה לראות ממש איך זה נעשה? |
|
|
|
|
|
|
||
|
||||
|
א. אה, נחמד! ב. כן, אני אשמח מאוד! תודה! |
|
|
|
|
|
|
||
|
||||
|
חשבתי שהבנתי שעקביות היא עקביות לגבי מקרה מסוים (לא מופיע 0=1) לא הבנתי? |
|
|
|
|
|
|
||
|
||||
|
אם מערכת היא לא עקבית לגבי משהו, היא לא עקבית לגבי הכל. כלומר, אם המערכת שלך מוכיחה 1=0 היא לא עקבית, ואם המערכת שלך לא עקבית היא מוכיחה 1=0. זו בדיוק הבעיה במערכת לא עקבית: אפשר להוכיח ממנה כל מה שרק תרצה. | |
|
|
|
|
|
||
|
||||
|
אם אני הבנתי נכון, לא מכל מערכת לא-עקבית אפשר להוכיח הכל - מערכת לא-עקבית היא כזו שיש בה משפט שאפשר להוכיח גם אותו וגם את היפוכו, אבל מכך לא נוגע שבמערכת הזאת אפשר להוכיח *כל* משפט והיפוכו. | |
|
|
|
|
|
||
|
||||
|
אם הבנתי נכון, מרגע שאפשר להוכיח במערכת דבר ואת היפוכו, אפשר להוכיח בה כל דבר. לרוע המזל, אני לא זוכר איך טכנית עושים את זה בדיוק, אז נצטרך לחכות לאלון או לאחד המתמטיקאים האחרים. | |
|
|
|
|
|
||
|
||||
|
זה תלוי במערכת המדויקת בה עובדים. במערכת עם כלל היסק אחד (מודוס פונס) מקובל להניח את האקסיומה A->(~A->B) לכל A ו-B.אם הוכחת את A וגם את ~A שתי גזירות נותנות לך את B (לכל B שהוא). במערכות עם הרבה כללי גזירה (ובלי אקסיומות) יש בדרך כלל את הכלל A->B ' A->~B בשני המקרים, מדובר בעצם בהנחת המבוקש: מניחים שסתירה משמעה שאחת ההנחות שלך שגויה.---------------------- A אפשר לא להוסיף את האקסיומה/ כלל גזירה הנ"ל ולקבל תורות לא טריויאליות עם סתירה. אני לא יודע אם זה מענין או למה זה טוב. |
|
|
|
|
|
|
||
|
||||
|
אני אנסה לשכנע שזו תוצאה טבעית מהדרך בה אנו מבינים את מושג ה"נביעה" או "גרירה". אורי כבר הראה את זה בלשון פורמלית; אני אנסה להדגים את זה בשפה טבעית. נבחן את הטענות הבאות. 1. אם מיץ-פטל הוא בת, אז (מיץ-פטל הוא בת או שאבוקדו זה טעים, או שניהם). זו נראית כמו טענה משונה קצת, אבל אם חושבים עליה אין ספק שהיא נכונה: אם *מניחים* שמיץ הוא בת, ודאי שמתקיים שמיץ הוא בת או ש... (לא חשוב מה). את ה"או שניהם" הזה בסוף חשוב להגיד בשפה טבעית, אבל במתמטיקה זו הפרשנות הרגילה של המילה "או", אז מכאן ואילך נכתוב סתם "או". 2. אם (מיץ-פטל הוא בת או שאבוקדו זה טעים), ומיץ-פטל הוא לא בת, אז אבוקדו זה טעים. זה גם ברור: הנחתי שלפחות אחד משני דברים מתקיים, ואז הנחתי שאחד מהם לא מתקיים, מה שלא מתיר ברירה לשני אלא להיות נכון. עכשיו ניקח את שני אלה יחדיו. נשים לב שהמסקנה של 1 היא בדיוק ההנחה של 2: 1+2. אם (מיץ-פטל הוא בת וגם מיץ-פטל הוא לא בת), אז אבוקדו זה טעים. כלומר, אם הגענו איכשהו למסקנה המופרכת שזה גם נכון וגם לא נכון שמיץ הוא בת, אפשר להסיק מסקנות מאוד מופרכות אחרות כמו שאבוקדו זה טעים(!). ובאופן כללי: אם (A נכון וגם A לא נכון), אז B. לכן, אם מערכת פורמלית מוכיחה ש-1=0 וגם ש=1<>0, אז היא מוכיחה כל משפט בשפה, בין אם נכון ובין אם לא נכון. |
|
|
|
|
|
|
||
|
||||
|
האם יש "אופי" מסוים לתורה הנפרדת ש"נבנת" על משפט C- המשפט הגדלי לעקביות מערכת מסוימת? אם אי אפשר להוכיח במערכת מסוימת משהו, אז היא עקבית לא? מש"ל לא? אם מימד הזמן אריטמטי אז הקאווליה של גדל היא האוזניים של אלוהים לא? -סליחה ותודה |
|
|
|
|
|
|
||
|
||||
|
''אם אי אפשר להוכיח במערכת מסוימת משהו, אז היא עקבית'' - הבעיה היא שכל הוכחה לפיה בעיה אינה כריעה, מתבססת על ההנחה שהמערכת עקבית. | |
|
|
|
|
|
||
|
||||
|
כן כן ברור, זה בדיוק המשפט שאי אפשר להוכיח בתוך המערכת. לרגע חשבתי שאמרתי משהו חכם. שלוש שניות של גאווה. אני אחזור לחור שלי עכשיו. |
|
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |