בתשובה לאינקוגניטו, 24/12/09 22:42
 |
|
 |
||
|
||||
 |
אה... רגע, לא הבנתי. מה בין הפוסט שלי לפורמליזם? ועל איזו מכונה דמיונית אתה מדבר? (אם זה לא ברור, אני חושב שהניסוח שהצגתי שם מבהיר הרבה יותר טוב את המושג של "תיאור", גם מבחינת מה הוא אומר על העולם, ממה שנפנופי הידיים הלשוניים יכולים אי פעם לעשות - הכי הפרדוקס הזה הוא עדות לחולשה שלהם). |
 |
 |
 |
|
|
|
||
|
||||
|
משפט לדוגמה "הנחה מהותית ביותר - בלעדיה, אין משמעות פורמלית למילה “תיאור”." כשהילברט חשב על הפורמליזים אזי אחת המטרות השאפתניות שלו היה ליצור מכונה שבצד אחד יהיה משפט מתמטי ואז תסובב מנואלה ובסוף תקבל הוכחה , זה הופרך על ידי טיורינג אבל הרעיון עדיין קסם לפורמליסטים. |
|
|
|
|
|
|
||
|
||||
|
יפה. איך המשפט שלי קשור לפורמליזם? למכונה הדמיונית של הילברט קראו מחשב, והעובדה שהוא חשב עוד לפני המצאת המחשב על כך שהכרחי לבדוק האם ניתן לבצע "פורמליזציה" שכזו למתמטיקה מעידה על הגאונות שלו. במבט לאחור לא הכי מפתיע שפרוייקט *כל כך* שאפתני נכשל, אבל היו חייבים לנסות אותו. מן הסתם זה שהילברט ניסה זאת לא אומר שהילברט לא התעניין במשמעות של המשפטים המתמטיים (זו תהיה הנחה לא מופרכת שהוא הבין את המשמעות לפחות כמו כל מתמטיקאי אחר בן זמנו). |
|
|
|
|
|
|
||
|
||||
|
1)בפוסט שלך אתה פותר (או איך שאתה לא קורא לזה) את הפרדוקס בצורה הבאה: אתה מגדיר באופן פורמלי את המילים שבפרדוקס ואז מגלה שבעצם המספר המתואר בלתי אפשרי. אתה בכלל לא מתיחס למשמעות האמיתית של המילים, אני לא אומר שזה רע באופן ספיציפי אבל זה כן מעיד על פורמליזים. מה גם שמקריאה בפוסט שלך באופן כללי הגישה שלך היא פורמליסטית (והאמת היא שכרגע נזכרתי שכשדיברת על זנון גם גלשת לאינסטרומנטליזם ). 2) להגיד שלמכונה של הילברט קראו מחשב זה אנכרוניזם, בתקופתו של הילברט מחשב היה אדם שמחשב חישובים. האמת היא זה מזכיר לי שבספר "קץ כלזמן" הגיבור הראשי הוא מחשב ולקח לי חצי ספר להבין שהם בעצם מדברים על אדם. |
|
|
|
|
|
|
||
|
||||
|
1) קצת התבלבלת. אני לא אומר ש"המספר המתואר בלתי אפשרי", אלא שהתיאור עצמו הוא בלתי אפשרי. כלומר, שלא ניתן לבצע את הפעולה של תיאור המספר ה"בלתי אפשרי". המסקנה, אם תרצה, היא שמי שמדבר באופן כללי ועמום על "תיאור" בעצם לא אומר כלום - אין משמעות אמיתית לביטוי העמום שלו. אין "משמעות אמיתית", אלא חוסר משמעות. אם כבר, לדעתי הגישה שלי היא זו שמנסה לחפש את "המשמעות האמיתית", ומדברת על מובן מאוד ספציפי וקונקרטי ומחובר למציאות של "תיאור" (תוכנית מחשב פיזית שמבצעת את החישוב פיזית). אפשר כמובן להגיד שאני מקשקש, אבל אני לא חושב שאני מפגין גישה פורמליסטית במיוחד כאן (כלומר, של התייחסות למילים כצורה בלבד ולהתעלם מהתוכן שלהן). 2) האנכרוניזם מכוון, כמובן. |
|
|
|
|
|
|
||
|
||||
|
===>"המסקנה, אם תרצה, היא שמי שמדבר באופן כללי ועמום על "תיאור" בעצם לא אומר כלום - אין משמעות אמיתית לביטוי העמום שלו. אין "משמעות אמיתית", אלא חוסר משמעות. אם כבר, לדעתי הגישה שלי היא זו שמנסה לחפש את "המשמעות האמיתית", ומדברת על מובן מאוד ספציפי וקונקרטי ומחובר למציאות של "תיאור" (תוכנית מחשב פיזית שמבצעת את החישוב פיזית)." לפי דעתי מה שאתה מתאר פה הוא סוג של פורמליזים, אולי זה לא הפורמליזים הקלאסי אבל העובדה שאתה אומר שכדי למצוא "משמעות אמיתית" של ביטויים יש לעשות להם הצרנה היא מאוד בעייתית. כי במעבר לשפה הטבעית לשפת תוכנה אנחנו תמיד מאבדים משהו והעובדה היא שבינתיים אנחנו לא יכולים לעשות בשפת תוכנה מה שאנחנו יכולים לעשות בשפה טבעית כך שאפילו בהסתכלות מתמטית זהו משהו שחבל לאבדו. ===>"אפשר כמובן להגיד שאני מקשקש" אם היית מקשקש לא הייתי מצטט אותך, ובכלל פורמליסטים לא מקשקשים. מה שהם אומרים נכון, הם פשוט מפספסים חלק חשוב במציאות. |
|
|
|
|
|
|
||
|
||||
|
אני אנסה לחדד עוד טיפה את מה שאני טוען שם. אני אומר שלדבר על "תיאור" באופן כללי זה להגיד משהו שהוא פשוט שגוי. כמו שבתורת הקבוצות להתייחס להכל כקבוצה זה פשוט שגויה - כלומר, אתה אמנם יכול לכתוב את המילים "קבוצת כל הקבוצות שאינן מכילות את עצמן", אבל האמירה הזו היא ריקה וחסרת משמעות. אז צריך "לחפש משמעות", ואני באתי והצעתי פירוש אחד אפשרי. לא, חס ושלום, את כל הפירושים האפשריים; אבל פירוש אפשרי אחד. בפירוש האפשרי הזה המצב נהיה עדיף בהרבה על המצב הקודם כי כעת יש הגיון במושג של "תיאור". האם אנחנו מאבדים משהו? רק אם אנחנו מתעקשים מעתה והלאה לדבוק במושג הזה בתור המושג *היחיד* של תיאור, ואת זה אני מן הסתם לא עושה - אני רק מנסה להדגיש שהמושג ה"כללי ביותר" לא אומר הרבה, בעצם, ולכן אם נתעקש לדבוק *בו* אז אנחנו מאבדים משהו. |
|
|
|
|
|
|
||
|
||||
|
האמירה ''קבוצת כל הקבוצות שאינן מכילות את עצמן'' איננה חסרת משמעות. היא מביעה קביעה אינטואיטיבית לגבי קבוצות שהיינו רוצים שהקבוצות יקיימו. העובדה שבצירוף עם עוד הנחות אתה מקבל פרדוקס רק אומרת שהאמירה לא יכולה להתקיים במציאות בצורה נאיבית. עדיין כדי להבין מה זה קבוצה אתה צריך להסתכל על ההסתכלות הכללית. | |
|
|
|
|
|
||
|
||||
|
טוב, נראה לי שהגענו לנקודת אי ההסכמה הפילוסופית. אני חושב שבגישה הזו אתה לא מבין מה זו קבוצה אלא מבין מה זו "קבוצה" - מושג אינטואיטיבי שאין לו פשר ממשי. הזכרת קודם את הפרדוקסים של זנון - גם כאן הבעיה היא זהה, לטעמי - מתלוננים על מושג הסכום של קושי שהוא מלאכותי ופורמליסטי, תוך התעלמות מכך שמושג ה"סכום" האינטואיטיבי הוא חסר פשר. (ואילו עוד הנחות? כל מה שצריך להניח הוא שקיים כזה יצור, "קבוצת כל הקבוצות שאינן מכילות את עצמן", כשהפשר של הכלה הוא שא' או מוכל בב' או לא מוכל בב' אבל לא שניהם). |
|
|
|
|
|
|
||
|
||||
|
המושג שלי הוא אולי אינטואיטיבי אבל בהחלט יש לו פשר. נניח והיינו ממצאים מערכת אקסיומות חדשה אחת השאלות שהיינו שואלים עליה היא האם היא דומה למערכת הקבוצות האמיתית. והענין שזה קרה יש מערכת אקסיומות אלטרנטיבית (או משלימה) לתורת הקבוצות שנקראת תורת האוספים ואחת הסיבות שהיא התקבלה היא כי אינטואיטיבית היא מאוד הגיונית. (עובדה שבמערכת של צרמלו ופרנקל ה''יצור'' הזה קיים והוא פשוט הקבוצה הריקה.) |
|
|
|
|
|
|
||
|
||||
|
(?) | |
|
|
|
|
|
||
|
||||
|
(במערכת האקסיומות של צרמלו פרנקל אין אף קבוצה שמכילה את עצמה בתור איבר לכן קבוצת כל הקבוצות שמכילות את עצמן כאיבר היא הקבוצה הריקה. זה מוכיח שכדי להגיע לפרדוקס צריכים עוד הנחות). |
|
|
|
|
|
|
||
|
||||
|
כזכור, אנחנו מדברים על "קבוצת" כל הקבוצות ש*אינן* מכילות את עצמן. | |
|
|
|
|
|
||
|
||||
|
מה שגדי אמר. | |
|
|
|
|
|
||
|
||||
|
אה זה פשוט, התבססי על המתמטיקה הרומנטית השמה את עדניה על הפסיכולוגיה האנושית אשר איננה מבדילה בין כן ללא. או בקיצור: פדיחה! |
|
|
|
|
|
|
||
|
||||
|
המצאת מושג חדש, והגדרת אותו. מה זה בדיוק עוזר לך שהוא דומה למשהו מ"העולם האמיתי"? לי אישית קשה לדמיין אינטואיטיבית קבוצה אינסופית, אבל מתברר שבעזרת הגרות מתאימות, המושג הזה שימושי למדי. |
|
|
|
|
|
|
||
|
||||
|
כמו שהמטרה העיקרית של המדע היא לתאר את העולם כך (לדעתי) גם אחת המטרות החשובות במתמטיקה היא לתאר את ה''עולם'' המתמטי לכן אני מעונין שמערכת האקסיומות שלי תהיה דומה ככל הניתן לעולם האמיתי. חוץ מזה אני חושב שבעולם האמיתי יש איכויות שאין בשום עולם אחר. לי גם קשה לדמיין מושג כמו אהבה והמילים עוזרות לי בזה. אבל ברור ששום שיר לא יגיע לרמת הבנה שאני מקבל כשאני חווה אהבה. |
|
|
|
|
|
|
||
|
||||
|
גם אני מעוניין שמערכת האקסיומות שלי תהיה דומה ככל הניתן לעולם האמיתי - וזה בדיוק גם מה שהילברט הפורמליסט היה מעוניין בו. הוא רצה מערכת אקסיומות שהיא כל כך טובה, שהיא *בדיוק* העולם האמיתי. | |
|
|
|
|
|
||
|
||||
|
איך יכול להיות שאתה רוצה שמערכת האקסיומות תהיה דומה לעולם האמיתי אם אתה כופר בקיומו (או שלא הבנתי את תגובה 532035) | |
|
|
|
|
|
||
|
||||
|
אני לא כופר בקיומו, אלא שאני חושב שבעולם האמיתי יש הרבה דברים שאפשר לקרוא להם "מערכת הקבוצות האמיתית" ולא ממש ברור במי מהם לבחור (האם נבחר במערכת קבוצות שבה השערת הרצף מתקיימת? או במערכת קבוצות שעבורה היא אינה מתקיימת? ומה עם אקסיומת הבחירה?) המצב בכל הנוגע לקבוצות הוא הרבה פחות חד משמעי מאשר במקרה של המספרים הטבעיים, למשל - כאן אנחנו יכולים לדבר על המודל ה"נכון" של אקסיומות פיאנו (ולנודניקים האחרים שמקיימים את האקסיומות לקרוא "מודלים לא סטנדרטיים"). בקיצור, "העולם האמיתי" הוא דבר מאוד מורכב, עד כדי כך שאפילו עם אקסיומות מסודרות אי אפשר לתאר את כולו באופן פשוט; אז מתמיהה אותי היומרה לנסות ולתאר אותו בלי אקסיומות מסודרות אלא עם נפנופי ידיים בלבד. |
|
|
|
|
|
|
||
|
||||
|
זה שאני לא יודע משהו לא אומר שיש דרגות חופש. לדוגמה אני לא יודע אם בספרד יש ברד או לא אבל אני יודע שאו שכן או שלא. באותה מידה אני לא יודע אם השערת הרצף נכונה או לא אבל אני כן יודע שרק אחת מן האפשרויות נכונה. מה שאומר שאחד מן המודלים משקף את העולם האמיתי והשני הוא סתם מודל. בקשר לאקסיומת הבחירה כאן אני מניח שהיא נכונה, סביר להניח שגם אתה. מה שגדל ניסה להוכיח היה בדיוק זה, שיש דברים בעולם האמיתי שלעולם לא נדע, כי מה לעשות וגם הוא היה אפלטוניסט. |
|
|
|
|
|
|
||
|
||||
|
זה פשוט לא נכון. מה זה אומר "סתם מודל"? מישהו שלא קיים בעולם הפיזי? גם המודל ה"נכון" לא קיים בעולם הפיזי. ב"עולם האמיתי" המתמטי יש הרבה יצורים שונים שמקיימים את אקסיומות תורת הקבוצות, והשאלה היא על מי מהם אנחנו רוצים להדביק את התווית "המודל הנכון". זה לא יהפוך אותו ל"אמיתי" יותר מהשני. גם המודלים הלא סטנדרטיים של אקסיומות פיאנו הם לא "אמיתיים" פחות מהמודל הסטנדרטי של הטבעיים; הטבעיים פשוט יותר מעניינים אותנו. גדל לא ניסה להראות שיש דברים ש"לעולם לא נדע" וגם לא הוכיח שום דבר כזה (אם כבר טיורינג ושות' נותנים תוצאה שהיא יותר ברוח זו), אלא הראה שבמקרה של תורת המספרים ודברים שמכילים אותה, לא יכולה להיות זהות בין מערכת אקסיומות "פשוטה" ובין המודל עצמו - כלומר, יש במודל עוד משהו שהוא מעבר לכל מערכת אקסיומות נתונה עבורו. זה בהחלט דבר טוב עבור פלטוניסט, אבל לא קשור למה שאנחנו מדברים עליו. כדי לחדד את הנקודה: בהינתן טענה מהסוג שמשפט גדל נותן, אנחנו לא יודעים אם היא נכונה או לא *במספרים הטבעיים*, אבל אנחנו יודעים שרק אחת משתי האפשרויות נכונה; אבל אם הטענה נכונה בטבעיים, אז בנוסף לכך קיים מודל לא סטנדרטי של מערכת האקסיומות שלנו שבו הטענה אינה נכונה. לכן אני חוזר לשאלה הבסיסית - איזה מהמודלים אני מעדיף? אבל לקיום של שניהם אני לא יכול להתכחש. |
|
|
|
|
|
|
||
|
||||
|
בוא ניקח את הדוגמה האחרונה שלך נניח שיש לי טענה מהסוג של גדל, נקרא לה טענה A אזי או שהיא נכונה בטבעיים או שלא. אם היא נכונה אזי אקסיומות פיאנו בתוספת עם הטענה ישקפו את הטבעיים בצורה יותר טובה מאקסיומות פיאנו הסטנדרטיות. לעומת זאת אקסיומת פיאנו בתוספת שלילת A יתנו לנו מודל שבו יש משפטים שלא תופסים בטבעיים (לדוגמה שלילת A). עכשיו לשאלה איזה מודל משקף יותר טוב את הטבעיים יש תשובה בינארית, רק הבעיה היא שאני לא יודע מהי. | |
|
|
|
|
|
||
|
||||
|
אני מסכים עם כל מילה שאמרת כאן, ולמעשה זה מה שניסיתי לומר עוד קודם. מה הבעיה? (אולי הבעיה היא בכך שאתה חושב שהמודל-עם-משפטים-שלא-תופסים-בטבעיים הוא "לא מציאותי". כאמור, אני חושב שהוא מציאותי בדיוק כמו הטבעיים, רק פחות מעניין אותנו). |
|
|
|
|
|
|
||
|
||||
|
אז בוא נתקדם לפונקציות על מספרים טבעיים, גם פה אתה חושב שכל משפט נכון או לא נכון על פונקציות של מספרים טבעיים? בפרט האם אתה חושב שהשערת הרצף נכונה או לא נכונה על פונקציות של מספרים טבעיים? ניתן לראות שגם לדעתך נובע ממשפט גדל שיש אלמנט במציאות (A משקף את המספרים הטבעיים) שאנחנו לא יכולים לדעת אם הוא נכון או לא. (מה שגדל ניסה לעשות לא משנה עכשיו). |
|
|
|
|
|
|
||
|
||||
|
מה הכוונה ב"השערת הרצף נכונה על פונקציות של מספרים טבעיים"? אני לא חושב שממשפט גדל נובע שיש אלמנט שאנחנו לא יכולים לדעת אם הוא נכון או לא; משפט גדל מדבר על השאלה אם הוא יכיח או לא ממערכת אקסיומות כלשהי, ובכלל המושג הזה של "לדעת" הוא לא הכי ברור אינטואיטיבית (האם אתה "יודע" שיש אינסוף מספרים ראשוניים? איך אתה יכול להיות בטוח שזה נכון בלי שיוכיחו לך את נכונות האקסיומות? ואיך אפשר לעשות את זה?). כאמור, מה שטיורינג עשה הרבה יותר קרוב להוכחה מדוייקת שיש דברים שאי אפשר "לדעת" - אם נותנים לנו מכונה, לא תמיד נוכל לדעת אם היא עוצרת או לא, וזה לא משנה בכלל מה מנגנון ההכרעה שאנחנו משתמשים בו (כל עוד הוא לא חזק יותר חישוביות ממכונת טיורינג - אבל לך תמצא מנגנון הכרעה סביר בעל תכונה זו). |
|
|
|
|
|
|
||
|
||||
|
אז פונקציות של פונקציות של פונקציות של מספרים טבעיים. תראה יכול להיות שאני טועה ולא לכל מספר יש עוקב, גם יכול להיות שניוטון טעה ודברים עולים למעלה במקום למטה, הכל יכול להיות. אני חושב שהאקסיומות כן נכונות (כלומר משקפות את המספרים הטבעיים) חוץ מזה שאנשים השקיעו הרבה כסף בעובדה שיש אין סוף מספרים טבעיים, שזה גם סוג של הוכחה. |
|
|
|
|
|
|
||
|
||||
|
מה הכוונה ב"השערת הרצף נכונה על פונקציות של פונקציות של מספרים טבעיים"? הנקודה בדברי הייתה שהמושג שלך של "לדעת" הוא בעייתי. זה שיש דברים שאפשר לדעת גם בלי הוכחות ובלי כלום, בעזרת הנסיון היומיומי שלנו, זה ברור (אגב, חלק מהדברים הללו הם שגויים בתכלית). אולי כדאי שנתמקד מחדש בדיון - מה ניסית להגיד בכל עניין הידיעה? כזכור, אני טוען שגם מודל לא-סטנדרטי של הטבעיים עדיין "קיים" במובן המתמטי של המושג, פשוט לא מעניין כמו המודל הסטנדרטי. |
|
|
|
|
|
|
||
|
||||
|
אפשר להגדיר פונקציות אינדיקטור שיחליפו קבוצות, כל פונקציה של פונקציות של מספרים טבעיים היא בעצם פונקציה של קבוצות וכו' בוא נעבור מקיים או נכון למשקף. גם התיאוריה של תלמי קיימת היא פשוט לא משקפת נכון את מערכת השמש. השאלה היא מהו המודל שמשקף את המספרים הטבעיים בצורה הטובה ביותר. |
|
|
|
|
|
|
||
|
||||
|
פעם אחרונה - על מה אתה מדבר כשאתה מדבר על "השערת הרצף" של הפונקציות של הפונקציות של הטבעיים? מה זה אומר בכלל? אם עוברים למשקף הכל אחלה (אם כי אני לא מסכים עם מה שאתה אומר על "המודל שמשקף את המספרים הטבעיים" - המספרים הטבעיים *הם עצמם מודל*), ואז אנחנו חוזרים לבעיה שהצגתי בהתחלה - לא ברור בכלל מה המודל של תורת הקבוצות ש"משקף" נכון את התפיסות האינטואיטיביות שלנו. בוא נעבור לאקסיומת הבחירה בתור דוגמה אחרת. ברור שמודל שבו אקסיומת הבחירה נכונה נראה לנו יותר "נכון" ממודל שבו היא לא נכונה. ברור גם שמודל שבו משפט הסדר הטוב אינו מתקיים נראה לנו יותר "נכון" ממודל שבו הוא כן נכון (המשפט הזה נשמע מאוד, מאוד מוזר, לפחות לי, אינטואיטיבית). לרוע המזל, מודל שבו אקסיומת הבחירה נכונה הוא גם מודל שבו משפט הסדר הטוב מתקיים, ולהפך... |
|
|
|
|
|
|
||
|
||||
|
מכיוון שאני מניח שהבנת מה ה"וכו"' אמר אני קצת לא מבין איפה הבעיה. המספרים הטבעיים הם לא מודל. פיאנו הוא מודל, פיאנו עם A הוא מודל ופיאנו עם שלילת A הוא מודל אחד משני המודלים מכיל סתירה והשני משקף את המודל של פיאנו (ולכן גם את הטבעיים) בצורה יותר מוצלחת. אני חושב שההגדרה שלך לאינטואיטיבי היא קצת שגויה, אתה משתמש באינטואיטיבי במובן "קל לראות" בעוד המובן לדעתי של אינטואיטבי הוא "לאחר שחקרתי עמוק וחקור את השלב האחרון אני עושה באינטואיציה" |
|
|
|
|
|
|
||
|
||||
|
השערת הרצף שאני מכיר אומרת - לא קיימת קבוצה מעוצמה שגדולה ממש מעוצמת הטבעיים, וקטנה ממש מעוצמת הממשיים. אני לא מבין איך עניין הפונקציות רלוונטי פה. פיאנו היא מערכת אקסיומות. דברים שמספקים את מערכת האקסיומות נקראים מודלים. המספרים הטבעיים הם מודל לדוגמה שכזה. אני לא בטוח שאני מבין איך פילוסופיית "השלב האחרון" הזו באה לידי ביטוי בפועל. למשל, בוא נחזור לפרדוקס של ברי - איפה נכנס ה"חקרתי עמוק וחקור" שם, אם אתה דבק בהגדרה המילולית המעורפלת? |
|
|
|
|
|
|
||
|
||||
|
ניתן לנסח את השערת הרצף באמצעות פונקציות (של פונקציות של טבעיים) אתה באמת רוצה שאני אכתוב את זה עד הסוף? או. קי. אזי מבין שתי מערכות האקסיומות (פיאנו עם A ובלי A) אחד מכיל סתירה והשניה משקפת את המספרים הטבעיים בצורה יותר מוצלחת. הפרדוקס של ברי הוא לא כזה פרדוקס מוצלח (עם ברי הסליחה) אני לא חושב שמישהו חוקר אותו ברצינות. יש לעומת זאת היגדים שכן ניתן באמצעות ניחוש מושכל להגיד אם הם נכונים או לא. |
|
|
|
|
|
|
||
|
||||
|
למען האמת, אני לא בטוח שאפשר לנסח אותה כך. נראה לי שהכי טוב אם תפנה אותי לספר טוב שדן בנושא. מה זאת אומרת "מכיל סתירה"? כל הרעיון כאן הוא ש-A לא תלוי באקסיומות, ולכן האקסיומות עם A או עם שלילת A הן בעצמן חסרות סתירה (אם האקסיומות היו מלכתחילה חסרות סתירה, כמובן). אני מסכים שאחת משתי המערכות הללו "משקפת את הטבעיים בצורה יותר מוצלחת"; זה גם מה שאני אומר כל הזמן. להזכירך, כל הדיון כאן התחיל מכך ש"התקוממת" על דרך הטיפול שלי בפרדוקס של ברי (שהייתה בערך כזו "הפרדוקס של ברי הוא לא כזה פרדוקס מוצלח; בואו נראה מה כן אפשר לקבל אם מנסחים בצורה מדוייקת יותר את מה שהוא מדבר עליו"). |
|
|
|
|
|
|
||
|
||||
|
בוא ניקח לדוגמה את השערת גולדבך יתכן שלא ניתן להוכיחה או להפריכה באמצעים שלנו אבל אילו היינו עוברים מספר מספר ובודקים אז או שבסופו של דבר היינו מגיעים להפרכה או שלא. אם לא זה אומר שההשערה נכונה ובפיאנו עם שלילתה יש סתירה. לא התקוממתי, טענתי שאני לא אוהב את הגישה הכללית. |
|
|
|
|
|
|
||
|
||||
|
אני לא מבין מה אתה מנסה לומר עם גולדבך כרגע. אם גולדבך אכן אינה נכונה, אז קיימת לה הפרכה מפיאנו, ולכן פיאנו + "גולדבך נכונה" היא אכן בעלת סתירה, אבל אנחנו בכלל מדברים על מקרים שבהם A לא ניתן להוכחה/הפרכה מהאקסיומות שאליהן מוסיפים אותו. | |
|
|
|
|
|
||
|
||||
|
דיברתי על מקרה שהשערת גולדבך נכונה ולא ניתן להוכיח אותה. | |
|
|
|
|
|
||
|
||||
|
במקרה זה היא לא נובעת מהאקסיומות, ולכן אם נוסיף אותה או את שלילתה לאקסיומות לא נקבל סתירה. | |
|
|
|
|
|
||
|
||||
|
או.קי. זוהי נקודה חשובה ואני שמח שהגענו אליה. למושג סתירה יש שתי משמעויות המשמעות הראשונה היא שאתה לוקח שתי משפטים ובאמצעות החוקים הבסיסיים של הלוגיקה אתה מגיע לסתירה פשוטה (נניח 1=0) המשמעות השניה היא שתי משפטים סותרים. עכשיו ניתן לכתוב תוכנת מחשב די פשוטה שתעבור על כל המספרים ותבדוק האם השערת גולבך נכונה עבורם, אם השערת גולבך שיקרית התוכנה תעצור בשלב מסוים. אם היא לא תעצור זה אומר שהשערת גולדבך נכונה ושלילתה יחד עם פיאנו היא מובילה לסתירה. |
|
|
|
|
|
|
||
|
||||
|
אם היא לא תעצור תוך כמה זמן? | |
|
|
|
|
|
||
|
||||
|
אם המחשב שלך מהיר, אז תוך אינסוף. אם הוא איטי זה יקח קצת יותר זמן. | |
|
|
|
|
|
||
|
||||
|
עד שיהיה עדכון חלונות ותצטרך לעשות ריסטארט. | |
|
|
|
|
|
||
|
||||
|
אני לא רואה שום הבדל בין שתי המשמעויות שלך (אם כי לא ברור לי מה כוונתך ב-"שני משפטים סותרים" - בעיני פשוט מדובר בשני משפטים שאם נוסיף אותם למערכת האקסיומות שלנו, נוכל להוכיח ממנה דבר והיפוכו גם אם קודם לא יכלנו). את מה שאתה מנסה לומר בעניין התוכנה אני לא מבין - התוכנה לא מחוייבת לעצור, ואם היא לא עוצרת לא בהכרח נוכל לדעת את זה. סתירה תוכל להיות רק אם אקסיומות פיאנו יוכלו *להוכיח* שהתוכנית לא תעצור אף פעם; ובמקרה זה, אקסיומות פיאנו *הוכיחו* שהשערת גולדבך נכונה, ולכן ברור שהוספת שלילת השערת גולדבך לאקסיומות תניב סתירה. | |
|
|
|
|
|
||
|
||||
|
בוא נניח שהמכונה לא עוצרת אזי המשפט ''המכונה עוצרת'' הוא שקרי. השאלה אם אנחנו יודעים את זה או אם אנחנו יכולים להוכיח את זה היא שאלה אחרת. | |
|
|
|
|
|
||
|
||||
|
הוא שקרי - איפה? במודל של המספרים הטבעיים הוא כמובן שקרי, אבל זה אותו הדבר כמו שהמשפט "השערת גולדבך שגויה" הוא שקרי. במודל הלא-סטנדרטי של הטבעים הוא דווקא אמיתי - זה מעיד על החולשה של השפה שלך, שלא באמת מסוגלת להבדיל בין המודל הסטנדרטי והמודל הלא סטנדרטי. | |
|
|
|
|
|
||
|
||||
|
איך חזרנו למודלים? הרי את התוכנית הייתי יכול לכתוב בruby שפועלת על קובנטו ולחבר את המחשב לפעמון שיצלצל כשהיא מסיימת. אם השערת גולדך שגויה הפעמון לא יצלצל. איך זה קשור למודל לא סטנדרטי? |
|
|
|
|
|
|
||
|
||||
|
אם השערת גולדבך נכונה הפעמון לא יצלצל, אבל מתי אני אוכל להגיד למחשב "טוב, תפסיק, שוכנעתי"? אף פעם לא. אז איך תוכנית הרובי שלי קידמה אותי? | |
|
|
|
|
|
||
|
||||
|
אף פעם לא תשתכנע. אבל זאת לא הנקודה, הנקודה היא שהמשפט ''הפעמון יצלצל'' הוא שיקרי. וזה לא קשור לא לאקסיומות ולא למודלים. | |
|
|
|
|
|
||
|
||||
|
מה שאתה מפספס כאן הוא שאת המשפט הזה צריך לנסח פורמלית בשפה של מערכת ההוכחה שלנו, אחרת לא אמרת שום דבר... בוא ננסה לעשות שוב סדר בדברים. מה בעצם הטענה שאתה מנסה לקדם עם כל עניין הפעמון הזה? |
|
|
|
|
|
|
||
|
||||
|
יכול להיות שאני מפספס משהו, אבל מכיוון שזה בערך הנושא העיקרי שאנחנו דנים עליו בכל זאת אני מצפה לאיזה הסבר. אני בכל מקרה לא מבין למה צריך לנסח פורמלית את העובדה שהפעמון יצלצל, יש איזשהו גבול לדברים שצריך פורמליסטיקה בשבילם, ולהגיד אם פעמון יצלצל או לא זה מספיק פשוט בשביל שאני לא אצטרך פורמליסטיקה. והטענה היא פשוטה: אם מניחים את אקסיומת פיאנו ושהשערת גולדבלך נכונה אזי אקסיומת פיאנו בתוספת שלילת השערת גולדבלך תוביל אותנו לסתירה. |
|
|
|
|
|
|
||
|
||||
|
סליחה שאני מתערב, אבל לא הבנתי את הטענה שלך. הנכונה במשפט - "אם מניחים את אקסיומת פיאנו ושהשערת גולדבלך נכונה" אומר: 1. "נובעת לוגית מאקסיומות פיאנו". 2. "אקסיומה בפני עצמה". 3. "מתקיימת עבור כל המספרים הטבעיים אבל לא לא ניתנת להוכחה לוגית על ידי אקסיומות פיאנו". 4. "מתקיימת עבור מערכות פיזיות שניתנות לתיאור על ידי מערכת שמקיימת את אקסיומות פיאנו" 5. "משהו אחר". |
|
|
|
|
|
|
||
|
||||
|
האפשרות הרביעית. והדוגמה עם rubby והפעמון היא בדיוק אותה מערכת פיזית. | |
|
|
|
|
|
||
|
||||
|
נראה לי שאתה וגדי מדברים על דברים שונים לגמרי. בכל מקרה, סליחה שהתערבתי. | |
|
|
|
|
|
||
|
||||
|
להפך, טוב שהתערבת. | |
|
|
|
|
|
||
|
||||
|
אני כמעט מסוגל לענות על השאלה שלך (האמת, אני חושב שכבר עניתי קודם, אבל ננסה שוב) - רק תגיד לי את כוונתך המדוייקת ב"סתירה". (ואני אסביר: "סתירה" כפי שאני מכיר אותו הוא מושג פורמליסטי. פירושו שמערכת ההוכחה מסוגלת להוכיח דבר ואת שלילתו. לכן מראש אנחנו מוגבלים לדבר על טענות שניתנות לניסוח במסגרת השפה של המערכת). |
|
|
|
|
|
|
||
|
||||
|
בהמשך לתגובה שלי לאלמוני הכוונה היא שהמערכת הפיזית מתנהגת שונה מהתחזיות. | |
|
|
|
|
|
||
|
||||
|
לא ראיתי שמישהו חזה תחזיות. נראה לי שהאלמוני צודק. אני אמנם חושב שאני מבין על מה אתה מדבר, אבל בד בבד גם חושב שזה לחלוטין לא קשור לכל מה שדיברנו עליו עד כה. אולי עדיף לסיים את הדיון כאן, או לאפס אותו ולהבהיר יותר במדוייק מה אנחנו מנסים לומר. |
|
|
|
|
|
|
||
|
||||
|
אני חזיתי שהפעמון יצלצל. ואם אתה מבין מה אני אומר אולי גם תסביר איפה בעצם הבעיה, ולמה אנחנו חייבים פורמליסטיקה. |
|
|
|
|
|
|
||
|
||||
|
אמרתי שאני חושב שאני מבין על מה אתה מדבר, לא שאני מבין מה אתה בעצם מנסה לטעון. לכן הצעתי שנאפס את הדיון - כבר מזמן לא ברור לי מה הנקודה שלך. (הנקודות שלי בכל הדיון: 1) הגדרות "אינטואיטיבות" לא משפרות את ההבנה שלנו את העולם אלא מקשות עליה; 2) המושג של "קיים" במתמטיקה הוא מורכב יותר משהאינטואיציה רומזת - כך למשל קיים מודל לתורת הקבוצות עם השערת הרצף ומודל לתורת הקבוצות עם שלילת השערת הרצף ושניהם לגיטימיים). |
|
|
|
|
|
|
||
|
||||
|
האמת היא שבדרך כלל הייתי פורש מדיון כזה כבר מזמן, אתה העלת את הנקודות שלך, אני העלתי את שלי, יקרא הקורא הנבון וישפוט. אבל פה נראה לי שיש פער בינינו שאני (ונראה לי שגם אתה) באמת מנסים לגשר עליו, ואני חושב שאם באמת נצליח להבין איפה הבעיה הדיון יתקדם. אבל אם נראה לך שאנחנו טוחנים מיים אפשר לסיים פה. |
|
|
|
|
|
|
||
|
||||
|
אני שוב אומר - אני פשוט לא מבין מה הטענה שלך. אם תגיד אותה, אולי יהיה על מה לדבר. | |
|
|
|
|
|
||
|
||||
|
טענתי היא בפשטות שבהינתן אוסף אקסיומות יש דברים שהם נכונים לגביהים למרות שלא ניתן להוכיח אותם בצורה צורנית. לדוגמה אם יש לי שתי פונקציות (במחשב): אחת שאומרת אם מספר אחד גדול מהשני והשניה שלוקחת מספר ומוסיפה לו אחד אני לא צריך את הנחת האינדוקציה כדי להבין שלכל מספר n+1>n. |
|
|
|
|
|
|
||
|
||||
|
כדי להראות שלא צריך את הנחת האינדוקציה, צריך גם להראות שלא השתמשת בה גם באופן סמוי. איך בדיוק הצלחת לבנות פונקציה שמוסיפה 1 לכל מספר נתון? בתור התחלה: מהו בדיוק מודל החישוב שלך? מחשב רגיל? אם אני אקח מספר מספיק גדול, הוא לא ייכנס בזכרון של המחשב. |
|
|
|
|
|
|
||
|
||||
|
אפשרות ראשונה n++ (או המקבילה בrubby) אפשרות שניה באמצעות פורים על הקלט. אתה יודע מה אני אסתפק במספרים שנכנסים בMB זיכרון. אם תצליח להוכיח את המשפט על קלטים כאלה בלי להשתמש בהנחת האינדוקציה אתה כנראה אדם הרבה יותר משועמם ממה שתיארתי לעצמי. |
|
|
|
|
|
|
||
|
||||
|
א. לשפה קוראים רובי, ובאנגלית Ruby. תוכל למצוא פרטים נוספים ב: http://www.ruby-lang.org/ ר' גם http://tryruby.org/ . למזלך הגדרתה (או לפחות המימוש הסטנדרטי שלה) לא סובלת מ־overflow של מספרים. בהרבה שפות מחשבים מקובלות, היית נופל כבר כאן. ב. פעולת ה־++ של רובי לוקחת צירוף ביטים מסויים שאמור לייצג את n ומחזירה צירוף ביטים מסויים שאמור לייצג את n+1. אתה בטוח שהפעולה כתובה נכון? תדע להבחין בין תוכנה דומה לתוכנה שמדי פעם (לא מגלה לך את התדירות) מכניסה שגיאה? ג. אם אתה מגביל את עצמך רק למספרים שנכנסים בזכרון של המחשב מהדור הנוכחי, הרי ש"ההוכחה" שלך לא תהיה תקפה עבור המחשבים של השנה הבאה (ועבור המחשבים החזקים הרבה יותר שנמצאים כבר היום במקומות שוננים). נראה לי מאוד לא משכנע. ד. עכשיו נסה לשכנע אותי שלכל מספר יש ריבוע. פתאום הגבול של הזכרון משמעותי בהרבה. לא הצלחת לשכנע שלכל מספר יש ריבוע? חבל, יש חלקים מעניינים ושימושיים למדי במתמטיקה שמסתמכים על כך. ה. צודק, אני משועמם. אתה לא משועמם? |
|
|
|
|
|
|
||
|
||||
|
ב. למעשה, ברובי אין פעולת ++. ועכשיו שברתי את שיא הנטפוק האיילי של כל הזמנים. |
|
|
|
|
|
|
||
|
||||
|
א. תודה ב. מעולם לא ראיתי איך תוכנת רובי כתובה, אני משער שאם היא לא כתובה יותר מדי מוזר אני אדע להגיד אם היא נכונה וגם אם לא, לא מדובר שקשה מדי לכתוב גם באסמבלר. ג. בסדר, זה לא כאילו ההוכחה הזאת באמת חשובה ( אני מניח שאתה לומד שn+1>n בתואר השני או משהו כזה). ד. גם ההוכחה הרגילה שלכל מספר יש ריבוע היא די מסובכת אבל זה לא הענין. ה. לנהל ויכוחים לא נגמרים עם תש"חיסט? כן. להוכיח שn+1>n בלי להשתמש בהנחת האינדוקציה? זה לא. גם לי יש גבולות. |
|
|
|
|
|
|
||
|
||||
|
ב. לא נכון. לא ידוע אלגוריתם כללי לבדיקת נכונות של תוכנית (ניטפוק קטן: מכיוון שכמות הזכרון במודל ה"מוגבל" שלנו מוגבלת, יש בעיקרון אפשרות לעבור על כל המצבים האפשריים. אולם זה ייקח המון זמן, ולא נראה לי שתזכה לסיים בדיקה אחת כזו בחייך. וגם אם היית מסיים, מספיק היה לי להוסיף למחשב תא זכרון אחד כדי לסבך לך שוב מחדש את החיים). אתה מאמין למה שכתבתי כאן? ג. (וכל השאר) מה שלא ברור לי הוא מה שיש לך נגד הפורמליזם. הניטפוקים שלי מתבססים על־כך שאתה מסרב להעזר גם גם במקומות שהוא מועיל. אני לא רוצה תוכנית ש"עובדת במספרים קטנים בלבד", או ש"עובדת בהסתברות גבוהה"1. אני רוצה תוכנית שעובדת. 1 ליתר דיוק, תוכנית שלפעמים צודקת, בהסתברות ידועה, עדיפה על כלום, ויש גם לה שימושים. אבל זה מחייב יתר מאמץ וזהירות. אבל זה שוב עוד ניטפוק מיותר. |
|
|
|
|
|
|
||
|
||||
|
א.לא טענתי שיש לי אלגוריתם, טענתי שאני אדע. וכן אני מאמין. ג. זה לא נכון שאני מסרב להיעזר בפורמליזם, מכיוון שאני לא איש תורת הקבוצות כל מה שאני עושה הוא פורמלי (זאת אומרת בתיאוריה) אני מתנגד להיגד כאילו הדבר היחידי שיש לי הוא משפטים וגרירות. יש דברים שהם נכונים בלי קשר למשפטים. |
|
|
|
|
|
|
||
|
||||
|
א. אם מסקירה של תוכנית תדע האם היא נכונה או לא, נראה לי שיכולותיך עוברות בהרבה את תוכניתן הממוצע. או ליתר דיוק: לא ברור לי אם קיים תוכניתן שיכול להשתוות לך. אפילו האדמו"ר דונלד קנות' [ויקיפדיה] שלימד אותנו שתוכנית מדבגים בסבלנות עם נייר ועפרון. בתור התחלה, אתה מוזמן לעזור לפתור בעיות פתוחות במימוש הסטנדרטי של רובי: ג. משפטים פורמליים אינם הדבר היחיד בעולם. חשוב מאוד לדעת ליישם אותם בתבונה בעולם האמיתי. בהתחשב בחישובים המסובכים שמחשבים עושים יום־יום (ולו כדי לכתוב את ההודעה הזו) נוח לי מאוד להסתמך על משפטים פורמליים במקרה הצורך. בינתיים הצלחת להעלות לא מעט טענות שנראו לך נכונות והתבררו כשגויות. אולי יש משהו בפורמליזם. |
|
|
|
|
|
|
||
|
||||
|
א. לא כל תכנית, אבל את היישום של פלוס 1 אני כנראה אצליח לזהות. וחוץ מזה מדובר בבערך שלוש שורות באסמבל כך שאפילו אני יכול לכתוב את זה. ג. גם לי נוח להסתמך על משפטים פורמליים, זה לא סותר את מה שאמרתי. |
|
|
|
|
|
|
||
|
||||
|
א. זה רק מוריד את השאלה לרמת הפשטה נמוכה יותר. אתה מניח שהמימוש של המעבד נכון. אתה חושב שאתה מסוגל להבדיל בין שתי מכונות וירטואליות שבאחת מהן יש באג קטן המימוש של אותו קוד אסמבלי לבין מכונה אחרת שבה אין באג כזה? (בלי לדעת מראש מה שגוי). | |
|
|
|
|
|
||
|
||||
|
לא, אני לא יכול. מצד שני אני לא מבין מה הנקודה שלך. אתה יודע כמה מאמרים יש שכל החישובים הסטטיסטיים נעשו על ידי מחשב? ומתוכם כמה נעשו על ידי אנשים ששפת התכנות היחידה שהם מכירים זה spss ? גם הם לא יכולים להבדיל בין קוד נכון לשגוי, אז מה? |
|
|
|
|
|
|
||
|
||||
|
הם מקווים לטוב. אבל אתה לא הצלחת לשכנע אותי בטענות מתגובה 532220. לא הצלחת לשכנע אותי שאתה יכול לספק לי הוכחה (ההוכחה שהצגת לא עובדת על מספרים גדולים מספיק). לא הצלחת להראות לי שהיא לא מסתמכת על אקסיומת האינדוקציה (גם לא ממש ניסחת את הטענה הזו בקפדנות). הבעיה היא שהיית מצליח לספק לי את אותה הוכחה שאמורה להיות משכנעת גם כאשר היא אינה נכונה. כדי שהיא תהיה נכונה, על כל n המחשב אמור להוציא לך בחישוב ערך גדול מ־n. אם אתכנת את המחשב לשקר, זה לא יעבוד. לדוגמה: אם אני יודע מראש שתבדוק רק מליון מספרים, אני אתכנת את המעבד שאני בונה לשקר לך (לחסר 1 מ־n במקום להגדיל ב־1) בבדיקה המליון ועוד אחד. לחילופין, אני יכול לתכנת את המעבד לשקר לך במקום אקראי, ואז קיים סיכוי1 שתחשוב שהמחשב מאשש את טענתך, למרות שהוא לא. אבל יש גם דרך יותר פשוטה: אני אפעיל את האלגוריתם הבא: א. בקש מאינקוגניטו להראות את נכונות הטענה לגבי x ב. טען: "ההוכחה לגבי המספרים עד x לא מספיקה לי - לא בדקת שהמחשב מחשבר נכון גם את הערך x+1". ג. הגדל את x ב־1 ד. חזור ל־א' אני מניח שקוראי האייל מכירים היטב טכניקות דומות. 1 אם כי במקרה הזה הסיכוי יכול להיות זניח למדי, אם לא נזהרים עם הפרמטרים) |
|
|
|
|
|
|
||
|
||||
|
וואו כתבתי שתי שורות, והצלחת להבין אותי הפוך לחלוטין, כנראה שאני באמת מוכשר. לא כתבתי שיש לי הוכחה או שאני יכול למצוא אחת. אמרתי שאני *מבין* ש n+1>n. כל הנקודה שלי היא שיש דברים שאני יודע שהם נכונים גם בלי הוכחות. |
|
|
|
|
|
|
||
|
||||
|
זה לא נכון תמיד בשעון שלי. הבעיה היא שמתמטיקה (גם המעשית) זימנה לנו לא מעט תוצאות לא אינטואיטיביות. לדוגמה: הצפנה אסימטרית, נחשבה עד לשנות השבעים למשהו לא הגיוני. |
|
|
|
|
|
|
||
|
||||
|
הכוונה בפונקציות שמוגדרות כמו שצריך. ושוב האינטואיציה היא מעבר לפורמליסטיקה ומובן שניתן לטעות, זה לא סיבה לוותר עליה. |
|
|
|
|
|
|
||
|
||||
|
א. סתם בשביל הכיף, הנה שפה שלא יודעת לקדם מספרים כמו שצריך (או שמא תוכניתן שלא יודע לכתוב קוד כמו שצריך) #include <stdio.h> הפלט:int main() { float f; for (f=0; ; f++) { printf("%f\n", f); } return 0; } 0.000000 1.000000 2.000000 ... 16777214.000000 16777215.000000 16777216.000000 16777216.000000 16777216.000000 (וישאר תקוע על הערך הזה) לפרטים נוספים: |
|
|
|
|
|
|
||
|
||||
|
מה זה "נכון לגבי אקסיומות"? אם אנחנו מדברים על מערכת אקסיומות בלוגיקה מסדר ראשון (כמו אקסיומות פיאנו, בניסוח המקובל שלהן) ואם "נכון לגבי אקסיומות" פירושו "מתקיים בכל מודל של האקסיומות", אז הטענה שלך פשוט שגויה (משפט השלמות של גדל מראה שכל טענה נכונה היא יכיחה במערכת שכזו). לכן נשאלת השאלה איפה נקודת המחלוקת שלנו - לדעתי ברור שהיא במשמעות שאתה מייחס ל"נכון לגבי אקסיומות". עד כמה שאני מבין אותך, אתה טוען ש"נכון לגבי אקסיומות" אין פירושו "נכון בכל מודל של האקסיומות" אלא "נכון במודל הספציפי של האקסיומות שאנחנו אוהבים, ושיזדיינו המודלים האחרים". עד כאן אני מדייק? |
|
|
|
|
|
|
||
|
||||
|
לא, אתה לא מדייק. נכון לגבי האקסיומות אכן פירושו נכון בכל מודל של האקסיומות. ומשפט גדל לא אומר שכל טענה נכונה היא יכיחה (אלא אם כן יש לך הגדרה שונה משלי לנכונה). בוא נסתכל (מאוד מאוד בכללי) על ההוכחה של גדל. מה שגדל עשה הוא לקודד משפטים בפרט הוא קודד את המשפט ''משפט זה לא יכיח תחת האקסיומות של גדל''. עכשיו אם המשפט יכיח אז הוא נכון ולכן הוא לא יכיח. אז הנה משפט נכון ולא יכיח. |
|
|
|
|
|
|
||
|
||||
|
אל תתבלבל בין משפט השלמות של גדל ומשפט אי השלמות של גדל. אלו שני משפטים שונים, ואפילו המשמעות של "שלמות" שונה. משפט השלמות מדבר על שלמות במובן של "כל מה שנכון ניתן להוכחה", ומשפט אי השלמות מדבר על שלמות במובן של "כל מה שניתן לניסוח ניתן להוכחה או ששלילתו ניתנת להוכחה". זה לא אותו דבר. מה שמשפט אי השלמות של גדל מראה הוא שעבור מערכות אקסיומות מסויימות קיימים תמיד שני מודלים שונים מהותית ביחס למשפט שניתן לנסח באמצעות השפה של המערכת. בפרט, המשפט שגדל בונה הוא נכון במודל אחד, ולא נכון במודל אחר (חשוב להבין שהמשפט של גדל לא אומר טענה כמו זו שציטטת באופן מפורש; הוא אומר משהו על מספרים, ולכן הפרשנות המדוייקת של מה שהוא אומר תלויה במודל שבו הטענה מפורשת ובהתנהגות של "מספרים" בתוך אותו מודל). |
|
|
|
|
|
|
||
|
||||
|
אם לקשר (באופו רופף ) לנושא המרכזי אז ויקיפדיה איתי משפט אי השלמות של גדל [ויקיפדיה] משפט רלוונטי (שמופיע כבר בהתחלה)."גדל הראה שבכל מערכת אקסיומות סופית ועשירה מספיק (כזו המכילה את אקסיומות האריתמטיקה החלשה) קיימות טענות אמיתיות שלא ניתן להוכיחן." | |
|
|
|
|
|
||
|
||||
|
לדעתי ויקיפדיה מתנסחת גרוע בנקודה הזו. "אמיתי" בהקשר הזה הוא "אמיתי במודל שמעניין אותנו", כשההנחה היא שתמיד עומד לנגד עינינו כזה (למשל, במקרה של פיאנו - המספרים הטבעיים). המשמעות בפירוש אינה "נכון בכל המודלים". אם אתה מתעקש להביא את ויקיפדיה העברית כמקור, אז בערך משפט השלמות של גדל [ויקיפדיה] יש התייחסות לכך: "גרסה פופולרית (ושגויה) של משפט אי השלמות הראשון של גדל קובעת ש"בכל תורה קיימת טענה אמיתית שאינה ניתנת להוכחה". משפט השלמות סותר במפורש את הניסוח הזה: כל משפט שהוא אמיתי (בכל מודל), ניתן להוכחה. אכן, לפי משפט אי השלמות קיימת בתורה (חזקה מספיק, דהיינו אריתמטית, אפקטיבית ועקבית) נוסחה שאינה ניתנת להוכחה (וגם לא לסתירה) - אבל אין זה נכון שנוסחה זו נכונה בכל מודל. אדרבא, לפי משפט השלמות, קיים מודל עקבי שבו היא נכונה, וקיים מודל עקבי שבו היא אינה נכונה." דיון קצת יותר חפרני בכל עניין האמת יש בספר המוצלח של Torkel Franzen על משפטי גדל (עמ' 28 והלאה). |
|
|
|
|
|
|
||
|
||||
|
הבנתי איפה הבלבול. משפט השלמות של גדל מדבר על משפטים מסדר ראשון, לעומת זאת פיאנו היא מסדר שני . תסתכל על האקסיומה השלישית במערכת פאנו [ויקיפדיה] ותראה שהיא מסדר שני. ואם תחשוב על זה קצת תראה שזה הכרחי. | |
|
|
|
|
|
||
|
||||
|
הבלבול לא כאן. פיאנו מנוסחת לרוב בסדר ראשון, כשאת אקסיומת האינדוקציה הבודדת מחליפה "תבנית אקסיומה" כללית - ומשפט אי השלמות של גדל חל גם על המערכת הזו. שוב, אם אתה מתעקש על ויקיפדיה, תעיף מבט באנגלית, בפרט בפרק של "First-order theory of arithmetic". | |
|
|
|
|
|
||
|
||||
|
"תבנית אקסיומה" היא פחות חזקה מהנחת האינדוקציה, או במילותיה של הויקיפדיה For instance, it is not possible in first-order logic to say that any set of natural numbers containing 0 and closed under successor is the entire set of natural numbers. What can be expressed is that any definable set of natural numbers has this property ואם יש לך הוכחה של משפט אי השלמות של גדל שמנוסחת בסדר ראשון אני אשמח לראות. |
|
|
|
|
|
|
||
|
||||
|
בוודאי ששפה מסדר שני היא יותר אקספרסיבית משפה מסדר ראשון. זה לא משנה את זה שכשמדברים על פיאנו, לרוב הכוונה דווקא לאקסיומות המנוסחות בסדר ראשון... בנוגע לרפרנסים - הספר הסטנדרטי וה"יבש" שעוסק בלוגיקה הוא של מנדלסון: אם כל מה שאתה רוצה הוא להשתכנע שמשפט גדל אכן תקף גם לפיאנו-מסדר-ראשון, פרנזן אומר זאת במפורש בספרו: "Two first-order theories prominent in logic to which the incompleteness theorem applies are Peano Arithmetic, or PA, which is a formal theory of elementary arithmetic, and Zermelo-Fraenkel set theory with the axiom of choice, ZFC."
|
|
|
|
|
|
|
||
|
||||
|
1) מאוד מפתיע אותי שיש אוסף אקסיומות שלגביהים גם משפט השלמות וגם משפט האי שלמות תופסים, הענין דורש בדיקה מקיפה, אל תעצור את הנשימה אבל אני הולך לברר את הענין, מילניום שניים ואני מבין מה קורה. 2) בוא נסכים שאנחנו מדברים על מתמטיקה סטנדרטית, אז אוסף אקסיומות זה משפטים בשפה הכוללת סימנים לוגיים, משתנים קבועים ופונקציות ומודל הוא קבוצה המקיימת את האקסיומות. משפט מאוד בסיסי במתמטיקה (שמופיע גם בויקיפדיה) אומר שאם יש לך שתי קבוצות בכל קבוצה יש לך איבר ופונקציה ושניהים מקיימים את אקסיומת פאנו אזי יש ביניהים איזומורפיזים ולכן כל משפט לוגי שנכון לאחד נכון לשני ולהיפך לכן בפרט אם ניקח שני מודלים שמקיימים את פאנו ואחד מהם מקיים את השערת גולדבך אז גם השני מקיים אותה. |
|
|
|
|
|
|
||
|
||||
|
1) אני לא מבין מה ההפתעה הגדולה. כבר ציטטתי לך את הקטע המתאים מויקיפדיה שמתייחס ל"בעייתיות" ומסביר למה לא קיימת כזו. 2) אני לא מכיר את המשפט הבסיסי במתמטיקה המדובר. לינק? שים לב שקיים גם משפט חביב בשם לוונהיים-סקולם שממנו עולה שאם יש לך מודל בן מניה לשפה נחמדה מסדר ראשון, אז יש לך מודל מכל עוצמה אינסופית עבור השפה הזו (ומן הסתם מודלים מעוצמות שונות אינם איזומורפיים). אולי בשלב הזה מותר לשאול מה ההשכלה שלך בנושאים שעליהם אנחנו מדברים כאן ומהיכן היא הגיעה? |
|
|
|
|
|
|
||
|
||||
|
1) טוב מה אני אגיד, אני חולק על ויקיפדיה. מקוה שזה חוקי. 2)מערכת פאנו [ויקיפדיה] בסעיף "מודלים". ומשפט לוונהיים-סקולם מדבר על שפות מסדר ראשון ולכן לא תקף למערכת פאנו. אני מתמאטיקאי ואחד המאמרים שלי עוסק בנושא קרוב. |
|
|
|
|
|
|
||
|
||||
|
1) בוודאי שזה חוקי, אלא שכאן לא מדובר במשהו שרק ויקיפדיה טוענים. 2) אחזור שוב על מה שכבר אמרתי: אני מדבר כאן כל הזמן על הניסוח של פיאנו בלוגיקה מסדר ראשון (שעבורו תכונת הקטגוריות איננה מתקיימת). 3) להגיד שאתה מתמטיקאי לא עונה ממש על השאלה שלי. תשובה טובה תהיה למשל מספר ספרים/מאמרים על הנושא שעליהם אתה מתבסס. |
|
|
|
|
|
|
||
|
||||
|
2) אתה טענת שאם לא קיימת הוכחה להשערת גולדבך אזי קיימים שתי מודלים למספרים הטבעיים שאחד מקיים את השערת גולדבך והשני לא. נניח שאנחנו מדברים על מודלים שמקיימים פאנו, מה אתה טוען? 3) מהפשוטים יש את הספר של האוניברסיטה המשודרת על גדל שאומר במפורש שלפי גדל יש משפטים נכונים שלא ניתן להוכיחם. חוץ מזה יש ספרים קלאסיים על לוגיקה מתמטית שאני לא זוכר עכשיו במדויק את שמותיהים וגם אי אפשר לצטט אותם כי כל משפט שלהם חצי מהמשפט זה סימונים שהם הגדירו קודם. |
|
|
|
|
|
|
||
|
||||
|
טוב, אני חושב שזה זמן טוב לסיים בו. עם כל הכבוד לספר של ארנון אברון (ויש כבוד - ספר מעולה מסוגו), נראה לי שלהזכיר רק אותו במפורש זה לא רציני, ואני מקבל את התחושה שגם המשך הדיון יהיה טחינת מים. | |
|
|
|
|
|
||
|
||||
|
טוב, נראה לי שהבנתי מה קורא פה והייתי רוצה לתמצת את המסקנות, כמובן שכל אחד שחושב שאין טעם להתייחס למישהו שמצטט את אברון, מוזמן לא לקרוא. 1) מעכשיו נשתמש בהגדרות של גדי (שהם עצם ההדרות הבסיסיות של הלוגיקה המתימטית) אז שפה זה אוסף של סימנים המייצגים קבועים, יחסים ופונקציות. משפטים הם משפטים לוגיים ומודל היא קבוצה שבה הקבועים המשתנים והפונקציות נקבעים. 2) משפט השלמות של גדל טוען שאם יש לנו שתי קבוצות בנות מניה של משפטים מסדר ראשון ולא ניתן להוכיח או להפריך שהקבוצה הראשונה גוררת את השנייה אזי קיימים שתי מודלים אחד שבו הקבוצה הראשונה מקיימת והשנייה לא והשני שבו שתי הקבוצות מתקיימות. 3) משפט האי שלמות הראשון של גדל אומר שאם יש לנו מערכת אקסיומות מספיק עשירה (ובתור שתי דוגמאות חשובות ניקח את אקסיומות צרמלו פרנקל לתורת הקבוצות ופיאנו למספרים הטבעיים) אזי קיים משפט שלא ניתן להוכיחו או להפריכו, המסקנה של המשפט הזה מתחלקת לשניים א) באקסיומות של צרמלו פרנקל נקבל (כתוצאה ממשפט השלמות) שקיימים שתי מודלים אחד שבו המשפט מתקיים והשני שבו הוא לא. ב) בפיאנו נקבל (עקב המשפט הקטגורי) שקיים משפט שנכון בכל מודל אך שלא ניתן להוכיחו או להפריכו. 4) חשוב להבין שמשפט השלמות של גדל לא מסיים את הסיפור. הוא בעצם מעביר את הבעיה מאקסיומות למודלים, אם בתור מודל לתורת הקבוצות המוכלות בממשיים ניקח את קבוצת הממשיים איחוד קבוצת החזקה של הממשיים ונגדיר "איבר ב" כאיבר ב אזי יש לנו מודל ועכשיו אנחנו יכולים לשאול: האם במודל הזה אנחנו יכולים להוכיח או להפריך את השערת הרצף? (רמז,לא). |
|
|
|
|
|
|
||
|
||||
|
הבהרה: לצטט את אברון זה אחלה. כשנכנסים לדיון על עומק הפרטים (שאברון במוצהר נאלץ לחפף בהם כי הוא כותב ספר לציבור הרחב), להביא אותו בתור המקור הראשי ולא לציין במפורש שום מקור אחר זה לא רציני. (2 הוא לא משפט השלמות של גדל, אלא נראה כמו מעין ניסוח לא מוצלח של משפט אי השלמות הראשון; 3ב' שגוי ונובע מבלבול שלך בין פיאנו מסדר ראשון שעליה חל משפט אי השלמות, ופיאנו מסדר שני שהיא קטגורית ולא עליה דיברתי) |
|
|
|
|
|
|
||
|
||||
|
2) מדובר אכן בניסוח של משפט השלמות בניסוח הכי חזק שניתן. 3ב. משפט אי השלמות הראשון אכן חל גם על פיאנו סדר שני, לדוגמה הנה הוכחה של משפט אי השלמות הראשון של גדל למספרים .http://www.maths.lth.se/matstat/staff/bengtr/mathlog... ורק הערה לאמיצים שעדיין איתנו, מדובר אומנם בהוכחה שלמה אבל מדובר בטקסט די קריא שכמעט לא דורש ידע מוקדם. הדברים היחידים שצריך להבין זה מה זה משפט לוגי ואת העובדה (שהיום היא טריוויאלית) שניתן להצמיד לכל משפט לוגי מספר. |
|
|
|
|
|
|
||
|
||||
|
משפט אי-השלמות לא חל על תורות מסדר שני (ואני לא מבין למה כוונתך ב"הוכחה של משפט אי השלמות הראשון של גדל למספרים".) הבעייה עם תורות מסדר שני היא בדיוק שאין להן את משפט ה*שלמות* - אין לנו (ולא יכול להיות לנו) מושג סינטקטי של "הוכחה" בתורות כאלה. במילים אחרות, אוסף המשפטים הנכונים של תורה כזו אינו ניתן אפילו למנייה רקורסיבית. מכאן יוצא שאי-אפשר אפילו *לנסח* את משפט אי-השלמות לתורות כאלה, כיוון שהוא דן בדיוק ביכולת להוכיח סינטקטית משפט או את שלילתו. משפט אי-השלמות הראשון תקף, כמובן, לכל תורה מסדר ראשון, כולל תורות של "מספרים", של קבוצות, ושל זברות ורודות. אם מה שמעניין אותך זו האמת לגבי מספרים טבעיים - ונדמה לי שכך הוא - אז אתה יכול כמעט לשכוח מכל הנ"ל ולהתרכז בתוצאה פשוטה וקונקרטית כמו: אין אלגוריתם היכול להכריע אם למשוואה דיופנטית נתונה יש פתרון. תוצאה זו מקיפה כל שיטה להוכיח טענות על המספרים הטבעיים - תהא זו דרך תורה מסדר ראשון, מסדר שני, מסדר שלישי או מה שלא יהיה. לגיטימי להמשיך לתהות האם נובע מכך שיש טענות על הטבעיים אשר "אין להן ערך אמת". אני אישית איני סבור כך (ויש באייל כמה דיונים בנושא הזה). השערת גולדבך איננה מועמדת טובה לטענה כזו (מהיותה פסוק מטיפוס פאי-1, כלומר שאם אינה נכונה כל תורה מינימלית מסוגלת להוכיח זו). |
|
|
|
|
|
|
||
|
||||
|
משפט השלמות לא חל על תורות מסדר שני אבל משפט אי השלמות הראשון כן חל. קודם כל ניסוחו: קיים משפט לוגי בשפה של מערכת פאנו שלא קיימת לו הוכחה, מכיוון שההוכחות התקפות דוקא כן ניתנות למניה רקורסיבית מה שאתה טוען הוא בסך הכל הוכחה אחרת למשפט. לגבי ההוכחה כבר נתתי pdf. לגבי האלגוריתם, קצת עצוב לי לבשר לך את זה אבל עשית את אחת הטעויות הבסיסיות באלגוריתמיקה, יש אלגוריתם, מבין שתי האלגוריתמים "כן" ו"לא" אחד מהם הוא הפיתרון המבוקש. |
|
|
|
|
|
|
||
|
||||
|
הופס - תגובה אחת וכבר אני מצטער שהצטרפתי לדיון. על לא דבר! | |
|
|
|
|
|
||
|
||||
|
מצטער שחשדתי בכשרים, בדיוק חשבתי שאולי התכוונת להגיד אלגוריתם שמקבל כל משוואה דיופנטית ועל משוואה ספציפית אומר אם כן או לא. | |
|
|
| חזרה לעמוד הראשי |  |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |