בתשובה לאינקוגניטו, 24/12/09 23:16
כ''ג יורדי הסירה 531996
יפה. איך המשפט שלי קשור לפורמליזם?

למכונה הדמיונית של הילברט קראו מחשב, והעובדה שהוא חשב עוד לפני המצאת המחשב על כך שהכרחי לבדוק האם ניתן לבצע "פורמליזציה" שכזו למתמטיקה מעידה על הגאונות שלו. במבט לאחור לא הכי מפתיע שפרוייקט *כל כך* שאפתני נכשל, אבל היו חייבים לנסות אותו. מן הסתם זה שהילברט ניסה זאת לא אומר שהילברט לא התעניין במשמעות של המשפטים המתמטיים (זו תהיה הנחה לא מופרכת שהוא הבין את המשמעות לפחות כמו כל מתמטיקאי אחר בן זמנו).
כ''ג יורדי הסירה 531998
1)בפוסט שלך אתה פותר (או איך שאתה לא קורא לזה) את הפרדוקס בצורה הבאה: אתה מגדיר באופן פורמלי את המילים שבפרדוקס ואז מגלה שבעצם המספר המתואר בלתי אפשרי. אתה בכלל לא מתיחס למשמעות האמיתית של המילים, אני לא אומר שזה רע באופן ספיציפי אבל זה כן מעיד על פורמליזים. מה גם שמקריאה בפוסט שלך באופן כללי הגישה שלך היא פורמליסטית (והאמת היא שכרגע נזכרתי שכשדיברת על זנון גם גלשת לאינסטרומנטליזם ).

2) להגיד שלמכונה של הילברט קראו מחשב זה אנכרוניזם, בתקופתו של הילברט מחשב היה אדם שמחשב חישובים. האמת היא זה מזכיר לי שבספר "קץ כלזמן" הגיבור הראשי הוא מחשב ולקח לי חצי ספר להבין שהם בעצם מדברים על אדם.
כ''ג יורדי הסירה 531999
1) קצת התבלבלת. אני לא אומר ש"המספר המתואר בלתי אפשרי", אלא שהתיאור עצמו הוא בלתי אפשרי. כלומר, שלא ניתן לבצע את הפעולה של תיאור המספר ה"בלתי אפשרי".

המסקנה, אם תרצה, היא שמי שמדבר באופן כללי ועמום על "תיאור" בעצם לא אומר כלום - אין משמעות אמיתית לביטוי העמום שלו. אין "משמעות אמיתית", אלא חוסר משמעות. אם כבר, לדעתי הגישה שלי היא זו שמנסה לחפש את "המשמעות האמיתית", ומדברת על מובן מאוד ספציפי וקונקרטי ומחובר למציאות של "תיאור" (תוכנית מחשב פיזית שמבצעת את החישוב פיזית).

אפשר כמובן להגיד שאני מקשקש, אבל אני לא חושב שאני מפגין גישה פורמליסטית במיוחד כאן (כלומר, של התייחסות למילים כצורה בלבד ולהתעלם מהתוכן שלהן).

2) האנכרוניזם מכוון, כמובן.
כ''ג יורדי הסירה 532004
===>"המסקנה, אם תרצה, היא שמי שמדבר באופן כללי ועמום על "תיאור" בעצם לא אומר כלום - אין משמעות אמיתית לביטוי העמום שלו. אין "משמעות אמיתית", אלא חוסר משמעות. אם כבר, לדעתי הגישה שלי היא זו שמנסה לחפש את "המשמעות האמיתית", ומדברת על מובן מאוד ספציפי וקונקרטי ומחובר למציאות של "תיאור" (תוכנית מחשב פיזית שמבצעת את החישוב פיזית)."

לפי דעתי מה שאתה מתאר פה הוא סוג של פורמליזים, אולי זה לא הפורמליזים הקלאסי אבל העובדה שאתה אומר שכדי למצוא "משמעות אמיתית" של ביטויים יש לעשות להם הצרנה היא מאוד בעייתית. כי במעבר לשפה הטבעית לשפת תוכנה אנחנו תמיד מאבדים משהו והעובדה היא שבינתיים אנחנו לא יכולים לעשות בשפת תוכנה מה שאנחנו יכולים לעשות בשפה טבעית כך שאפילו בהסתכלות מתמטית
זהו משהו שחבל לאבדו.

===>"אפשר כמובן להגיד שאני מקשקש" אם היית מקשקש לא הייתי מצטט אותך, ובכלל פורמליסטים לא מקשקשים. מה שהם אומרים נכון, הם פשוט מפספסים חלק חשוב במציאות.
כ''ג יורדי הסירה 532010
אני אנסה לחדד עוד טיפה את מה שאני טוען שם. אני אומר שלדבר על "תיאור" באופן כללי זה להגיד משהו שהוא פשוט שגוי. כמו שבתורת הקבוצות להתייחס להכל כקבוצה זה פשוט שגויה - כלומר, אתה אמנם יכול לכתוב את המילים "קבוצת כל הקבוצות שאינן מכילות את עצמן", אבל האמירה הזו היא ריקה וחסרת משמעות.

אז צריך "לחפש משמעות", ואני באתי והצעתי פירוש אחד אפשרי. לא, חס ושלום, את כל הפירושים האפשריים; אבל פירוש אפשרי אחד. בפירוש האפשרי הזה המצב נהיה עדיף בהרבה על המצב הקודם כי כעת יש הגיון במושג של "תיאור". האם אנחנו מאבדים משהו? רק אם אנחנו מתעקשים מעתה והלאה לדבוק במושג הזה בתור המושג *היחיד* של תיאור, ואת זה אני מן הסתם לא עושה - אני רק מנסה להדגיש שהמושג ה"כללי ביותר" לא אומר הרבה, בעצם, ולכן אם נתעקש לדבוק *בו* אז אנחנו מאבדים משהו.
כ''ג יורדי הסירה 532013
האמירה ''קבוצת כל הקבוצות שאינן מכילות את עצמן'' איננה חסרת משמעות. היא מביעה קביעה אינטואיטיבית לגבי קבוצות שהיינו רוצים שהקבוצות יקיימו. העובדה שבצירוף עם עוד הנחות אתה מקבל פרדוקס רק אומרת שהאמירה לא יכולה להתקיים במציאות בצורה נאיבית. עדיין כדי להבין מה זה קבוצה אתה צריך להסתכל על ההסתכלות הכללית.
כ''ג יורדי הסירה 532015
טוב, נראה לי שהגענו לנקודת אי ההסכמה הפילוסופית. אני חושב שבגישה הזו אתה לא מבין מה זו קבוצה אלא מבין מה זו "קבוצה" - מושג אינטואיטיבי שאין לו פשר ממשי. הזכרת קודם את הפרדוקסים של זנון - גם כאן הבעיה היא זהה, לטעמי - מתלוננים על מושג הסכום של קושי שהוא מלאכותי ופורמליסטי, תוך התעלמות מכך שמושג ה"סכום" האינטואיטיבי הוא חסר פשר.

(ואילו עוד הנחות? כל מה שצריך להניח הוא שקיים כזה יצור, "קבוצת כל הקבוצות שאינן מכילות את עצמן", כשהפשר של הכלה הוא שא' או מוכל בב' או לא מוכל בב' אבל לא שניהם).
כ''ג יורדי הסירה 532023
המושג שלי הוא אולי אינטואיטיבי אבל בהחלט יש לו פשר. נניח והיינו ממצאים מערכת אקסיומות חדשה אחת השאלות שהיינו שואלים עליה היא האם היא דומה למערכת הקבוצות האמיתית. והענין שזה קרה יש מערכת אקסיומות אלטרנטיבית (או משלימה) לתורת הקבוצות שנקראת תורת האוספים ואחת הסיבות שהיא התקבלה היא כי אינטואיטיבית היא מאוד הגיונית.

(עובדה שבמערכת של צרמלו ופרנקל ה''יצור'' הזה קיים והוא פשוט הקבוצה הריקה.)
כ''ג יורדי הסירה 532026
(?)
כ''ג יורדי הסירה 532029
(במערכת האקסיומות של צרמלו פרנקל אין אף קבוצה שמכילה את עצמה בתור איבר לכן קבוצת כל הקבוצות שמכילות את עצמן כאיבר היא הקבוצה הריקה.
זה מוכיח שכדי להגיע לפרדוקס צריכים עוד הנחות).
כ''ג יורדי הסירה 532036
כזכור, אנחנו מדברים על "קבוצת" כל הקבוצות ש*אינן* מכילות את עצמן.
כ''ג יורדי הסירה 532069
מה שגדי אמר.
כ''ג יורדי הסירה 532088
אה זה פשוט, התבססי על המתמטיקה הרומנטית השמה את עדניה על הפסיכולוגיה האנושית אשר איננה מבדילה בין כן ללא.
או בקיצור: פדיחה!
כ''ג יורדי הסירה 532027
המצאת מושג חדש, והגדרת אותו.

מה זה בדיוק עוזר לך שהוא דומה למשהו מ"העולם האמיתי"? לי אישית קשה לדמיין אינטואיטיבית קבוצה אינסופית, אבל מתברר שבעזרת הגרות מתאימות, המושג הזה שימושי למדי.
כ''ג יורדי הסירה 532034
כמו שהמטרה העיקרית של המדע היא לתאר את העולם כך (לדעתי) גם אחת המטרות החשובות במתמטיקה היא לתאר את ה''עולם'' המתמטי לכן אני מעונין שמערכת האקסיומות שלי תהיה דומה ככל הניתן לעולם האמיתי. חוץ מזה אני חושב שבעולם האמיתי יש איכויות שאין בשום עולם אחר.

לי גם קשה לדמיין מושג כמו אהבה והמילים עוזרות לי בזה. אבל ברור ששום שיר לא יגיע לרמת הבנה שאני מקבל כשאני חווה אהבה.
כ''ג יורדי הסירה 532037
גם אני מעוניין שמערכת האקסיומות שלי תהיה דומה ככל הניתן לעולם האמיתי - וזה בדיוק גם מה שהילברט הפורמליסט היה מעוניין בו. הוא רצה מערכת אקסיומות שהיא כל כך טובה, שהיא *בדיוק* העולם האמיתי.
כ''ג יורדי הסירה 532038
איך יכול להיות שאתה רוצה שמערכת האקסיומות תהיה דומה לעולם האמיתי אם אתה כופר בקיומו (או שלא הבנתי את תגובה 532035)
כ''ג יורדי הסירה 532040
אני לא כופר בקיומו, אלא שאני חושב שבעולם האמיתי יש הרבה דברים שאפשר לקרוא להם "מערכת הקבוצות האמיתית" ולא ממש ברור במי מהם לבחור (האם נבחר במערכת קבוצות שבה השערת הרצף מתקיימת? או במערכת קבוצות שעבורה היא אינה מתקיימת? ומה עם אקסיומת הבחירה?)

המצב בכל הנוגע לקבוצות הוא הרבה פחות חד משמעי מאשר במקרה של המספרים הטבעיים, למשל - כאן אנחנו יכולים לדבר על המודל ה"נכון" של אקסיומות פיאנו (ולנודניקים האחרים שמקיימים את האקסיומות לקרוא "מודלים לא סטנדרטיים").

בקיצור, "העולם האמיתי" הוא דבר מאוד מורכב, עד כדי כך שאפילו עם אקסיומות מסודרות אי אפשר לתאר את כולו באופן פשוט; אז מתמיהה אותי היומרה לנסות ולתאר אותו בלי אקסיומות מסודרות אלא עם נפנופי ידיים בלבד.
כ''ג יורדי הסירה 532091
זה שאני לא יודע משהו לא אומר שיש דרגות חופש.
לדוגמה אני לא יודע אם בספרד יש ברד או לא אבל אני יודע שאו שכן או שלא. באותה מידה אני לא יודע אם השערת הרצף נכונה או לא אבל אני כן יודע שרק אחת מן האפשרויות נכונה. מה שאומר שאחד מן המודלים משקף את העולם האמיתי והשני הוא סתם מודל.

בקשר לאקסיומת הבחירה כאן אני מניח שהיא נכונה, סביר להניח שגם אתה.

מה שגדל ניסה להוכיח היה בדיוק זה, שיש דברים בעולם האמיתי שלעולם לא נדע, כי מה לעשות וגם הוא היה אפלטוניסט.
כ''ג יורדי הסירה 532093
זה פשוט לא נכון.

מה זה אומר "סתם מודל"? מישהו שלא קיים בעולם הפיזי? גם המודל ה"נכון" לא קיים בעולם הפיזי. ב"עולם האמיתי" המתמטי יש הרבה יצורים שונים שמקיימים את אקסיומות תורת הקבוצות, והשאלה היא על מי מהם אנחנו רוצים להדביק את התווית "המודל הנכון". זה לא יהפוך אותו ל"אמיתי" יותר מהשני. גם המודלים הלא סטנדרטיים של אקסיומות פיאנו הם לא "אמיתיים" פחות מהמודל הסטנדרטי של הטבעיים; הטבעיים פשוט יותר מעניינים אותנו.

גדל לא ניסה להראות שיש דברים ש"לעולם לא נדע" וגם לא הוכיח שום דבר כזה (אם כבר טיורינג ושות' נותנים תוצאה שהיא יותר ברוח זו), אלא הראה שבמקרה של תורת המספרים ודברים שמכילים אותה, לא יכולה להיות זהות בין מערכת אקסיומות "פשוטה" ובין המודל עצמו - כלומר, יש במודל עוד משהו שהוא מעבר לכל מערכת אקסיומות נתונה עבורו. זה בהחלט דבר טוב עבור פלטוניסט, אבל לא קשור למה שאנחנו מדברים עליו.

כדי לחדד את הנקודה: בהינתן טענה מהסוג שמשפט גדל נותן, אנחנו לא יודעים אם היא נכונה או לא *במספרים הטבעיים*, אבל אנחנו יודעים שרק אחת משתי האפשרויות נכונה; אבל אם הטענה נכונה בטבעיים, אז בנוסף לכך קיים מודל לא סטנדרטי של מערכת האקסיומות שלנו שבו הטענה אינה נכונה. לכן אני חוזר לשאלה הבסיסית - איזה מהמודלים אני מעדיף? אבל לקיום של שניהם אני לא יכול להתכחש.
כ''ג יורדי הסירה 532103
בוא ניקח את הדוגמה האחרונה שלך נניח שיש לי טענה מהסוג של גדל, נקרא לה טענה A אזי או שהיא נכונה בטבעיים או שלא. אם היא נכונה אזי אקסיומות פיאנו בתוספת עם הטענה ישקפו את הטבעיים בצורה יותר טובה מאקסיומות פיאנו הסטנדרטיות. לעומת זאת אקסיומת פיאנו בתוספת שלילת A יתנו לנו מודל שבו יש משפטים שלא תופסים בטבעיים (לדוגמה שלילת A). עכשיו לשאלה איזה מודל משקף יותר טוב את הטבעיים יש תשובה בינארית, רק הבעיה היא שאני לא יודע מהי.
כ''ג יורדי הסירה 532119
אני מסכים עם כל מילה שאמרת כאן, ולמעשה זה מה שניסיתי לומר עוד קודם. מה הבעיה?

(אולי הבעיה היא בכך שאתה חושב שהמודל-עם-משפטים-שלא-תופסים-בטבעיים הוא "לא מציאותי". כאמור, אני חושב שהוא מציאותי בדיוק כמו הטבעיים, רק פחות מעניין אותנו).
כ''ג יורדי הסירה 532125
אז בוא נתקדם לפונקציות על מספרים טבעיים, גם פה אתה חושב שכל משפט נכון או לא נכון על פונקציות של מספרים טבעיים?
בפרט האם אתה חושב שהשערת הרצף נכונה או לא נכונה על פונקציות של מספרים טבעיים?

ניתן לראות שגם לדעתך נובע ממשפט גדל שיש אלמנט במציאות (A משקף את המספרים הטבעיים) שאנחנו לא יכולים לדעת אם הוא נכון או לא. (מה שגדל ניסה לעשות לא משנה עכשיו).
כ''ג יורדי הסירה 532129
מה הכוונה ב"השערת הרצף נכונה על פונקציות של מספרים טבעיים"?

אני לא חושב שממשפט גדל נובע שיש אלמנט שאנחנו לא יכולים לדעת אם הוא נכון או לא; משפט גדל מדבר על השאלה אם הוא יכיח או לא ממערכת אקסיומות כלשהי, ובכלל המושג הזה של "לדעת" הוא לא הכי ברור אינטואיטיבית (האם אתה "יודע" שיש אינסוף מספרים ראשוניים? איך אתה יכול להיות בטוח שזה נכון בלי שיוכיחו לך את נכונות האקסיומות? ואיך אפשר לעשות את זה?).

כאמור, מה שטיורינג עשה הרבה יותר קרוב להוכחה מדוייקת שיש דברים שאי אפשר "לדעת" - אם נותנים לנו מכונה, לא תמיד נוכל לדעת אם היא עוצרת או לא, וזה לא משנה בכלל מה מנגנון ההכרעה שאנחנו משתמשים בו (כל עוד הוא לא חזק יותר חישוביות ממכונת טיורינג - אבל לך תמצא מנגנון הכרעה סביר בעל תכונה זו).
כ''ג יורדי הסירה 532134
אז פונקציות של פונקציות של פונקציות של מספרים טבעיים.

תראה יכול להיות שאני טועה ולא לכל מספר יש עוקב, גם יכול להיות שניוטון טעה ודברים עולים למעלה במקום למטה, הכל יכול להיות. אני חושב שהאקסיומות כן נכונות (כלומר משקפות את המספרים הטבעיים) חוץ מזה שאנשים השקיעו הרבה כסף בעובדה שיש אין סוף מספרים טבעיים, שזה גם סוג של הוכחה.
כ''ג יורדי הסירה 532136
מה הכוונה ב"השערת הרצף נכונה על פונקציות של פונקציות של מספרים טבעיים"?

הנקודה בדברי הייתה שהמושג שלך של "לדעת" הוא בעייתי. זה שיש דברים שאפשר לדעת גם בלי הוכחות ובלי כלום, בעזרת הנסיון היומיומי שלנו, זה ברור (אגב, חלק מהדברים הללו הם שגויים בתכלית). אולי כדאי שנתמקד מחדש בדיון - מה ניסית להגיד בכל עניין הידיעה? כזכור, אני טוען שגם מודל לא-סטנדרטי של הטבעיים עדיין "קיים" במובן המתמטי של המושג, פשוט לא מעניין כמו המודל הסטנדרטי.
כ''ג יורדי הסירה 532139
אפשר להגדיר פונקציות אינדיקטור שיחליפו קבוצות, כל פונקציה של פונקציות של מספרים טבעיים היא בעצם פונקציה של קבוצות וכו'

בוא נעבור מקיים או נכון למשקף. גם התיאוריה של תלמי קיימת היא פשוט לא משקפת נכון את מערכת השמש. השאלה היא מהו המודל שמשקף את המספרים הטבעיים בצורה הטובה ביותר.
כ''ג יורדי הסירה 532141
פעם אחרונה - על מה אתה מדבר כשאתה מדבר על "השערת הרצף" של הפונקציות של הפונקציות של הטבעיים? מה זה אומר בכלל?

אם עוברים למשקף הכל אחלה (אם כי אני לא מסכים עם מה שאתה אומר על "המודל שמשקף את המספרים הטבעיים" - המספרים הטבעיים *הם עצמם מודל*), ואז אנחנו חוזרים לבעיה שהצגתי בהתחלה - לא ברור בכלל מה המודל של תורת הקבוצות ש"משקף" נכון את התפיסות האינטואיטיביות שלנו.

בוא נעבור לאקסיומת הבחירה בתור דוגמה אחרת. ברור שמודל שבו אקסיומת הבחירה נכונה נראה לנו יותר "נכון" ממודל שבו היא לא נכונה. ברור גם שמודל שבו משפט הסדר הטוב אינו מתקיים נראה לנו יותר "נכון" ממודל שבו הוא כן נכון (המשפט הזה נשמע מאוד, מאוד מוזר, לפחות לי, אינטואיטיבית). לרוע המזל, מודל שבו אקסיומת הבחירה נכונה הוא גם מודל שבו משפט הסדר הטוב מתקיים, ולהפך...
כ''ג יורדי הסירה 532144
מכיוון שאני מניח שהבנת מה ה"וכו"' אמר אני קצת לא מבין איפה הבעיה.

המספרים הטבעיים הם לא מודל. פיאנו הוא מודל, פיאנו עם A הוא מודל ופיאנו עם שלילת A הוא מודל אחד משני המודלים מכיל סתירה והשני משקף את המודל של פיאנו (ולכן גם את הטבעיים) בצורה יותר מוצלחת.

אני חושב שההגדרה שלך לאינטואיטיבי היא קצת שגויה, אתה משתמש באינטואיטיבי במובן "קל לראות" בעוד המובן לדעתי של אינטואיטבי הוא "לאחר שחקרתי עמוק וחקור את השלב האחרון אני עושה באינטואיציה"
כ''ג יורדי הסירה 532145
השערת הרצף שאני מכיר אומרת - לא קיימת קבוצה מעוצמה שגדולה ממש מעוצמת הטבעיים, וקטנה ממש מעוצמת הממשיים. אני לא מבין איך עניין הפונקציות רלוונטי פה.

פיאנו היא מערכת אקסיומות. דברים שמספקים את מערכת האקסיומות נקראים מודלים. המספרים הטבעיים הם מודל לדוגמה שכזה.

אני לא בטוח שאני מבין איך פילוסופיית "השלב האחרון" הזו באה לידי ביטוי בפועל. למשל, בוא נחזור לפרדוקס של ברי - איפה נכנס ה"חקרתי עמוק וחקור" שם, אם אתה דבק בהגדרה המילולית המעורפלת?
כ''ג יורדי הסירה 532147
ניתן לנסח את השערת הרצף באמצעות פונקציות (של פונקציות של טבעיים) אתה באמת רוצה שאני אכתוב את זה עד הסוף?

או. קי. אזי מבין שתי מערכות האקסיומות (פיאנו עם A ובלי A) אחד מכיל סתירה והשניה משקפת את המספרים הטבעיים בצורה יותר מוצלחת.

הפרדוקס של ברי הוא לא כזה פרדוקס מוצלח (עם ברי הסליחה) אני לא חושב שמישהו חוקר אותו ברצינות. יש לעומת זאת היגדים שכן ניתן באמצעות ניחוש מושכל להגיד אם הם נכונים או לא.
כ''ג יורדי הסירה 532148
למען האמת, אני לא בטוח שאפשר לנסח אותה כך. נראה לי שהכי טוב אם תפנה אותי לספר טוב שדן בנושא.

מה זאת אומרת "מכיל סתירה"? כל הרעיון כאן הוא ש-A לא תלוי באקסיומות, ולכן האקסיומות עם A או עם שלילת A הן בעצמן חסרות סתירה (אם האקסיומות היו מלכתחילה חסרות סתירה, כמובן). אני מסכים שאחת משתי המערכות הללו "משקפת את הטבעיים בצורה יותר מוצלחת"; זה גם מה שאני אומר כל הזמן.

להזכירך, כל הדיון כאן התחיל מכך ש"התקוממת" על דרך הטיפול שלי בפרדוקס של ברי (שהייתה בערך כזו "הפרדוקס של ברי הוא לא כזה פרדוקס מוצלח; בואו נראה מה כן אפשר לקבל אם מנסחים בצורה מדוייקת יותר את מה שהוא מדבר עליו").
כ''ג יורדי הסירה 532155
בוא ניקח לדוגמה את השערת גולדבך יתכן שלא ניתן להוכיחה או להפריכה באמצעים שלנו אבל אילו היינו עוברים מספר מספר ובודקים אז או שבסופו של דבר היינו מגיעים להפרכה או שלא. אם לא זה אומר שההשערה נכונה ובפיאנו עם שלילתה יש סתירה.

לא התקוממתי, טענתי שאני לא אוהב את הגישה הכללית.
כ''ג יורדי הסירה 532156
אני לא מבין מה אתה מנסה לומר עם גולדבך כרגע. אם גולדבך אכן אינה נכונה, אז קיימת לה הפרכה מפיאנו, ולכן פיאנו + "גולדבך נכונה" היא אכן בעלת סתירה, אבל אנחנו בכלל מדברים על מקרים שבהם A לא ניתן להוכחה/הפרכה מהאקסיומות שאליהן מוסיפים אותו.
כ''ג יורדי הסירה 532157
דיברתי על מקרה שהשערת גולדבך נכונה ולא ניתן להוכיח אותה.
כ''ג יורדי הסירה 532159
במקרה זה היא לא נובעת מהאקסיומות, ולכן אם נוסיף אותה או את שלילתה לאקסיומות לא נקבל סתירה.
כ''ג יורדי הסירה 532160
או.קי. זוהי נקודה חשובה ואני שמח שהגענו אליה.
למושג סתירה יש שתי משמעויות המשמעות הראשונה היא שאתה לוקח שתי משפטים ובאמצעות החוקים הבסיסיים של הלוגיקה אתה מגיע לסתירה פשוטה (נניח 1=0) המשמעות השניה היא שתי משפטים סותרים. עכשיו ניתן לכתוב תוכנת מחשב די פשוטה שתעבור על כל המספרים ותבדוק האם השערת גולבך נכונה עבורם, אם השערת גולבך שיקרית התוכנה תעצור בשלב מסוים. אם היא לא תעצור זה אומר שהשערת גולדבך נכונה ושלילתה יחד עם פיאנו היא מובילה לסתירה.
כ''ג יורדי הסירה 532161
אם היא לא תעצור תוך כמה זמן?
the difficult we do at once 532164
אם המחשב שלך מהיר, אז תוך אינסוף. אם הוא איטי זה יקח קצת יותר זמן.
חסם טבעי 532272
עד שיהיה עדכון חלונות ותצטרך לעשות ריסטארט.
כ''ג יורדי הסירה 532162
אני לא רואה שום הבדל בין שתי המשמעויות שלך (אם כי לא ברור לי מה כוונתך ב-"שני משפטים סותרים" - בעיני פשוט מדובר בשני משפטים שאם נוסיף אותם למערכת האקסיומות שלנו, נוכל להוכיח ממנה דבר והיפוכו גם אם קודם לא יכלנו). את מה שאתה מנסה לומר בעניין התוכנה אני לא מבין - התוכנה לא מחוייבת לעצור, ואם היא לא עוצרת לא בהכרח נוכל לדעת את זה. סתירה תוכל להיות רק אם אקסיומות פיאנו יוכלו *להוכיח* שהתוכנית לא תעצור אף פעם; ובמקרה זה, אקסיומות פיאנו *הוכיחו* שהשערת גולדבך נכונה, ולכן ברור שהוספת שלילת השערת גולדבך לאקסיומות תניב סתירה.
כ''ג יורדי הסירה 532169
בוא נניח שהמכונה לא עוצרת אזי המשפט ''המכונה עוצרת'' הוא שקרי. השאלה אם אנחנו יודעים את זה או אם אנחנו יכולים להוכיח את זה היא שאלה אחרת.
כ''ג יורדי הסירה 532182
הוא שקרי - איפה? במודל של המספרים הטבעיים הוא כמובן שקרי, אבל זה אותו הדבר כמו שהמשפט "השערת גולדבך שגויה" הוא שקרי. במודל הלא-סטנדרטי של הטבעים הוא דווקא אמיתי - זה מעיד על החולשה של השפה שלך, שלא באמת מסוגלת להבדיל בין המודל הסטנדרטי והמודל הלא סטנדרטי.
כ''ג יורדי הסירה 532188
איך חזרנו למודלים?
הרי את התוכנית הייתי יכול לכתוב בruby שפועלת על קובנטו ולחבר את המחשב לפעמון שיצלצל כשהיא מסיימת. אם השערת גולדך שגויה הפעמון לא יצלצל. איך זה קשור למודל לא סטנדרטי?
כ''ג יורדי הסירה 532190
אם השערת גולדבך נכונה הפעמון לא יצלצל, אבל מתי אני אוכל להגיד למחשב "טוב, תפסיק, שוכנעתי"? אף פעם לא. אז איך תוכנית הרובי שלי קידמה אותי?
כ''ג יורדי הסירה 532192
אף פעם לא תשתכנע. אבל זאת לא הנקודה, הנקודה היא שהמשפט ''הפעמון יצלצל'' הוא שיקרי. וזה לא קשור לא לאקסיומות ולא למודלים.
כ''ג יורדי הסירה 532194
מה שאתה מפספס כאן הוא שאת המשפט הזה צריך לנסח פורמלית בשפה של מערכת ההוכחה שלנו, אחרת לא אמרת שום דבר...

בוא ננסה לעשות שוב סדר בדברים. מה בעצם הטענה שאתה מנסה לקדם עם כל עניין הפעמון הזה?
כ''ג יורדי הסירה 532195
יכול להיות שאני מפספס משהו, אבל מכיוון שזה בערך הנושא העיקרי שאנחנו דנים עליו בכל זאת אני מצפה לאיזה הסבר.

אני בכל מקרה לא מבין למה צריך לנסח פורמלית את העובדה שהפעמון יצלצל, יש איזשהו גבול לדברים שצריך פורמליסטיקה בשבילם, ולהגיד אם פעמון יצלצל או לא זה מספיק פשוט בשביל שאני לא אצטרך פורמליסטיקה.

והטענה היא פשוטה: אם מניחים את אקסיומת פיאנו ושהשערת גולדבלך נכונה אזי אקסיומת פיאנו בתוספת שלילת השערת גולדבלך תוביל אותנו לסתירה.
כ''ג יורדי הסירה 532198
סליחה שאני מתערב, אבל לא הבנתי את הטענה שלך.

הנכונה במשפט - "אם מניחים את אקסיומת פיאנו ושהשערת גולדבלך נכונה" אומר:
1. "נובעת לוגית מאקסיומות פיאנו".
2. "אקסיומה בפני עצמה".
3. "מתקיימת עבור כל המספרים הטבעיים אבל לא לא ניתנת להוכחה לוגית על ידי אקסיומות פיאנו".
4. "מתקיימת עבור מערכות פיזיות שניתנות לתיאור על ידי מערכת שמקיימת את אקסיומות פיאנו"
5. "משהו אחר".
כ''ג יורדי הסירה 532203
האפשרות הרביעית. והדוגמה עם rubby והפעמון היא בדיוק אותה מערכת פיזית.
כ''ג יורדי הסירה 532206
נראה לי שאתה וגדי מדברים על דברים שונים לגמרי. בכל מקרה, סליחה שהתערבתי.
כ''ג יורדי הסירה 532208
להפך, טוב שהתערבת.
כ''ג יורדי הסירה 532199
אני כמעט מסוגל לענות על השאלה שלך (האמת, אני חושב שכבר עניתי קודם, אבל ננסה שוב) - רק תגיד לי את כוונתך המדוייקת ב"סתירה".

(ואני אסביר: "סתירה" כפי שאני מכיר אותו הוא מושג פורמליסטי. פירושו שמערכת ההוכחה מסוגלת להוכיח דבר ואת שלילתו. לכן מראש אנחנו מוגבלים לדבר על טענות שניתנות לניסוח במסגרת השפה של המערכת).
כ''ג יורדי הסירה 532209
בהמשך לתגובה שלי לאלמוני הכוונה היא שהמערכת הפיזית מתנהגת שונה מהתחזיות.
כ''ג יורדי הסירה 532211
לא ראיתי שמישהו חזה תחזיות.

נראה לי שהאלמוני צודק. אני אמנם חושב שאני מבין על מה אתה מדבר, אבל בד בבד גם חושב שזה לחלוטין לא קשור לכל מה שדיברנו עליו עד כה. אולי עדיף לסיים את הדיון כאן, או לאפס אותו ולהבהיר יותר במדוייק מה אנחנו מנסים לומר.
כ''ג יורדי הסירה 532212
אני חזיתי שהפעמון יצלצל.

ואם אתה מבין מה אני אומר אולי גם תסביר איפה בעצם הבעיה, ולמה אנחנו חייבים פורמליסטיקה.
כ''ג יורדי הסירה 532213
אמרתי שאני חושב שאני מבין על מה אתה מדבר, לא שאני מבין מה אתה בעצם מנסה לטעון. לכן הצעתי שנאפס את הדיון - כבר מזמן לא ברור לי מה הנקודה שלך.

(הנקודות שלי בכל הדיון: 1) הגדרות "אינטואיטיבות" לא משפרות את ההבנה שלנו את העולם אלא מקשות עליה; 2) המושג של "קיים" במתמטיקה הוא מורכב יותר משהאינטואיציה רומזת - כך למשל קיים מודל לתורת הקבוצות עם השערת הרצף ומודל לתורת הקבוצות עם שלילת השערת הרצף ושניהם לגיטימיים).
כ''ג יורדי הסירה 532216
האמת היא שבדרך כלל הייתי פורש מדיון כזה כבר מזמן, אתה העלת את הנקודות שלך, אני העלתי את שלי, יקרא הקורא הנבון וישפוט.

אבל פה נראה לי שיש פער בינינו שאני (ונראה לי שגם אתה) באמת מנסים לגשר עליו, ואני חושב שאם באמת נצליח להבין איפה הבעיה הדיון יתקדם. אבל אם נראה לך שאנחנו טוחנים מיים אפשר לסיים פה.
כ''ג יורדי הסירה 532217
אני שוב אומר - אני פשוט לא מבין מה הטענה שלך. אם תגיד אותה, אולי יהיה על מה לדבר.
יש אמת מעבר למילים. 532220
טענתי היא בפשטות שבהינתן אוסף אקסיומות יש דברים שהם נכונים לגביהים למרות שלא ניתן להוכיח אותם בצורה צורנית.

לדוגמה אם יש לי שתי פונקציות (במחשב): אחת שאומרת אם מספר אחד גדול מהשני והשניה שלוקחת מספר ומוסיפה לו אחד אני לא צריך את הנחת האינדוקציה כדי להבין שלכל מספר n+1>n.
יש אמת מעבר למילים. 532222
כדי להראות שלא צריך את הנחת האינדוקציה, צריך גם להראות שלא השתמשת בה גם באופן סמוי. איך בדיוק הצלחת לבנות פונקציה שמוסיפה 1 לכל מספר נתון?

בתור התחלה: מהו בדיוק מודל החישוב שלך? מחשב רגיל? אם אני אקח מספר מספיק גדול, הוא לא ייכנס בזכרון של המחשב.
יש אמת מעבר למילים. 532225
אפשרות ראשונה n++ (או המקבילה בrubby) אפשרות שניה באמצעות פורים על הקלט.

אתה יודע מה אני אסתפק במספרים שנכנסים בMB זיכרון. אם תצליח להוכיח את המשפט על קלטים כאלה בלי להשתמש בהנחת האינדוקציה אתה כנראה אדם הרבה יותר משועמם ממה שתיארתי לעצמי.
יש אמת מעבר למילים. 532229
א. לשפה קוראים רובי, ובאנגלית Ruby. תוכל למצוא פרטים נוספים ב: http://www.ruby-lang.org/ ר' גם http://tryruby.org/ .
למזלך הגדרתה (או לפחות המימוש הסטנדרטי שלה) לא סובלת מ־overflow של מספרים. בהרבה שפות מחשבים מקובלות, היית נופל כבר כאן.

ב. פעולת ה־++ של רובי לוקחת צירוף ביטים מסויים שאמור לייצג את n ומחזירה צירוף ביטים מסויים שאמור לייצג את n+1. אתה בטוח שהפעולה כתובה נכון? תדע להבחין בין תוכנה דומה לתוכנה שמדי פעם (לא מגלה לך את התדירות) מכניסה שגיאה?

ג. אם אתה מגביל את עצמך רק למספרים שנכנסים בזכרון של המחשב מהדור הנוכחי, הרי ש"ההוכחה" שלך לא תהיה תקפה עבור המחשבים של השנה הבאה (ועבור המחשבים החזקים הרבה יותר שנמצאים כבר היום במקומות שוננים). נראה לי מאוד לא משכנע.

ד. עכשיו נסה לשכנע אותי שלכל מספר יש ריבוע. פתאום הגבול של הזכרון משמעותי בהרבה. לא הצלחת לשכנע שלכל מספר יש ריבוע? חבל, יש חלקים מעניינים ושימושיים למדי במתמטיקה שמסתמכים על כך.

ה. צודק, אני משועמם. אתה לא משועמם?
יש אמת מעבר למילים. 532231
ב. למעשה, ברובי אין פעולת ++.

ועכשיו שברתי את שיא הנטפוק האיילי של כל הזמנים.
יש אמת מעבר למילים. 532233
א. תודה
ב. מעולם לא ראיתי איך תוכנת רובי כתובה, אני משער שאם היא לא כתובה יותר מדי מוזר אני אדע להגיד אם היא נכונה וגם אם לא, לא מדובר שקשה מדי לכתוב גם באסמבלר.
ג. בסדר, זה לא כאילו ההוכחה הזאת באמת חשובה ( אני מניח שאתה לומד שn+1>n בתואר השני או משהו כזה).
ד. גם ההוכחה הרגילה שלכל מספר יש ריבוע היא די מסובכת אבל זה לא הענין.
ה. לנהל ויכוחים לא נגמרים עם תש"חיסט? כן. להוכיח שn+1>n בלי להשתמש בהנחת האינדוקציה? זה לא. גם לי יש גבולות.
יש אמת מעבר למילים. 532237
ב. לא נכון. לא ידוע אלגוריתם כללי לבדיקת נכונות של תוכנית

(ניטפוק קטן: מכיוון שכמות הזכרון במודל ה"מוגבל" שלנו מוגבלת, יש בעיקרון אפשרות לעבור על כל המצבים האפשריים. אולם זה ייקח המון זמן, ולא נראה לי שתזכה לסיים בדיקה אחת כזו בחייך. וגם אם היית מסיים, מספיק היה לי להוסיף למחשב תא זכרון אחד כדי לסבך לך שוב מחדש את החיים).

אתה מאמין למה שכתבתי כאן?

ג. (וכל השאר) מה שלא ברור לי הוא מה שיש לך נגד הפורמליזם. הניטפוקים שלי מתבססים על־כך שאתה מסרב להעזר גם גם במקומות שהוא מועיל. אני לא רוצה תוכנית ש"עובדת במספרים קטנים בלבד", או ש"עובדת בהסתברות גבוהה"‏1. אני רוצה תוכנית שעובדת.

1 ליתר דיוק, תוכנית שלפעמים צודקת, בהסתברות ידועה, עדיפה על כלום, ויש גם לה שימושים. אבל זה מחייב יתר מאמץ וזהירות. אבל זה שוב עוד ניטפוק מיותר.
יש אמת מעבר למילים. 532240
א.לא טענתי שיש לי אלגוריתם, טענתי שאני אדע.

וכן אני מאמין.
ג. זה לא נכון שאני מסרב להיעזר בפורמליזם, מכיוון שאני לא איש תורת הקבוצות כל מה שאני עושה הוא פורמלי (זאת אומרת בתיאוריה) אני מתנגד להיגד כאילו הדבר היחידי שיש לי הוא משפטים וגרירות. יש דברים שהם נכונים בלי קשר למשפטים.
יש אמת מעבר למילים. 532247
א. אם מסקירה של תוכנית תדע האם היא נכונה או לא, נראה לי שיכולותיך עוברות בהרבה את תוכניתן הממוצע. או ליתר דיוק: לא ברור לי אם קיים תוכניתן שיכול להשתוות לך. אפילו האדמו"ר דונלד קנות' [ויקיפדיה] שלימד אותנו שתוכנית מדבגים בסבלנות עם נייר ועפרון.

בתור התחלה, אתה מוזמן לעזור לפתור בעיות פתוחות במימוש הסטנדרטי של רובי:
ג. משפטים פורמליים אינם הדבר היחיד בעולם. חשוב מאוד לדעת ליישם אותם בתבונה בעולם האמיתי. בהתחשב בחישובים המסובכים שמחשבים עושים יום־יום (ולו כדי לכתוב את ההודעה הזו) נוח לי מאוד להסתמך על משפטים פורמליים במקרה הצורך.

בינתיים הצלחת להעלות לא מעט טענות שנראו לך נכונות והתבררו כשגויות. אולי יש משהו בפורמליזם.
יש אמת מעבר למילים. 532249
א. לא כל תכנית, אבל את היישום של פלוס 1 אני כנראה אצליח לזהות. וחוץ מזה מדובר בבערך שלוש שורות באסמבל כך שאפילו אני יכול לכתוב את זה.
ג. גם לי נוח להסתמך על משפטים פורמליים, זה לא סותר את מה שאמרתי.
יש אמת מעבר למילים. 532250
א. זה רק מוריד את השאלה לרמת הפשטה נמוכה יותר. אתה מניח שהמימוש של המעבד נכון. אתה חושב שאתה מסוגל להבדיל בין שתי מכונות וירטואליות שבאחת מהן יש באג קטן המימוש של אותו קוד אסמבלי לבין מכונה אחרת שבה אין באג כזה? (בלי לדעת מראש מה שגוי).
יש אמת מעבר למילים. 532252
לא, אני לא יכול.
מצד שני אני לא מבין מה הנקודה שלך. אתה יודע כמה מאמרים יש שכל החישובים הסטטיסטיים נעשו על ידי מחשב? ומתוכם כמה נעשו על ידי אנשים ששפת התכנות היחידה שהם מכירים זה spss ?
גם הם לא יכולים להבדיל בין קוד נכון לשגוי, אז מה?
יש אמת מעבר למילים. 532256
הם מקווים לטוב.

אבל אתה לא הצלחת לשכנע אותי בטענות מתגובה 532220. לא הצלחת לשכנע אותי שאתה יכול לספק לי הוכחה (ההוכחה שהצגת לא עובדת על מספרים גדולים מספיק). לא הצלחת להראות לי שהיא לא מסתמכת על אקסיומת האינדוקציה (גם לא ממש ניסחת את הטענה הזו בקפדנות).

הבעיה היא שהיית מצליח לספק לי את אותה הוכחה שאמורה להיות משכנעת גם כאשר היא אינה נכונה. כדי שהיא תהיה נכונה, על כל n המחשב אמור להוציא לך בחישוב ערך גדול מ־n. אם אתכנת את המחשב לשקר, זה לא יעבוד. לדוגמה: אם אני יודע מראש שתבדוק רק מליון מספרים, אני אתכנת את המעבד שאני בונה לשקר לך (לחסר 1 מ־n במקום להגדיל ב־1) בבדיקה המליון ועוד אחד. לחילופין, אני יכול לתכנת את המעבד לשקר לך במקום אקראי, ואז קיים סיכוי‏1 שתחשוב שהמחשב מאשש את טענתך, למרות שהוא לא.

אבל יש גם דרך יותר פשוטה: אני אפעיל את האלגוריתם הבא:

א. בקש מאינקוגניטו להראות את נכונות הטענה לגבי x
ב. טען: "ההוכחה לגבי המספרים עד x לא מספיקה לי - לא בדקת שהמחשב מחשבר נכון גם את הערך x+1".
ג. הגדל את x ב־1
ד. חזור ל־א'

אני מניח שקוראי האייל מכירים היטב טכניקות דומות.

1 אם כי במקרה הזה הסיכוי יכול להיות זניח למדי, אם לא נזהרים עם הפרמטרים)
יש אמת מעבר למילים. 532259
וואו כתבתי שתי שורות, והצלחת להבין אותי הפוך לחלוטין, כנראה שאני באמת מוכשר.

לא כתבתי שיש לי הוכחה או שאני יכול למצוא אחת. אמרתי שאני *מבין* ש n+1>n. כל הנקודה שלי היא שיש דברים שאני יודע שהם נכונים גם בלי הוכחות.
יש אמת מעבר למילים. 532262
זה לא נכון תמיד בשעון שלי.

הבעיה היא שמתמטיקה (גם המעשית) זימנה לנו לא מעט תוצאות לא אינטואיטיביות.

לדוגמה: הצפנה אסימטרית, נחשבה עד לשנות השבעים למשהו לא הגיוני.
יש אמת מעבר למילים. 532264
הכוונה בפונקציות שמוגדרות כמו שצריך.

ושוב האינטואיציה היא מעבר לפורמליסטיקה ומובן שניתן לטעות, זה לא סיבה לוותר עליה.
יש אמת מעבר למילים. 532437
א. סתם בשביל הכיף, הנה שפה שלא יודעת לקדם מספרים כמו שצריך (או שמא תוכניתן שלא יודע לכתוב קוד כמו שצריך)

#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

(וישאר תקוע על הערך הזה)

לפרטים נוספים:
יש אמת מעבר למילים. 532226
מה זה "נכון לגבי אקסיומות"?

אם אנחנו מדברים על מערכת אקסיומות בלוגיקה מסדר ראשון (כמו אקסיומות פיאנו, בניסוח המקובל שלהן) ואם "נכון לגבי אקסיומות" פירושו "מתקיים בכל מודל של האקסיומות", אז הטענה שלך פשוט שגויה (משפט השלמות של גדל מראה שכל טענה נכונה היא יכיחה במערכת שכזו). לכן נשאלת השאלה איפה נקודת המחלוקת שלנו - לדעתי ברור שהיא במשמעות שאתה מייחס ל"נכון לגבי אקסיומות". עד כמה שאני מבין אותך, אתה טוען ש"נכון לגבי אקסיומות" אין פירושו "נכון בכל מודל של האקסיומות" אלא "נכון במודל הספציפי של האקסיומות שאנחנו אוהבים, ושיזדיינו המודלים האחרים". עד כאן אני מדייק?
יש אמת מעבר למילים. 532230
לא, אתה לא מדייק.

נכון לגבי האקסיומות אכן פירושו נכון בכל מודל של האקסיומות.
ומשפט גדל לא אומר שכל טענה נכונה היא יכיחה (אלא אם כן יש לך הגדרה שונה משלי לנכונה). בוא נסתכל (מאוד מאוד בכללי) על ההוכחה של גדל. מה שגדל עשה הוא לקודד משפטים בפרט הוא קודד את המשפט ''משפט זה לא יכיח תחת האקסיומות של גדל''. עכשיו אם המשפט יכיח אז הוא נכון ולכן הוא לא יכיח. אז הנה משפט נכון ולא יכיח.
יש אמת מעבר למילים. 532232
אל תתבלבל בין משפט השלמות של גדל ומשפט אי השלמות של גדל. אלו שני משפטים שונים, ואפילו המשמעות של "שלמות" שונה. משפט השלמות מדבר על שלמות במובן של "כל מה שנכון ניתן להוכחה", ומשפט אי השלמות מדבר על שלמות במובן של "כל מה שניתן לניסוח ניתן להוכחה או ששלילתו ניתנת להוכחה". זה לא אותו דבר.

מה שמשפט אי השלמות של גדל מראה הוא שעבור מערכות אקסיומות מסויימות קיימים תמיד שני מודלים שונים מהותית ביחס למשפט שניתן לנסח באמצעות השפה של המערכת. בפרט, המשפט שגדל בונה הוא נכון במודל אחד, ולא נכון במודל אחר (חשוב להבין שהמשפט של גדל לא אומר טענה כמו זו שציטטת באופן מפורש; הוא אומר משהו על מספרים, ולכן הפרשנות המדוייקת של מה שהוא אומר תלויה במודל שבו הטענה מפורשת ובהתנהגות של "מספרים" בתוך אותו מודל).
יש אמת מעבר למילים. 532234
אם לקשר (באופו רופף ) לנושא המרכזי אז ויקיפדיה איתי משפט אי השלמות של גדל [ויקיפדיה] משפט רלוונטי (שמופיע כבר בהתחלה)."גדל הראה שבכל מערכת אקסיומות סופית ועשירה מספיק (כזו המכילה את אקסיומות האריתמטיקה החלשה) קיימות טענות אמיתיות שלא ניתן להוכיחן."
יש אמת מעבר למילים. 532236
לדעתי ויקיפדיה מתנסחת גרוע בנקודה הזו. "אמיתי" בהקשר הזה הוא "אמיתי במודל שמעניין אותנו", כשההנחה היא שתמיד עומד לנגד עינינו כזה (למשל, במקרה של פיאנו - המספרים הטבעיים). המשמעות בפירוש אינה "נכון בכל המודלים". אם אתה מתעקש להביא את ויקיפדיה העברית כמקור, אז בערך משפט השלמות של גדל [ויקיפדיה] יש התייחסות לכך:

"גרסה פופולרית (ושגויה) של משפט אי השלמות הראשון של גדל קובעת ש"בכל תורה קיימת טענה אמיתית שאינה ניתנת להוכחה". משפט השלמות סותר במפורש את הניסוח הזה: כל משפט שהוא אמיתי (בכל מודל), ניתן להוכחה. אכן, לפי משפט אי השלמות קיימת בתורה (חזקה מספיק, דהיינו אריתמטית, אפקטיבית ועקבית) נוסחה שאינה ניתנת להוכחה (וגם לא לסתירה) - אבל אין זה נכון שנוסחה זו נכונה בכל מודל. אדרבא, לפי משפט השלמות, קיים מודל עקבי שבו היא נכונה, וקיים מודל עקבי שבו היא אינה נכונה."

דיון קצת יותר חפרני בכל עניין האמת יש בספר המוצלח של Torkel Franzen על משפטי גדל (עמ' 28 והלאה).
יש אמת מעבר למילים. 532241
הבנתי איפה הבלבול. משפט השלמות של גדל מדבר על משפטים מסדר ראשון, לעומת זאת פיאנו היא מסדר שני . תסתכל על האקסיומה השלישית במערכת פאנו [ויקיפדיה] ותראה שהיא מסדר שני. ואם תחשוב על זה קצת תראה שזה הכרחי.
יש אמת מעבר למילים. 532243
הבלבול לא כאן. פיאנו מנוסחת לרוב בסדר ראשון, כשאת אקסיומת האינדוקציה הבודדת מחליפה "תבנית אקסיומה" כללית - ומשפט אי השלמות של גדל חל גם על המערכת הזו. שוב, אם אתה מתעקש על ויקיפדיה, תעיף מבט באנגלית, בפרט בפרק של "First-order theory of arithmetic".
יש אמת מעבר למילים. 532248
"תבנית אקסיומה" היא פחות חזקה מהנחת האינדוקציה, או במילותיה של הויקיפדיה 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

ואם יש לך הוכחה של משפט אי השלמות של גדל שמנוסחת בסדר ראשון אני אשמח לראות.
יש אמת מעבר למילים. 532251
בוודאי ששפה מסדר שני היא יותר אקספרסיבית משפה מסדר ראשון. זה לא משנה את זה שכשמדברים על פיאנו, לרוב הכוונה דווקא לאקסיומות המנוסחות בסדר ראשון...

בנוגע לרפרנסים - הספר הסטנדרטי וה"יבש" שעוסק בלוגיקה הוא של מנדלסון:

אם כל מה שאתה רוצה הוא להשתכנע שמשפט גדל אכן תקף גם לפיאנו-מסדר-ראשון, פרנזן אומר זאת במפורש בספרו:

"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."
יש אמת מעבר למילים. 532299
1) מאוד מפתיע אותי שיש אוסף אקסיומות שלגביהים גם משפט השלמות וגם משפט האי שלמות תופסים, הענין דורש בדיקה מקיפה, אל תעצור את הנשימה אבל אני הולך לברר את הענין, מילניום שניים ואני מבין מה קורה.
2) בוא נסכים שאנחנו מדברים על מתמטיקה סטנדרטית, אז אוסף אקסיומות זה משפטים בשפה הכוללת סימנים לוגיים, משתנים קבועים ופונקציות ומודל הוא קבוצה המקיימת את האקסיומות. משפט מאוד בסיסי במתמטיקה (שמופיע גם בויקיפדיה) אומר שאם יש לך שתי קבוצות בכל קבוצה יש לך איבר ופונקציה ושניהים מקיימים את אקסיומת פאנו אזי יש ביניהים איזומורפיזים ולכן כל משפט לוגי שנכון לאחד נכון לשני ולהיפך לכן בפרט אם ניקח שני מודלים שמקיימים את פאנו ואחד מהם מקיים את השערת גולדבך אז גם השני מקיים אותה.
יש אמת מעבר למילים. 532302
1) אני לא מבין מה ההפתעה הגדולה. כבר ציטטתי לך את הקטע המתאים מויקיפדיה שמתייחס ל"בעייתיות" ומסביר למה לא קיימת כזו.
2) אני לא מכיר את המשפט הבסיסי במתמטיקה המדובר. לינק?

שים לב שקיים גם משפט חביב בשם לוונהיים-סקולם

שממנו עולה שאם יש לך מודל בן מניה לשפה נחמדה מסדר ראשון, אז יש לך מודל מכל עוצמה אינסופית עבור השפה הזו (ומן הסתם מודלים מעוצמות שונות אינם איזומורפיים).

אולי בשלב הזה מותר לשאול מה ההשכלה שלך בנושאים שעליהם אנחנו מדברים כאן ומהיכן היא הגיעה?
יש אמת מעבר למילים. 532303
1) טוב מה אני אגיד, אני חולק על ויקיפדיה. מקוה שזה חוקי.
2)מערכת פאנו [ויקיפדיה] בסעיף "מודלים". ומשפט לוונהיים-סקולם מדבר על שפות מסדר ראשון ולכן לא תקף למערכת פאנו.

אני מתמאטיקאי ואחד המאמרים שלי עוסק בנושא קרוב.
יש אמת מעבר למילים. 532307
1) בוודאי שזה חוקי, אלא שכאן לא מדובר במשהו שרק ויקיפדיה טוענים.

2) אחזור שוב על מה שכבר אמרתי: אני מדבר כאן כל הזמן על הניסוח של פיאנו בלוגיקה מסדר ראשון (שעבורו תכונת הקטגוריות איננה מתקיימת).

3) להגיד שאתה מתמטיקאי לא עונה ממש על השאלה שלי. תשובה טובה תהיה למשל מספר ספרים/מאמרים על הנושא שעליהם אתה מתבסס.
יש אמת מעבר למילים. 532309
2) אתה טענת שאם לא קיימת הוכחה להשערת גולדבך אזי קיימים שתי מודלים למספרים הטבעיים שאחד מקיים את השערת גולדבך והשני לא.
נניח שאנחנו מדברים על מודלים שמקיימים פאנו, מה אתה טוען?
3) מהפשוטים יש את הספר של האוניברסיטה המשודרת על גדל שאומר במפורש שלפי גדל יש משפטים נכונים שלא ניתן להוכיחם.
חוץ מזה יש ספרים קלאסיים על לוגיקה מתמטית שאני לא זוכר עכשיו במדויק את שמותיהים וגם אי אפשר לצטט אותם כי כל משפט שלהם חצי מהמשפט זה סימונים שהם הגדירו קודם.
יש אמת מעבר למילים. 532311
טוב, אני חושב שזה זמן טוב לסיים בו. עם כל הכבוד לספר של ארנון אברון (ויש כבוד - ספר מעולה מסוגו), נראה לי שלהזכיר רק אותו במפורש זה לא רציני, ואני מקבל את התחושה שגם המשך הדיון יהיה טחינת מים.
יש אמת מעבר למילים. 532397
טוב, נראה לי שהבנתי מה קורא פה והייתי רוצה לתמצת את המסקנות, כמובן שכל אחד שחושב שאין טעם להתייחס למישהו שמצטט את אברון, מוזמן לא לקרוא.

1) מעכשיו נשתמש בהגדרות של גדי (שהם עצם ההדרות הבסיסיות של הלוגיקה המתימטית) אז שפה זה אוסף של סימנים המייצגים קבועים, יחסים ופונקציות. משפטים הם משפטים לוגיים ומודל היא קבוצה שבה הקבועים המשתנים והפונקציות נקבעים.
2) משפט השלמות של גדל טוען שאם יש לנו שתי קבוצות בנות מניה של משפטים מסדר ראשון ולא ניתן להוכיח או להפריך שהקבוצה הראשונה גוררת את השנייה אזי קיימים שתי מודלים אחד שבו הקבוצה הראשונה
מקיימת והשנייה לא והשני שבו שתי הקבוצות מתקיימות.
3) משפט האי שלמות הראשון של גדל אומר שאם יש לנו מערכת אקסיומות מספיק עשירה (ובתור שתי דוגמאות חשובות ניקח את אקסיומות צרמלו פרנקל לתורת הקבוצות ופיאנו למספרים הטבעיים) אזי קיים משפט שלא ניתן להוכיחו או להפריכו, המסקנה של המשפט הזה מתחלקת לשניים
א) באקסיומות של צרמלו פרנקל נקבל (כתוצאה ממשפט השלמות) שקיימים שתי מודלים אחד שבו המשפט מתקיים והשני שבו הוא לא.
ב) בפיאנו נקבל (עקב המשפט הקטגורי) שקיים משפט שנכון בכל מודל אך שלא ניתן להוכיחו או להפריכו.
4) חשוב להבין שמשפט השלמות של גדל לא מסיים את הסיפור. הוא בעצם מעביר את הבעיה מאקסיומות למודלים, אם בתור מודל לתורת הקבוצות המוכלות בממשיים ניקח את קבוצת הממשיים איחוד קבוצת החזקה של הממשיים ונגדיר "איבר ב" כאיבר ב אזי יש לנו מודל ועכשיו אנחנו יכולים לשאול: האם במודל הזה אנחנו יכולים להוכיח או להפריך את השערת הרצף? (רמז,לא).
יש אמת מעבר למילים. 532400
הבהרה: לצטט את אברון זה אחלה. כשנכנסים לדיון על עומק הפרטים (שאברון במוצהר נאלץ לחפף בהם כי הוא כותב ספר לציבור הרחב), להביא אותו בתור המקור הראשי ולא לציין במפורש שום מקור אחר זה לא רציני.

(2 הוא לא משפט השלמות של גדל, אלא נראה כמו מעין ניסוח לא מוצלח של משפט אי השלמות הראשון; 3ב' שגוי ונובע מבלבול שלך בין פיאנו מסדר ראשון שעליה חל משפט אי השלמות, ופיאנו מסדר שני שהיא קטגורית ולא עליה דיברתי)
יש אמת מעבר למילים. 532401
2) מדובר אכן בניסוח של משפט השלמות בניסוח הכי חזק שניתן.
3ב. משפט אי השלמות הראשון אכן חל גם על פיאנו סדר שני, לדוגמה הנה הוכחה של משפט אי השלמות הראשון של גדל למספרים .http://www.maths.lth.se/matstat/staff/bengtr/mathlog...
ורק הערה לאמיצים שעדיין איתנו, מדובר אומנם בהוכחה שלמה אבל מדובר בטקסט די קריא שכמעט לא דורש ידע מוקדם. הדברים היחידים שצריך להבין זה מה זה משפט לוגי ואת העובדה (שהיום היא טריוויאלית) שניתן להצמיד לכל משפט לוגי מספר.
יש אמת מעבר למילים. 532402
משפט אי-השלמות לא חל על תורות מסדר שני (ואני לא מבין למה כוונתך ב"הוכחה של משפט אי השלמות הראשון של גדל למספרים".)

הבעייה עם תורות מסדר שני היא בדיוק שאין להן את משפט ה*שלמות* - אין לנו (ולא יכול להיות לנו) מושג סינטקטי של "הוכחה" בתורות כאלה. במילים אחרות, אוסף המשפטים הנכונים של תורה כזו אינו ניתן אפילו למנייה רקורסיבית. מכאן יוצא שאי-אפשר אפילו *לנסח* את משפט אי-השלמות לתורות כאלה, כיוון שהוא דן בדיוק ביכולת להוכיח סינטקטית משפט או את שלילתו.

משפט אי-השלמות הראשון תקף, כמובן, לכל תורה מסדר ראשון, כולל תורות של "מספרים", של קבוצות, ושל זברות ורודות.

אם מה שמעניין אותך זו האמת לגבי מספרים טבעיים - ונדמה לי שכך הוא - אז אתה יכול כמעט לשכוח מכל הנ"ל ולהתרכז בתוצאה פשוטה וקונקרטית כמו: אין אלגוריתם היכול להכריע אם למשוואה דיופנטית נתונה יש פתרון. תוצאה זו מקיפה כל שיטה להוכיח טענות על המספרים הטבעיים - תהא זו דרך תורה מסדר ראשון, מסדר שני, מסדר שלישי או מה שלא יהיה.

לגיטימי להמשיך לתהות האם נובע מכך שיש טענות על הטבעיים אשר "אין להן ערך אמת". אני אישית איני סבור כך (ויש באייל כמה דיונים בנושא הזה). השערת גולדבך איננה מועמדת טובה לטענה כזו (מהיותה פסוק מטיפוס פאי-‏1, כלומר שאם אינה נכונה כל תורה מינימלית מסוגלת להוכיח זו).
יש אמת מעבר למילים. 532422
משפט השלמות לא חל על תורות מסדר שני אבל משפט אי השלמות הראשון כן חל. קודם כל ניסוחו: קיים משפט לוגי בשפה של מערכת פאנו שלא קיימת לו הוכחה, מכיוון שההוכחות התקפות דוקא כן ניתנות למניה רקורסיבית מה שאתה טוען הוא בסך הכל הוכחה אחרת למשפט. לגבי ההוכחה כבר נתתי pdf.

לגבי האלגוריתם, קצת עצוב לי לבשר לך את זה אבל עשית את אחת הטעויות הבסיסיות באלגוריתמיקה, יש אלגוריתם, מבין שתי האלגוריתמים "כן" ו"לא" אחד מהם הוא הפיתרון המבוקש.
יש אמת מעבר למילים. 532423
הופס - תגובה אחת וכבר אני מצטער שהצטרפתי לדיון. על לא דבר!
יש אמת מעבר למילים. 532424
מצטער שחשדתי בכשרים, בדיוק חשבתי שאולי התכוונת להגיד אלגוריתם שמקבל כל משוואה דיופנטית ועל משוואה ספציפית אומר אם כן או לא.
יש אמת מעבר למילים. 532427
טאגליין!
יש אמת מעבר למילים. 532428
איזה כיף זה לאנשי המתמטיקה לעומת אנשי מדעי הרוח.
  יש אמת מעבר למילים. • דרור
  יש אמת מעבר למילים. • האייל האלמוני
  יש אמת מעבר למילים. • דרור
  you don't know what you've got till its gone • ראובן
  יש אמת מעבר למילים. • אלון עמית
  יש אמת מעבר למילים. • יהונתן אורן
  יש אמת מעבר למילים. • גדי אלכסנדרוביץ'
  יש אמת מעבר למילים. • יהונתן אורן
  יש אמת מעבר למילים. • גדי אלכסנדרוביץ'
  יש אמת מעבר למילים. • יהונתן אורן
  יש אמת מעבר למילים. • גדי אלכסנדרוביץ'
  יש אמת מעבר למילים. • יהונתן אורן
  יש אמת מעבר למילים. • אלון עמית
  יש אמת מעבר למילים. • יהונתן אורן
  יש אמת מעבר למילים. • גדי אלכסנדרוביץ'
  יש אמת מעבר למילים. • אלון עמית
  יש שקשוקה מעבר לביצים • סייעתא דשמיא
  טוב, נמאס לי להיות מרטיר • אינקוגניטו
  שיבושם לך • איזור חסר אגו במוחו של אלון עמית
  שיבושם לך • האייל האלמוני
  שיבושם לך • אלון עמית
  שיבושם לך • גדי אלכסנדרוביץ'
  שיבושם לך • אלון עמית
  שיבושם לך • אינקוגניטו
  שיבושם לך • גדי אלכסנדרוביץ'
  שיבושם לך • אלון עמית
  שיבושם לך • גדי אלכסנדרוביץ'
  שיבושם לך • אלון עמית
  שיבושם לך • אינקוגניטו
  שיבושם לך • אלון עמית
  שיבושם לך • אלון עמית
  שיבושם לך • אינקוגניטו
  יש אמת מעבר למילים. • אלון עמית
  יש אמת מעבר למילים. • ידידיה
  יש אמת מעבר למילים. • אלון עמית
  יש אמת מעבר למילים. • אינקוגניטו
  יש אמת מעבר למילים. • גדי אלכסנדרוביץ'
  כ''ג יורדי הסירה • גדי אלכסנדרוביץ'
  כ''ג יורדי הסירה • זהריקו
  כ''ג יורדי הסירה • אינקוגניטו

חזרה לעמוד הראשי

מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים