בתשובה לאינקוגניטו, 27/12/09 19:23
 |
|
 |
||
|
||||
 |
אל תתבלבל בין משפט השלמות של גדל ומשפט אי השלמות של גדל. אלו שני משפטים שונים, ואפילו המשמעות של "שלמות" שונה. משפט השלמות מדבר על שלמות במובן של "כל מה שנכון ניתן להוכחה", ומשפט אי השלמות מדבר על שלמות במובן של "כל מה שניתן לניסוח ניתן להוכחה או ששלילתו ניתנת להוכחה". זה לא אותו דבר. מה שמשפט אי השלמות של גדל מראה הוא שעבור מערכות אקסיומות מסויימות קיימים תמיד שני מודלים שונים מהותית ביחס למשפט שניתן לנסח באמצעות השפה של המערכת. בפרט, המשפט שגדל בונה הוא נכון במודל אחד, ולא נכון במודל אחר (חשוב להבין שהמשפט של גדל לא אומר טענה כמו זו שציטטת באופן מפורש; הוא אומר משהו על מספרים, ולכן הפרשנות המדוייקת של מה שהוא אומר תלויה במודל שבו הטענה מפורשת ובהתנהגות של "מספרים" בתוך אותו מודל). |
 |
 |
 |
|
|
|
||
|
||||
|
אם לקשר (באופו רופף ) לנושא המרכזי אז ויקיפדיה איתי משפט אי השלמות של גדל [ויקיפדיה] משפט רלוונטי (שמופיע כבר בהתחלה)."גדל הראה שבכל מערכת אקסיומות סופית ועשירה מספיק (כזו המכילה את אקסיומות האריתמטיקה החלשה) קיימות טענות אמיתיות שלא ניתן להוכיחן." | |
|
|
|
|
|
||
|
||||
|
לדעתי ויקיפדיה מתנסחת גרוע בנקודה הזו. "אמיתי" בהקשר הזה הוא "אמיתי במודל שמעניין אותנו", כשההנחה היא שתמיד עומד לנגד עינינו כזה (למשל, במקרה של פיאנו - המספרים הטבעיים). המשמעות בפירוש אינה "נכון בכל המודלים". אם אתה מתעקש להביא את ויקיפדיה העברית כמקור, אז בערך משפט השלמות של גדל [ויקיפדיה] יש התייחסות לכך: "גרסה פופולרית (ושגויה) של משפט אי השלמות הראשון של גדל קובעת ש"בכל תורה קיימת טענה אמיתית שאינה ניתנת להוכחה". משפט השלמות סותר במפורש את הניסוח הזה: כל משפט שהוא אמיתי (בכל מודל), ניתן להוכחה. אכן, לפי משפט אי השלמות קיימת בתורה (חזקה מספיק, דהיינו אריתמטית, אפקטיבית ועקבית) נוסחה שאינה ניתנת להוכחה (וגם לא לסתירה) - אבל אין זה נכון שנוסחה זו נכונה בכל מודל. אדרבא, לפי משפט השלמות, קיים מודל עקבי שבו היא נכונה, וקיים מודל עקבי שבו היא אינה נכונה." דיון קצת יותר חפרני בכל עניין האמת יש בספר המוצלח של 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 שהזכרתי קודם) | |
|
|
|
|
|
||
|
||||
|
יכול להיות. אני לא חושב שזה מאוד משנה - בסה''כ יש כאן סדרה לא ארוכה של טענות ברורות מאוד לגבי היכולת להוכיח באופן פורמלי דברים לגבי מספרים טבעיים. אלו שאלות מעניינות שאני בד''כ נהנה לדון בהן (יותר מדי נהנה לפעמים), אבל לא באופן שהדיון הזה התדרדר אליו. | |
|
|
|
|
|
||
|
||||
|
תאמין לי אם הייתי יודע שעל זה הדיון הייתי מוותר לך מלכתחילה, אז משפט גדל לא מדבר על סדר שני זה המשפט השני שמדבר על סדר שני. ביג דיל. |
|
|
|
|
|
|
||
|
||||
|
בדיוק: ביג דיל. (על מה בדיוק היית צריך "לוותר" לי? ביקשת ממך משהו?) | |
|
|
|
|
|
||
|
||||
|
(צ''ל ''ביג דיל''. גם לדעתי שמות המשפטים אינם חשובים.) | |
|
|
|
|
|
||
|
||||
|
דיברתי עם גדי, לא שאכפת לי שאתה מדבר עם הטרחן שקרא לך שקרן, פשוט משמעות המילה ''לך'' משתנה. | |
|
|
|
|
|
||
|
||||
|
(שכחתי להמליץ, לא בפעם הראשונה כמדומני, על Computability and Logic של Boolos, Burgess and Jeffrey. יש שם ניסוחים מדוייקים של כל המשפטים שהצליחו לבלבל אותך עד כה, כולל פרק קצר ונאה המסביר איך כל המשפטים הבסיסיים מתרסקים בתורות מסדר שני: משפט הקומפקטיות, סקולם-לוונהיים, ומשפט השלמות). | |
|
|
|
|
|
||
|
||||
|
אני לא מבין כלום במתמטיקה, אבל יש לי הרגשה שאתם לא בדיון הנכון. | |
|
|
|
|
|
||
|
||||
|
אני מקווה שאתה טועה, אבל אין לי רצון עז להעמיק חקר בשאלה הזו. | |
|
|
|
|
|
||
|
||||
|
לא ממש תכננתי לחזור לדיון הזה כי נראה לי שיש בו כל מה שצריך בשביל לקבוע דעה. אבל על תגובה 164351 קשה לוותר. | |
|
|
|
|
|
||
|
||||
|
לקחתי מהספרייה. נראה אחלה ספר (אני חושב שהצצתי בו פעם ולא התעמקתי - עכשיו אנסה לעשות קריאת Cover to cover). | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |