בתשובה לאינקוגניטו, 26/12/09 23:59
 |
|
 |
||
|
||||
 |
למען האמת, אני לא בטוח שאפשר לנסח אותה כך. נראה לי שהכי טוב אם תפנה אותי לספר טוב שדן בנושא. מה זאת אומרת "מכיל סתירה"? כל הרעיון כאן הוא ש-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. לגבי האלגוריתם, קצת עצוב לי לבשר לך את זה אבל עשית את אחת הטעויות הבסיסיות באלגוריתמיקה, יש אלגוריתם, מבין שתי האלגוריתמים "כן" ו"לא" אחד מהם הוא הפיתרון המבוקש. |
|
|
|
|
|
|
||
|
||||
|
הופס - תגובה אחת וכבר אני מצטער שהצטרפתי לדיון. על לא דבר! | |
|
|
|
|
|
||
|
||||
|
מצטער שחשדתי בכשרים, בדיוק חשבתי שאולי התכוונת להגיד אלגוריתם שמקבל כל משוואה דיופנטית ועל משוואה ספציפית אומר אם כן או לא. | |
|
|
|
|
|
||
|
||||
|
איזה כיף זה לאנשי המתמטיקה לעומת אנשי מדעי הרוח. | |
|
|
|
|
|
||
|
||||
|
אני מכיר רק צרמלו מסדר ראשון (אברם), וצרמלו מסדר שני (יוסי בנאי). | |
|
|
|
|
|
||
|
||||
|
סורמלו (אברם, יוסי בנאי). | |
|
|
|
|
|
||
|
||||
|
(יודע, לא צריך להרוס כל בדיחה) | |
|
|
|
|
|
||
|
||||
|
קבלתם את כל הבחורות ואתם עוד מתלוננים? | |
|
|
|
|
|
||
|
||||
|
למה? בגלל הכותרת? חוץ מזה, מה שראובן אמר. |
|
|
|
|
|
|
||
|
||||
|
לא, בגלל שקל יחסית לנפות עמדות מוטעות או טרחניות (אני לא מתייחס דווקא לאינקוגניטו. אין לי את הידע הנחוץ כדי לגבש דעה על דבריו). במדעי הרוח לא ברור מהם הקריטריונים להיותה של עמדה בעלת ערך. גרוע מכך, פעמים רבות חברי אסכולות שונות מתייחסים מלכתחילה לדברי חברי אסכולות אחרות כשטויות שאינן ראויות לעיון. ועוד יותר גרוע מכך, לפעמים מתברר בסופו של דבר שהטרחנים צדקו. בנוגע למה שראובן אמר, אני לא חושב שלך יש על מה להתלונן. |
|
|
|
|
|
|
||
|
||||
|
מצד אחד אתה צודק, ומצד שני... ובכן, אלון כבר כתב מאמר מצויין על ה"מצד שני" הזה, ואחר כך ראינו גם איך זה בא לידי ביטוי בפועל. מעטים הם המקרים שבהם אפשר ממש להצביע על טעויות של הצד השני ולומר "אתה טועה!". וגם אז, לרוע המזל, הוא עשוי לטעון שמדובר בבלבול רגעי ולא בחוסר הבנה מהותי (כשמדובר בדיון; כמובן שאם מדובר במאמר, טעות מחסלת אותו). |
|
|
|
|
|
|
||
|
||||
|
כל אחד עלול לטעות ולדבר שטויות. זה קורה גם למקצוענים וגם למלומדים, וזה באמת לא נורא בעיניי. העניין הוא שישנם אנשים שאין טעם להיכנס לדיון איתם. לא בגלל שהם טועים, אלא בגלל שהם דוגמטים ולא מוכנים לקבל ביקורת תקפה. במתמטיקה, כך אני מתרשם, תוכל לעלות על אדם שהוא גם טועה וגם דוגמטי די מהר ובכך לחסוך לעצמך אנרגיה ועגמת נפש. מנגד, בתחומים ''רכים'' יותר, קיים סיכוי טוב שאם אינך מקבל את דרכי הטיעון של יריבך לדיון, זה דוגמטי מצדך ולאו דווקא מצידו. יכול להיות שיש לו דווקא משהו חשוב להגיד, אבל בגלל שצורת ההצגה, הנחות היסוד או המתודולוגיה שונים מאלו שאתה רגיל בהן, מתנהל לו שיח חירשים. במצב כזה, קשה מאוד, ונדרשת לפעמים השקעה רבה, כדי לדעת שמולך ניצב פשוט אדם דוגמטי ולא בן-שיח סביר. | |
|
|
|
|
|
||
|
||||
|
על זה בדיוק אני מדבר - גם במתמטיקה, להצביע על טעות של מישהו לא בהכרח יגרום לו לומר "אופס" ולסיים בכך את הדיון תוך קבלת עמדתו של הצד השני (אני חושב שכל אחד ממתמטיקאי האייל סיים כך דיון לפחות פעם אחת, ולי זה קרה הרבה יותר מפעם אחת). ואכן, לעלות על אדם דוגמטי וטועה זה יחסית קל; הבעיה היא שדווקא בגלל שהטעות כל כך "ברורה", הדחף להמשיך ולציין אותה לא נעלם, והתוצאה היא דיון של 7,000 תגובות. |
|
|
|
|
|
|
||
|
||||
|
כן, אבל אתה יכול לסיים את הדיון מבחינתך. להגיד לעצמך "זהו טרחן". לחייך, להיפרד בנימוס ולרדוף אחרי הנערה שמסתובבת עם מגש האפריטיפים. אתה לא צריך להמשיך לשוחח איתו כל המסיבה בגלל שהנושא עצמו מעניין אותך. אם יש אנשים אחרים מעוניינים להחליף איתו 7,000 תגובות נוספות זה לא צריך לשנות לך. | |
|
|
|
|
|
||
|
||||
|
יכול. מוטב תגיד לאלכוהוליסט שהוא יכול פשוט לקום בבוקר ולחייך ולזרוק את הבקבוק לפח. אולי כבר עדיף להיות כמוך ולחשוב שיש הצדקה להמשך הדיון-עם-הטרחן שנעוצה באינטרוספקציה ובספקנות עצמית מתמשכת, ולא סתם בכך שאתה מכור בעל יצר הרס עצמי. |
|
|
|
|
|
|
||
|
||||
|
אבל אתה לא איש מדעי הרוח. תצטרך למצוא תירוץ אחר. | |
|
|
|
|
|
||
|
||||
|
אני חושב שאתה צודק, וזה עבורי אחד הדברים המושכים בתחום. במהלך המפגש שלי עם פילוסופיה מודרנית (קונטיננטלית, בייחוד), הרגשתי לא מעט פעמים שאני חשוף לטרחנות דוגמטית ויחד עם זאת שאין דרך מסודרת, פשוטה לפחות, לשכנע אחרים שזה המצב. בסוף פשוט ויתרתי והסתפקתי במה שהצעת לגדי - לחייך ולעבור למגש האפריטיפים. ובנוגע למה שראובן אמר, אתה גם צודק. ד"ש :-) |
|
|
|
|
|
|
||
|
||||
|
למה זה אחד הדברים המושכים בתחום עבורך? אני מרגיש חשוף לטרחנות בעיקר כשאני נתקל בפילוסופיה אנליטית. אני מתאר לעצמי שלפחות חלק מההרגשה הזאת נובע מחוסר ההיכרות שלי עם הפרדיגמה. ואני מצטער שאין לי יותר הכשרה בפילוסופיה קונטיננטלית. לפעמים אני מרגיש שאני זקוק בדחיפות לפגוש רעיונות חדשים ומלהיבים. אז נכון שקריאה בפילוסופיה קונטיננטלית מחייבת הנמכה מסוימת של אמות המידה ה"רציונאליות". אבל הרווח הוא במשמעות, ובעושר הזוויות והאפשרויות להתבונן על העולם ועל החיים. אבל טוב, זה ויכוח ישן. |
|
|
|
|
|
|
||
|
||||
|
ראית שאני פורש מדיון על מתמטיקה שלא מוצה, ולא הסקת את המסקנה...? | |
|
|
|
|
|
||
|
||||
|
מסתבר שלא. לא קראתי את כל הפתילים (אולי היתה זו שגיאה) והשתכנעתי שיש כאן טעם בעוד קצת הסברים. נראה שאין. | |
|
|
|
|
|
||
|
||||
|
|
|
|
|
|
|
||
|
||||
|
אתה כתבת שאי אפשר אפילו לנסח את משפט אי השלמות לתורות מסדר שני . לעומת זאת בתגובה 166640 כתבת לד"ר טי "אני בטוח שאתה מכיר את משפט אי-השלמות ללוגיקה מסדר שני" בקיצור יא שקרן רימית את כולם וחשבת שלא יעלו עליך. אז עד שלא תסביר אני אחשוב שאתה שקרן ואם ההסבר שלך יהיה מספיק טוב אני אחשוב שאתה סתם חמור קופץ בראש. | |
|
|
|
|
|
||
|
||||
|
במקום להתעמק בתגובות עתיקות (ושגויות) שלי, תוכל ללמוד הרבה יותר מקריאת ספרות בנושא (כמו הספר עליו המלצתי). התגובה ההיא נכתבה בשנת 2003, ואת רוב מה שאני יודע על הנושא למדתי אחר-כך - בין השאר בעקבות העניין שהתעורר בי במהלך הדיון ההוא (ד"ר טי היה בבת אחת מתדיין בלתי-נסבל וגם הרבה יותר נעים לדיון ממך). מה ש*התכוונתי* להזכיר אז היה המשפט שאומר שאין ללוגיקה מסדר שני משפט שלמות, ובבורותי קראתי לזאת "משפט אי-השלמות ללוגיקה מסדר שני". אבל אפילו אז הבנתי שאין מדובר ב"משפט אי-השלמות של גדל". כפי שהוסבר כבר, ה"שלמות" של משפט השלמות וה"אי-שלמות" של משפט אי-השלמות הן מושגים שונים לחלוטין. משפט אי-השלמות של גדל אומר שבתנאים מסויימים קיים פסוק שאין לו הוכחה וגם לשלילתו אין כזו. זהו משפט מתמטי, לא פילוסופי ולא מטא-מתמטי, ומכאן שיש משמעות פורמלית למושג "הוכחה" המופיע בניסוח שהרגע ציטטתי. משמעות זו היא שרשרת של פסוקים העונה על התנאים הטכניים של "הוכחה" עבור תחשיב הפסוקים מסדר ראשון. דא עקא, שלתחשיב הפסוקים מסדר שני אין מושג כזה של שרשרת המהווה הוכחה. ועוד היבט: בכל פעם שאתה מפעיל (בהצלחה) את המשפט הזה על מערכת אקסיומות מסויימת, אתה יכול להסיק (בעזרת משפט השלמות) שלאותה מערכת יש שני מודלים שונים. לאריתמטיקה מסדר שני יש מודל יחיד (זוהי תורה קטגורית), וממילא אתה יכול לראות שאי-אפשר להפעיל עליה את המנגנון הזה. דבר אחד נכון בהחלט: גם באריתמטיקה מסדר שני יש משפטים שלא ניתן להוכיח-פורמלית, אבל זאת מסיבה פשוטה מאוד: אין דרך פורמלית להצרין "נביעה לוגית" בלוגיקה מסדר שני, וממילא אין לנו יכולית להוכיח-פורמלית משפטים בלוגיקה כזו. המונח "אקסיומות פאנו" יכול להתייחס גם לניסוח מסדר ראשון (עם סכמת-אקסיומות עבור אינדוקציה) וגם לניסוח מסדר שני. דומני שכיום מקובל הרבה יותר להתייחס לסדר ראשון. זה לא מאוד משנה - העיקר הוא להבין, בכל הקשר נתון, על איזו תורה מדובר (שכן ההבדלים ביניהן, כפי שהסברתי, מהותיים מאוד). ועכשיו, מסיבות שאני בטוח שאתה מבין, אפרוש סופית מהדיון איתך. אם משהו עדיין לא ברור, קרא את הספר עליו המלצתי או את ספרו המצויין של Torkel Franzen. |
|
|
|
|
|
|
||
|
||||
|
לא בהכרח מלמד לגבי תרבות הדיון, אבל ד"ר טי כנראה יודע חשבון טוב מאינקוגניטו. |
|
|
|
|
|
|
||
|
||||
|
והוא אף מחזיק ביכולת להודות בטעות (תגובה 171334). אילו ידעתי אז את כל מה שאני יודע היום הייתי יכול לעזור לו להגיע למסקנה הזו הרבה יותר מהר. | |
|
|
|
|
|
||
|
||||
|
חידוד קטן: אין בעיה להגדיר "מערכת הוכחה" עבור לוגיקה מסדר שני - למשל, רמאות קטנה שנקראת "הוכחה סמנטית", שבה אומרים שקבוצת פסוקים א' מוכיחה את הפסוק ב' אם כל מודל ל-א' הוא מודל לב' (כלומר, א' גורר סמנטית את ב'). כמובן שזו מערכת הוכחה חסרת כל ערך, אבל מבחינה הגדרתית היא לגיטימית. הבעייתיות הרלוונטית במערכת הזו היא שזו לא מערכת *אפקטיבית*, כלומר דרישת האפקטיביות (שהיא הרי קריטית אצל גדל) היא מה שנכשל הפעם, ולא השלמות (אני רואה את גדל כמעין משפט Trade-off - אי אפשר להיות בו זמנית גם שלמים, גם עקביים וגם אפקטיביים). (אני מודה ש"הוכחה סמנטית" הוא מושג שבו נתקלתי רק בהקשר של תחשיב הפסוקים, ושם אפילו הייתה לו תועלת כלשהי; אבל אני לא רואה בעיה עם ההכללה האידיוטית שלי, מבחינה עקרונית). |
|
|
|
|
|
|
||
|
||||
|
ודאי - לכן הדגשתי "להצרין". זו לא "רמאות", זו פשוט הדגשת ההבדל בין נביעה לוגית ליכיחות פורמלית. משפט השלמות של גדל מראה שההבדל הזה לא קיים בלוגיקה מסדר ראשון, וחסרונו בלוגיקה מסדר שני מראה את הבעייתיות של מערכות אקסיומטיות מסדר שני. | |
|
|
|
|
|
||
|
||||
|
1) גם לי נמאס מהדיון הזה. 2) יש משפט אי שלמות לסדר שני. 3) רק בריאות. 4)ביי. |
|
|
|
|
|
|
||
|
||||
|
(נסיון אחרון) 2) רפרנס לספר (Textbook, כזה שמוכיח דברים באופן רציני) שמנסח ומוכיח את המשפט? (אם יש רק מאמר, אז מאמר) |
|
|
|
|
|
|
||
|
||||
|
(מאוד ייתכן שיש משפט המכונה בשם הזה - אז מה? כל מה שאמרתי הוא שמשפט אי-השלמות הראשון של גדל מנוסח באופן כזה שאינו חל על תורות מסדר שני, כי הוא מניח כנתון קיומה של מערכת הוכחה פורמלית). | |
|
|
|
|
|
||
|
||||
|
(וואו, נכנסת לשדה מוקשים. עכשיו אפשר לשלוף לך ספר שמשחק באופן שונה עם הטרמינולוגיה וכן מדבר על משפט אי השלמות הראשון, במובן של ה-Tradeoff שהזכרתי קודם) | |
|
|
|
|
|
||
|
||||
|
יכול להיות. אני לא חושב שזה מאוד משנה - בסה''כ יש כאן סדרה לא ארוכה של טענות ברורות מאוד לגבי היכולת להוכיח באופן פורמלי דברים לגבי מספרים טבעיים. אלו שאלות מעניינות שאני בד''כ נהנה לדון בהן (יותר מדי נהנה לפעמים), אבל לא באופן שהדיון הזה התדרדר אליו. | |
|
|
|
|
|
||
|
||||
|
תאמין לי אם הייתי יודע שעל זה הדיון הייתי מוותר לך מלכתחילה, אז משפט גדל לא מדבר על סדר שני זה המשפט השני שמדבר על סדר שני. ביג דיל. |
|
|
|
|
|
|
||
|
||||
|
בדיוק: ביג דיל. (על מה בדיוק היית צריך "לוותר" לי? ביקשת ממך משהו?) | |
|
|
|
|
|
||
|
||||
|
(צ''ל ''ביג דיל''. גם לדעתי שמות המשפטים אינם חשובים.) | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |