בתשובה לסמיילי, 20/07/05 10:26
 |
|
 |
||
|
||||
 |
א. על השאלה האחרונה יותר קל לי לענות. כדי להוכיח שלמות של תורה, צריך לטפל באיזשהו אופן בכל הנוסחאות בשפה שלה ולהוכיח שהן כריעות. דרך נוחה, יחסית, לעשות זאת היא לפתח תהליך של "פישוט" נוסחאות כאלה: מראים שכל נוסחה שקולה לאחת אחרת בעלת מבנה פשוט יותר, וזאת תוך שימוש באקסיומות של התורה. נדמה לי שהמכשיר החשוב ביותר מסוג זה נקרא "חילוץ כמתים". באופן לא מפתיע, עיקר הקושי בתורות מסדר ראשון נעוץ בכמתים "יש" ו"לכל"; כשיש הרבה מזל, אפשר להראות איך לקחת נוסחה ולהתחיל להעיף ממנה כמתים, וכשיש המון מזל, אפשר להראות שאפשר להישאר בלי כמתים בכלל. המונח הטכני הוא "חילוץ כמתים" (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 מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |