בתשובה לסמיילי, 14/07/05 11:28
 |
|
 |
||
|
||||
 |
פספסת את ההגדרות במאמר, או שהן לא מספיק בעברית פשוטה, או לא מספיק מדוייקות? (ברצינות אני שואל, לא בלעג חלילה). |  |
 |
 |
|
|
|
||
|
||||
|
או-קיי. דרישת האפקטיביות היא פשוטה: מחשב יכול לבחון הוכחה-פורמלית ולהכריע (בלי לטעות) אם היא תקינה או לא. על השאלה "מה זה מחשב" עונים "מכונת-טיורינג", או פשוט: יש תהליך מכני לגמרי, מוגדר היטב וסופי שמקבל רצף של אותיות ואומר "כן, זו אקסיומה" או "לא, זו איננה אקסיומה"; כמו כן, יש תהליך כזה שמקבל סדרה של רצפים כאלה ועונה כן/לא על השאלה "האם הנוסחה האחרונה בסדרה מתקבלת מקודמותיה דרך הפעלה של אחד מכללי ההיקש המותרים". השורה התחתונה של דרישת האפקטיביות היא: אפשר לכתוב תכנית מחשב שתייצר אחד אחד את כל המשפטים שהתורה מוכיחה-פורמלית, ורק אותם. לא משנה כמה זמן זה יקח, ולא משנה אם חלק מהמשפטים יופיעו שוב ושוב בפלט. חשוב שכל משפט ייוצר מתישהוא. דרישת האריתמטיות היא כזו: המערכת הפורמלית צריכה להיות מסוגלת לייצג מספרים טבעיים, ולהוכיח עליהם כמה עובדות בסיסיות. "לייצג מספרים טבעיים" אומר שה*שפה* של המערכת הפורמלית, כלומר הסימנים המותרים בה בשימוש, צריכה להכיל את 0, +, *, > ו-' שזה הסימון ל"עוקב", *או* שהיא תכיל סימנים אחרים המייצגים את הללו באופן אפקטיבי. ב"עוקב" הכוונה "זה שגדול יותר באחד": 0 זה אפס, '0 זה אחת, "0 זה שתיים, וכו'. "להוכיח עליהם כמה עובדות בסיסיות": כאן זה כבר תלוי אם אתה מדבר על המשפט הראשון או השני; השני דורש בהחלט יותר, כלומר יש מערכות שהמשפט הראשון חל עליהן והשני לא. אני לא יודע כמה אתה רוצה להתעמק בדרישות-הממש-מינימליות; לשני המשפטים מספיקות לגמרי האקסיומות של Peano, הנותנות את החוקים הבסיסיים של חיבור וכפל (כמו "X כפול העוקב של Y שווה ל-X כפול Y ועוד X") ואת כלל האינדוקציה (שהוא, למעשה, אינסוף אקסיומות). שוב, אני לא יודע אם חשוב לך שנדבר על המערכות החלשות יותר לגביהן המשפט תקף. מתמטיקאים שאינם לוגיקאים מתייחסים לאקסיומות פאנו ממש כתחתית החבית; הרבה הוכחות מתמטיות דורשות הרבה יותר, ואף אחד באוכלוסיה הזו לא מתאמץ להשתמש בפחות. אם מישהו רוצה לשסות את גדל באיזה תחום לא מתמטי, נניח סוציולוגיה, הוא עשוי לסבור שאת אקסיומות פאנו אולי אין לו אבל משהו חלש יותר כן. במצב כזה הייתי מציג עוד כמה שאלות מקדימות לפני שמבררים אם סוציולוגיה כוללת יותר או פחות מ-Robinson Arithmetic, אבל אם זו הנטייה שלך אני יכול לפרט יותר. אם זה לא הכיוון שרצית לחדד, שאל שוב. |
|
|
|
|
|
|
||
|
||||
|
נדמה לי שההגדרה שלך לאפקטיביות (השורה התחתונה) חלשה מדי; אפקטיביות דורשת כריעות(R), והדרישה שלך היא ל RE. תוכנית המחשב האמורה, תצטרך לדעת לייצר את כל המשפטים בסדר לקסיקוגרפי על מנת לקבל כריעות. | |
|
|
|
|
|
||
|
||||
|
הכריעות היא עבור האקסיומות וכללי ההיסק כלומר הבעיות "האם X אקסיומה" "האם X הוא היסק חוקי" צריכות להיות כריעות (ומכאן נובע גם ש"האם X הוכחה" היא כריעה). אם יש להו את זה אנו מקבלים בקלות שהשפה של כל המשפטים היכיחים בתורה היא RE. משפט גדל אומר שהיא לא R. | |
|
|
|
|
|
||
|
||||
|
אבל למה אתה צריך שלושה שמות? גוראל הוא עברות עתידי לגורביץ' שאתה מריץ בנתיים כפיילוט פה? | |
|
|
|
|
|
||
|
||||
|
גוראל הוא עברות עברי של גורביץ'. | |
|
|
|
|
|
||
|
||||
|
מה שאורי אמר: זו בדיוק הנקודה. הדרישה היא שאוסף המשפטים היכיחים יהיה RE, אחרת המערכת די ממש לא שווה שום דבר. בשביל זה דרוש שנקודת המוצא וכללי המעבר יהיו R. כל הקטע במשפטים של צ'רץ', טיורינג', טרסקי וגדל הוא שה-RE הזה הוא באמת לא R. | |
|
|
|
|
|
||
|
||||
|
האם יש מערכות שלא מכילות את המספרים הטבעיים, ועדיין אפשר לומר עליהן שהן אריתמטיות (אך ורק במובן שהן עונות למשפטי גדל כמו שתוארו למעלה)? אם כן, מהן? מה המכנה המשותף (אם יש כזה) שהופך אותן לכאלה? יש לך דוגמא למערכת כזו? אם לא, יש משפט כזה? (אם השאלה שלי טפשית מכדי להתיחס, אתה יכול להתעלם, אם תשובה תסבך אותך או אותי יותר מידי, אני אוכל להסתפק בהפניה) |
|
|
|
|
|
|
||
|
||||
|
לשאלה הראשונה: לא במובן שאני יכול לחשוב עליו. כאמור, מערכת שעליה משפטי-גדל תקפים צריכה "להכיל" את הטבעיים במובן שתיארתי (לייצג את המספרים, ולהוכיח עליהם כמה עובדות פשוטות). ברור שהיא יכולה לייצג אותם באיזה אופן שונה מהרגיל אבל איזומורפי (סליחה על הביטוי). (למשל מערכת שמדברת על מחרוזות של האותיות ע' ו-פ' כמו עעפעפפעפעפעעפפע, ויש בה פעולות # ו-$ שהן, בעצם, חיבור וכפל בינאריים). אני לא יודע אם יש (או ייתכן) "משפט" כזה; כל מה שיש הוא משפט גדל, והתנאים שהוא דורש, שזה חלק מהם. משפטים שוללניים מטיפוס אחר (כמו אי-הכריעות של בעיית העצירה) אינם דורשים את התנאי הזה, וגם מסקנותיהם אחרות, למרות שהם דומים ברוחם ויש קשרים לוגיים בינם לבין משפטי גדל עצמם. דרך-אגב, השימוש בביטוי "מכילה את הטבעיים" הוא בעייתי קצת. התורה של שדות-סגורים-ממשית מדברת על המספרים הממשיים (ומבנים דומים להם), כולל הפעולות הרגילות של חיבור וכפל. המערכת מאפשרת להוכיח טענות לא טריוויאליות כמו קיום פתרונות לכל מיני סוגים של משוואות פולינומיאליות. המספרים הממשיים כוללים את הטבעיים, אבל משפט גדל לא תקף כאן, כי לא ניתן לבודד את הטבעיים מתוך הממשיים בשפה של התורה הזו. |
|
|
|
|
|
|
||
|
||||
|
מה שאתה אומר זה שמשפט גדל קיים רק במערכות שמכילות את הטבעיים, או שמשפט גדל מוכר רק במערכות שמכילות את הטבעיים? | |
|
|
|
|
|
||
|
||||
|
אני לא בטוח איך לפרש את השאלה: משפט גדל הוא משפט גדל, באיזה מובן הוא יכול להיות קיים במערכת שהוא לא מוכר בה? אתה שואל האם ייתכן שיש משפטים אחרים האומרים גם על מערכות מסוגים אחרים לגמרי שהן לא שלמות? צריך להיזהר פה; המושגים של "שלמות", "עקביות" וכו' מניחים ממילא משהו על המערכות בהן הם דנים (למשל שיש דבר כזה "שלילה" של פסוק). אם מחפשים משפט כללי על מערכות גנריות המייצרות אובייקטים באופן מכני (כמו שמערכת אקסיומטית אפקטיבית מייצרת הוכחות), אני סבור שהדבר הקרוב ביותר היא משפט טיורינג על בעיית העצירה. זה מספיק קרוב בעיניך? אתה חושב על איזשהו סוג ספציפי של מערכות? |
|
|
|
|
|
|
||
|
||||
|
אני לא זוכר את משפט טיורינג. ואין לי אף מערכת ספציפית בראש. אני רק חושב שזה מעניין (אם זה נכון) שיש תורות שיודעים אליהם שאינן שלמות, ויש תורות שיודעים אליהם שהן שלמות. אבל כל התורות מהסוג הראשון איזומורפיות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 מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |