בטעות מראש 317025
אם תורה Z מכילה משפט C שאומר שהיא עקבית
יש בה תמיד אכסיומה או משפט יכיח שעומד בסתירה
למשפט אחר בתוכה?
בטעות מראש 317039
בסייגים מסויימים, זה נכון. אם תורה <העונה על תנאים מסויימים> מוכיחה את העקביות של עצמה, אז היא לא עקבית, כלומר מוכיחה משהו שעומד בסתירה למשהו אחר שהיא מוכיחה. זה נובע ישירות ("contrapositively") מהמשפט השני של גדל.

כתבת "תורה Z *מכילה* משפט C", ולא ברור לי אם התכוונת לכך ש-C הוא משפט יכיח-פורמלית בתורה, או שהוא כלול ב-Z כאקסיומה; המסקנה ש-Z אינה עקבית נכונה בשני המקרים, אבל כדאי רק לציין שזו משימה מאוד טריקית לייצר אקסיומה כזו שתביא גם את עצמה בחשבון. כלומר, אפשר להוסיף לתורה T את האקסיומה "T עקבית", אבל התורה המתקבלת Z כבר איננה T, והאקסיומה שהוספנו עדיין אומרת רק ש-T עקבית, לא ש-Z כולה היא כזו.
קטונתי מאפס 317060
תודה

איך מיצגים את המשפט תורה T עקבית בצורה אריטמטית ?
קטונתי מאפס 317065
סליחה, ניסוח מחורבן, איך מבטאים עקביות ב-*שפה* קבילה ?
מינוס אחת 317095
אם 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.

(למה קטונת מאפס? זו שאלה מצויינת).
מינוס אחת 317098
לא הבנתי משהו. הנוסחה המתוארת את "X הוא אקסיומה" יכולה להיות בעלת אורך אינסופי? כי הרי יש אינסוף אקסיומות, ולכן אם תכתוב נוסחה בסגנון "X שווה 1 או X שווה 2 או..." לא תגמור אף פעם.
מינוס אחת 317102
בגלל זה דרשנו שאוסף האקסיומות יהיה אפקטיבי: יש אלגוריתם סופי (= נוסחה סופית) המכריע אם נוסחה נתונה היא אקסיומה. גם אם יש אינסוף אקסיומות, יש תכנית מחשב קצרה ופשוטה המזהה אותן.

למשל, ב-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 הוא הקוד של אקסיומה כזו.
מינוס אחת 317106
לא. דרישת האפקטיביות היא בדיוק שניתן לכתוב נוסחה סופית שאומרת "X הוא אקסיומה" ו"X הוא היסק תקף".
מינוס אחת 317112
כמובן שפסוק C לא שקול לעקביות המערכת, אלא רק תנאי הכרחי לה. פסוק העקביות יהיה "לא קיים Y המקודד שרשרת טענות כך שהקוד של הנוסחה 1=0 הוא מסקנה תקינה משרשרת זו, וגם לא קיים Y המקודד שרשרת טענות כך שהקוד של הנוסחה ... היא מסקנה תקינה משרשרת זו, וגם ..."

אבל, איך ניתן לייצג את "פונקצית הגרירה" (שאומרת האם ניתן להסיק מסקנה X מטענות Y, או לא) באמצעות המושגים הבסיסיים של אקסיומות פאנו?
מינוס אחת 317118
לא, הפסוק C שהבאתי שקול לגמרי לעקביות המערכת. אם היא לא עקבית, היא מוכיחה (בקלות) את 0=1, לא צריך אלטרנטיבות.

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

ב. כן, אני אשמח מאוד! תודה!
מינוס אחד 317188
חשבתי שהבנתי שעקביות היא עקביות לגבי מקרה מסוים (לא מופיע 0=1)
לא הבנתי?
מינוס אחד 317189
אם מערכת היא לא עקבית לגבי משהו, היא לא עקבית לגבי הכל. כלומר, אם המערכת שלך מוכיחה 1=0 היא לא עקבית, ואם המערכת שלך לא עקבית היא מוכיחה 1=0. זו בדיוק הבעיה במערכת לא עקבית: אפשר להוכיח ממנה כל מה שרק תרצה.
מינוס אחד 317206
אם אני הבנתי נכון, לא מכל מערכת לא-עקבית אפשר להוכיח הכל - מערכת לא-עקבית היא כזו שיש בה משפט שאפשר להוכיח גם אותו וגם את היפוכו, אבל מכך לא נוגע שבמערכת הזאת אפשר להוכיח *כל* משפט והיפוכו.
מינוס אחד 317207
אם הבנתי נכון, מרגע שאפשר להוכיח במערכת דבר ואת היפוכו, אפשר להוכיח בה כל דבר. לרוע המזל, אני לא זוכר איך טכנית עושים את זה בדיוק, אז נצטרך לחכות לאלון או לאחד המתמטיקאים האחרים.
מינוס אחד 317210
זה תלוי במערכת המדויקת בה עובדים. במערכת עם כלל היסק אחד (מודוס פונס) מקובל להניח את האקסיומה

A->(~A->B)
לכל A ו-B.
אם הוכחת את A וגם את ~A שתי גזירות נותנות לך את B (לכל B שהוא).

במערכות עם הרבה כללי גזירה (ובלי אקסיומות) יש בדרך כלל את הכלל

A->B ' A->~B
----------------------
A

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

נבחן את הטענות הבאות.

1. אם מיץ-פטל הוא בת, אז (מיץ-פטל הוא בת או שאבוקדו זה טעים, או שניהם).

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

2. אם (מיץ-פטל הוא בת או שאבוקדו זה טעים), ומיץ-פטל הוא לא בת, אז אבוקדו זה טעים.

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

עכשיו ניקח את שני אלה יחדיו. נשים לב שהמסקנה של 1 היא בדיוק ההנחה של 2:

1+2. אם (מיץ-פטל הוא בת וגם מיץ-פטל הוא לא בת), אז אבוקדו זה טעים.

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

אם (A נכון וגם A לא נכון), אז B.

לכן, אם מערכת פורמלית מוכיחה ש-‏1=0 וגם ש=1<>0, אז היא מוכיחה כל משפט בשפה, בין אם נכון ובין אם לא נכון.
פינוס גחן 317700
האם יש "אופי" מסוים לתורה הנפרדת ש"נבנת" על משפט C- המשפט הגדלי לעקביות מערכת מסוימת?

אם אי אפשר להוכיח במערכת מסוימת משהו, אז היא עקבית לא? מש"ל לא?

אם מימד הזמן אריטמטי אז הקאווליה של גדל היא האוזניים של אלוהים לא? -סליחה

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

חזרה לעמוד הראשי המאמר המלא

מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים