בתשובה לאלון עמית, 17/07/05 17:17
 |
|
 |
||
|
||||
 |
אני לא זוכר את משפט טיורינג. ואין לי אף מערכת ספציפית בראש. אני רק חושב שזה מעניין (אם זה נכון) שיש תורות שיודעים אליהם שאינן שלמות, ויש תורות שיודעים אליהם שהן שלמות. אבל כל התורות מהסוג הראשון איזומורפיות1 המספרים השלמים. אני הייתי מצפה שיקרה אחד מהדברים הבאים: 1. איזה מתמטיקאי ימצא תורה שאיננה שלמה, ואיננה איזומורפית1 בשום צורה שהיא למספרים השלמים. 2. איזה מתמטיקאי יוכיח שלא קיימת תורה שאיננה שלמה, מלבד המספרים השלמים (והתורות האיזומורפיות1 לה). 3. איזה מתמטיקאי יוכיח שמשפט 2 בלתי ניתן להוכחה ולהפרכה. 4. איזה מתמטיקאי ימצא (או, אפילו יוכיח) כלל שאומר איזה תורות שלמות ואיזה לא. 1 בכל מקום בו כתוב "איזומורפי" יש להחליף ב"דומה בצורה כלשהי שאני לא יודע איך לקרוא לה מכיוון שמשפט גדל גדול עלי בכמה מידות", על כל ההטיות המתאימות. |
 |
 |
 |
|
|
|
||
|
||||
|
יש המון תורות שאינן שלמות ואינן איזומורפיות או מכילות (או מה-שלא-יהיה) לטבעיים. למשל התורה הריקה, אין בה אקסיומות בכלל (חוץ מהאקסיומות הלוגיות הרגילות). האם קיים משהו כלשהו? התורה לא מכריעה. רוצה קצת יותר? התורה שאומרת שקיים אובייקט אחד לפחות. האם יש שניים? התורה לא מכריעה. לדוגמאות פחות ביזאריות/טריויאליות ראה תגובה 317393 |
|
|
|
|
|
|
||
|
||||
|
לא הבנתי את שלושת הדוגמאות שלך. התורה לא אמורה להכריע בקשר לדברים שאינם מוגדרים בתורה, לא? | |
|
|
|
|
|
||
|
||||
|
קרא את תגובה 317614 וחזור אלי אם עדיין לא מובן. | |
|
|
|
|
|
||
|
||||
|
קראתי. (האמת, מלבד הסמנטיקה, זה לא חידש לי כלום. דווקא תגובה 318023 הצליחה להסביר את זה בצורה פשוטה מספיק בשביל שאבין). | |
|
|
|
|
|
||
|
||||
|
התורה לא אמורה להכריע לגבי דברים שאי אפשר לנסח ב*שפה*. למשל, את המשפט "לכל X יש Y כך ש-(f(X,Y" אפשר לנסח בכל שפה שיש בה "לכל", "יש", משתנים X ו-Y, ויחס דו-מקומי כלשהו f. זה כשלעצמו לא אומר כלום על האקסיומות של התורה; יכולות להיות לה מעט, הרבה, פשוטות, מסובכות, לא חשוב. אתה יכול לבנות תורה פשוטה המפרמלת תכונות של תגובות באייל: כל תגובה היא תגובה למאמר או תגובה לתגובה אחרת; לכל תגובה יש תגובה-אם יחידה (או מאמר-אב יחיד); תגובת-האם של תגובה שונה מהתגובה עצמה, ונגיד שעצרת כאן. אפשר לנסח עכשיו את המשפט "יש תגובה א' שהיא תגובה לתגובה ב' שהיא תגובה לתגובה א"'. זה לא קורה באייל, אבל האקסיומות שהצגנו לא מספיקות כדי להוכיח זאת (וכמובן שאינן מוכיחות גם שזה *כן* קורה), והרי לך עוד תורה לא-שלמה ולא-אריתמטית. "אי-שלמות" היא תכונה נגטיבית, ויש אותה להמון תורות; משפט גדל מפתיע בכך שהוא אומר שיש אותה ל*כל* תורה אריתמטית+עוד תכונות. לא נראה לי שיש דרך סבירה "לאפיין" תורות לא-שלמות (חוץ מאשר לומר עליהן שהן לא שלמות). |
|
|
|
|
|
|
||
|
||||
|
אני חושב שהבנתי, עכשיו מה שאני לא מבין זה למה עשו מהמשפט הזה כזה סיפור. | |
|
|
|
|
|
||
|
||||
|
בדוגמה שהבאתי של מבנה התגובות באייל, ברור שסתם לא שמתי מספיק אקסיומות; אילו התאמצתי יותר, הייתי יכול להגיע למצב של שלמות: כל טענה נכונה על מבנה עץ-התגובות אפשר היה להוכיח. לפני גדל, היתה תקווה - לא בלתי-סבירה - שאפשר יהיה לעשות זאת גם לדבר שנראה כה פשוט: המספרים הטבעיים. כשגדל הראה שזה בלתי-אפשרי, היתה התרגשות מוצדקת - זו אכן התפתחות דרמטית ביסודות המתמטיקה. עם זאת, אתה יכול לתאר לעצמך שאני לא בדיוק מתווכח עם התיזה ש"עשו ממנו כזה סיפור" *מחוץ* למתמטיקה. |
|
|
|
|
|
|
||
|
||||
|
ועוד שתי שאלות (מצטער, אני יודע שאלה שאלות טפשיות, שבטח גם ענית להם קודם). א. איפשהו (תגובה 317163, הי, הנה משהו כן נקלט) כתבת הגיאומטריה היא מערכת שלמה. איך הוכיחו את זה? אך בכלל מוכיחים דבר כזה על תורות לא טריויאליות? ב. אם יש לי תורה לא שלמה (נגיד, המספרים השלמים), ז"א יש לה משפט שאי אפשר להוכיח אותו או להפריך אותו אז האם אפשר לבנות תורה חדשה שהמשפט הזה הוא אקסיומה (שלילית או חיובית)? האם אפשר להפוך בדרך כזו את המספרים השלמים לתורה שלמה (גם אם בעזרת הוספת אין סוף אקסיומות)? |
|
|
|
|
|
|
||
|
||||
|
א. על השאלה האחרונה יותר קל לי לענות. כדי להוכיח שלמות של תורה, צריך לטפל באיזשהו אופן בכל הנוסחאות בשפה שלה ולהוכיח שהן כריעות. דרך נוחה, יחסית, לעשות זאת היא לפתח תהליך של "פישוט" נוסחאות כאלה: מראים שכל נוסחה שקולה לאחת אחרת בעלת מבנה פשוט יותר, וזאת תוך שימוש באקסיומות של התורה. נדמה לי שהמכשיר החשוב ביותר מסוג זה נקרא "חילוץ כמתים". באופן לא מפתיע, עיקר הקושי בתורות מסדר ראשון נעוץ בכמתים "יש" ו"לכל"; כשיש הרבה מזל, אפשר להראות איך לקחת נוסחה ולהתחיל להעיף ממנה כמתים, וכשיש המון מזל, אפשר להראות שאפשר להישאר בלי כמתים בכלל. המונח הטכני הוא "חילוץ כמתים" (quantifier elimination), ולמרות שלמדתי על זה קצת פעם אין לי די ידע כדי להסביר את זה כאן באופן סביר (אני מהמר שאורי יכול, למרות קיטוריו) - בכל אופן, יש על זה לא מעט מידע ברשת. ספציפית לגבי גיאומטריה, אני לא חושב שאי-פעם ראיתי את ההוכחה, אך אני יכול לנחש כמה דרכים לעשות זאת - אם לא יענו לך אחרים אנסה את כוחי. ב. לשאלה הראשונה: בוודאי, למה לא? אין תורות שאסור לבנות; מקסימום תצא תורה לא מעניינת באיזשהו אופן. אכן, בכל פעם שמתגלה משפט לא כריע אפשר "לפצל" את התורה הפורמלית ולבנות שתי תורות מתחרות: אחת שבה הוא נכון ואחת שלא. חשוב לזכור שלתורות האלה אין בהכרח מעמד שווה; ברוב המצבים, אחת מהן היא "סבירה" והשנייה "משונה". לשאלה השנייה: לא אם אתה מתעקש להישאר עם תורה עקבית ואפקטיבית. אם מוותרים על עקביות, זה קל: מוסיפים אקסיומה הסותרת אקסיומה קיימת, ומקבלים מערכת לא-עקבית (אבל שלמה!). גם אם מנסים להשאיר עקביות תוך ויתור על אפקטיביות, אפשר לבנות תורות שלמות לשלמים - הזכרנו אחת כבר, "True Arithmetic", שפשוט יש בה את כל המשפטים הנכונים בתור אקסיומות. זו לא תורה מעניינת מההיבט המעשי כי אין אלגוריתם שיוכל להגיד לך אם משהו הוא אקסיומה. אם אכן שומרים על עקביות ואפקטיביות, ברור שמשפט גדל יחול גם על המערכת המורחבת (בהנחה שהוא חל על המקורית), ולא הרווחנו כלום בהיבט הזה. למשפט גדל לא משנה אם יש מספר סופי או אינסופי של אקסיומות. אני אחכה בסבלנות שתגשים את הבטחתך לשאול שאלות טפשיות. |
|
|
|
|
|
|
||
|
||||
|
כאן המקום להעיר שלכל תורה אפקטיבית ושלמה (בפרט לא אריתמטית) יש אלגוריתם שמכריע עבור כל משפט האם הוא נכון או לא. לפעמים האלגוריתם הזה הוא "חיסול כמתים" (למה חילוץ? למה להיות חיובי?). אם יהיה ביקוש, אני ארחיב. | |
|
|
|
|
|
||
|
||||
|
רגע - זה ברור, לא? אם תורה היא אפקטיבית, אפשר לייצר אחד-אחד את המשפטים שלה, ואם היא שלמה, כל משפט (או שלילתו) יצוץ מתישהו. לזה אתה מתכוון? כמובן ש"חילוץ כמתים" (כזה אני) היא שיטה קצת יותר יעילה לעשות זאת. |
|
|
|
|
|
|
||
|
||||
|
ברור, ברור. רק ניסיתי להגיד שתורה (אפקטיבית) לא יכולה להיות שלמה באיזה אופן לא קונסטרוקטיבי. | |
|
|
|
|
|
||
|
||||
|
כמדומני נרמז באחת מהתגובות שגאומטריה היא תורה שלמה (במידה ואני טועה אנא בחר תורה כרצונך, עדיף אחת שאני מכיר, והדגם עליה), איזה אלגוריתם יכול להוכיח/להפריך כל טענה שלי בתחום ? נדמה היה לי במהלך לימודי (נאלצתי לקחת קורס אחת בתאוריה מתמטית, לא היה כל כך נורא) שחלק גדול מהתאוריה היא בלה-בלה ומבוססת על תפיסה של אנשים את הנושא 1, מה שמסביר איך כל השנים עקרון כגון השלישי הנמנע נמנע מלהתגלות, או איך הפרופסור שלי הוכיח משהו שהסתמך על אקסיאומת הבחירה מבלי להזכיר אותה (אחרי שהוא ראה שאף אחד לא שם לב, והיו שם חברה די מבריקים, הוא הסביר את הנושא). כמו כן, אמנם יתכן שיש פה שימוש בתאוריות לא שלמות, אבל משפטים שהוכחו כגון פרמה, הועמדו לביקורת ע"י עשרות מומחים כשכל אחד מקבל חלק קטן לבדוק. במידה והיה אלגוריתם לבדיקה האם הדבר לא היה טכני ומידי ? או שבתאוריות לא שלמות אי אפשר לאמת את המשפטים ע"י אלגוריתם ? 1 - חלילה אין לראות בכך זילזול במתמטיקה ומתמטיקאים, פשוט כמו שאמר אותו בפרופסור בתשובה לשאלה האם פיזיקאים שואלים אותו שאלות : "לא, וגם אם הם היו שואלים הם לא היו מאמינים לתשובה". |
|
|
|
|
|
|
||
|
||||
|
"איזה אלגוריתם" - ברוב המקרים, אין אלגוריתם *פרקטי* לאימות/הפרכה, אם כי בתורות פשוטות מאוד אין קושי למצוא כזה. נדמה לי שבגיאומטריה של המישור זה אכן נעשה: (נסה להתעלם מההומור הגיקי לגבי ספר מהעתיד; שים לב לסעיף Theorems שבו יש הוכחות ממוחשבות למשפטים ידועים בגיאומטריה). "במידה והיה אלגוריתם לבדיקה האם הדבר לא היה טכני ומידי" - כן, *אם* היה כזה, ו*אם* הוא היא רץ בזמן סביר, ו*אם* אנדרו ויילס היה מתאמץ לכתוב את ההוכחה שלו בשפה פורמלית. מתמטיקאים כמעט אף-פעם לא עושים זאת; המטרה שלהם היא לשכנע את עמיתיהם שההוכחה תקפה. עם זאת, התחום של הוכחות ממוחשבות (ובדיקה ממוחשבת של הוכחות) הולך ומתפתח. למשל: ועוד. אם זה מעניין אותך, חפש proof checking בגוגל. יהיה מעניין לראות אם בעוד 50 שנה יתחולל איזה שינוי מהותי בדרך בה מתמטיקאים מוודאים את התגליות שלהם, ומשוחחים עליהן (אני לא בטוח שזה יקרה כל כך מהר, ולא בטוח שזה צריך לקרות). "או שבתאוריות לא שלמות אי אפשר לאמת את המשפטים ע"י אלגוריתם" - בתאוריות לא שלמות אי-אפשר *להוכיח* את *כל* המשפטים ע"י אלגוריתם, אבל ודאי שאפשר *לאמת* הוכחה מוצעת. |
|
|
|
|
|
|
||
|
||||
|
שכחתי לרגע שקיים הבדל בין ''קיים'' לבין ''אני יכול לרשום אותו על פיסת נייר סופית''. | |
|
|
|
|
|
||
|
||||
|
|
|
|
|
|
|
||
|
||||
|
כן, אבל לא כזה שבהכרח תדע מראש כמה זמן יקח לו. האלגוריתם הכללי הוא פשוט לעבור על כל ההוכחות האפשריות אחת אחת ולחפש הוכחה למשפט שלך או לשלילתו. מאחר והתורה שלמה, יש הוכחה כזו ולכן האלגוריתם ימצא אותה ויעצור. | |
|
|
|
|
|
||
|
||||
|
|
|
|
|
|
|
||
|
||||
|
זה לא מפריע לאלגוריתם הכללי, בתנאי שניתן לסדר את האקסיומות בזו אחר זו. גם במקרה זה אפשר לבנות בזה אחר זה את המשפטים היכיחים. כמובן שלא נסיים לעולם את עבודת הבנייה הזו, אבל בהינתן משפט יכיח, נגיע אליו בסופו של דבר. | |
|
|
|
|
|
||
|
||||
|
אני חייב להודות שכנראה שוב לא הבנתי. מצפה להמשך של תגובה 318842 | |
|
|
|
|
|
||
|
||||
|
(ומה זה בכלל "אלגוריתם שמכריע תקפות"? | |
|
|
|
|
|
||
|
||||
|
א. ראה תגובתי לסמיילי. ב. לגבי חיסול כמתים: ננסה לתת דוגמא פשוטה. השפה שלנו תכלול יחס אחד "≤" ואת יחס השיוויון, שבד"כ מתיחסים אליו כחלק מהלוגיקה. התורה שלנו תכלול את האקסיומות שאומרות ש"≤" הוא יחס סדר מלא, שהן לכל a,b,c מתקיים: if a ≤ b and b ≤ a then a = b (antisymmetry) בנוסף ניקח את האקסיומה שהסדר הנ"ל "צפוף":if a ≤ b and b ≤ c then a ≤ c (transitivity) a ≤ b or b ≤ a (totalness) לכל a,b קיים c כך ש: if a≤b and not a=b then a≤c and not a=c and c≤b and not b=c כלומר בין כל שתי נקודות יש נקודה.בנוסף ניקח את האקסיומה שאומרת שאין נקודות קצה: לכל a יש b,c כך ש: b≤a and not b=a and a≤c and not a=c כלומר לכל נקודה יש גדולה ממנה וקטנה ממנה.התורה הנ"ל נקראת תורה של סדר מלא צפוף ללא מקודות קצה. טענה: כל משפט בשפה שקול (תחת התורה הנ"ל) למשפט ללא כמתים. הוכחה, מסקנות ודוגמאות אחרות אח"כ (צריך לצבור כח). |
|
|
|
|
|
|
||
|
||||
|
תודה. אני מצפה להמשך. רק שתי שאלות: מדוע ההסתרבלות עם קטן/שווה במקרים שאתה מדבר על קטן ממש? אתה נמנע בכוונה מהיחס "קטן ממש"? והאם צפיפות איננה תמיד צפיפות "בתוך" משהו? |
|
|
|
|
|
|
||
|
||||
|
1) אפשר להגדיר את הכל עם "קטן ממש" במקום "קטן-שוה". אני לא חושב שזה יצא קצר או פשוט או מובן יותר. 2) בגלל זה כתבתי "צפוף" במרכאות כפולות. פשוט נוהגים לכנות את התכונה הזו כך. |
|
|
|
|
|
|
||
|
||||
|
תודה.:) אני באמת מצפה להמשך, אבל רק אם תהיה לך סבלנות. |
|
|
|
|
|
|
||
|
||||
|
את השויון אתה יכול להגדיר ע"י הפסוק הראשון שלך "(if a ≤ b and b ≤ a then a = b)" ברוח מה שהזכרתי כאן לא מזמן, כך שאינך זקוק לו כחלק מהשפה מלכתחילה. לא? | |
|
|
|
|
|
||
|
||||
|
לא. היית יכול לצרף לשפה יחס, ולסמן אותו בסימן "=", ולציין ש"(if a ≤ b and b ≤ a then a = b)", אבל זה לא היה אומר ששני אובייקטים שיש ביניהם היחס = חייבים להיות באמת שווים במודל המתואר ע"י האקסיומות. "מודל" (כמו שהסברתי באיזה מקום) מאפשר לך לקחת כל סימן-יחס ולהתאים לו יחס כלשהו בין איברי הקבוצה המהווה את המודל. אין כל הגבלה על מה היחס הזה יכול להיות, בתנאי שהוא מקיים את כל האקסיומות בתורה שלך. כלומר, אם נניח שהמודל שלך הוא הנקודות במישור, הסימן "=" יכול היה לציין את היחס "שתי נקודות הן = אםם הן נמצאות באותו גובה", או אפילו "כל שתי נקודות הן = זו לזו". זה לא מה שרצית שהיחס = יציין. עכשיו, יכולת לנסות ולהוסיף אקסיומות לגבי = שהיו "מכריחות" אותו להיות מה שאתה כן רוצה: שני אובייקטים במודל הם שווים רק אם הם אותו אובייקט. למרבה הצער, בשפה מסדר ראשון לא ניתן לעשות זאת. לכן, כפי שאורי הזכיר, מתייחסים לסימן = כאל חלק מהלוגיקה: הוא לא אחד הסימנים שיש לך זכות להתאים להם איזה יחס שאתה רוצה, אלא אחד הסימנים (כמו הסימן "וגם" או "לכל") שהמשמעות שלהם קבועה; בכל מודל של התורה, "=" תמיד מציין שוויון בין איברי המודל. |
|
|
|
|
|
|
||
|
||||
|
אני חושב שהבנתי, תודה. עכשיו אני צריך לחשוב למה זה לא מפריע במקומות אחרים. | |
|
|
|
|
|
||
|
||||
|
רק רציתי להוסיף ששום דבר משמעותי לא היה משתנה אם היינו עובדים עם = בתור יחס רגיל שמקיים את כל האקסיומות הנכונות - שהוא יחס שקילות ושאם a=b אז אפשר להחליף a ב-b בכל מקום שרוצים. היינו נאלצים לשנות קצת את ההגדרות של איזומורפיזם של מודלים אבל לא יותר מזה. | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |