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

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

__

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

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

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

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

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

---

(סיגמה-פי זה איך שהמורה שלי קרא למערכת שמבוססת על האקסיומות של פיאנו וחלה על המספרים הטבעיים. זה מה שאתה קורא PA?)

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

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

__

PA זה Peano Arithmetic, כן.

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

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

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

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

חסר לי גם הפאנץ'-ליין של הטיעון. נראה לי שסיימת בנקודה בה הראית שהאדם-כמערכת-פורמלית לא יכולה להוכיח משהו (את Gp). אז?
בקיצור 314349
א. אתה אומר שהאדם שקול למ"ט. מ"ט שקולה למערכת פורמאלית. מכאן שהאדם שקול למערכת פורמאלית.
ב. כשאני מוכיח ש:"1+1=2" או משהו כזה, זה אומר שהאינפורמציה הזאת נמצאת בתוכי בצורה זו או אחרת, בשפה זו או אחרת. זה אומר שבשפה הפורמאלית שבה המערכת השקולה לי מנוסחת, ניתן לבטא ולהוכיח "1+1=2".
ג. אתה אומר שידע "רך", כמו המשפטים "כשחם אז מזיעים", הוא לא אמיתי או שקרי. האם ידע זה כולל את המשפט "האדם הוא מ"ט"?

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

ג. לא, הטענה על היות המוח שקול למערכת חישובית נראית לי די חד-משמעית. למה?

ד. איך הגעת למסקנה שאתה אינך PA? אתה כן יכול להוכיח את Gp? אמרת שאתה יכול לעשות זאת *בהנחה ש-PA עקבית*. יפה. זאת יכולה לעשות גם PA!

שים לב: אם PA עקבית, אז היא לא יכולה להוכיח את Gp. אבל היא כן יכולה להוכיח את "אם PA עקבית, אז Gp".

ההבדל ברור? וברור מדוע זה *בדיוק* מה שגם אתה יכול לעשות?

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

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

כיצד ניתן להוכיח שמערכת כלשהי היא עקבית? איך מוכחת עקביות PA ב-ZFC?
___

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

"אם נוכיח שלא ייתכן שהאדם הוא מ"ט השקולה למערכת לא-עקבית, אז הוכחנו שהאדם אינו מ"ט, נכון?"

לא הבנתי. למה? ובאיזה מובן של "נוכיח" אתה משתמש כאן?

"כיצד ניתן להוכיח שמערכת כלשהי היא עקבית?" - צריך לבנות לה מודל. מן הסתם בשביל לעשות זאת צריך להניח שמערכת *אחרת* היא עקבית...

"איך מוכחת עקביות PA ב-ZFC?" - ב-ZFC אפשר (בקלות) לבנות מודל ל-PA. הדרך המקובלת לעשות זאת היא להגדיר את "אפס" כקבוצה הריקה, ואת n+1 כאיחוד של הקבוצה n עם הקבוצה {n}. כמובן שיש להיזהר: ההוכחה הזו לא שווה כלום אם ZFC עצמה אינה עקבית, או אם יש לך סיבה לדחות את אחת האקסיומות של ZFC. למשל, אחת האקסיומות קרויה "אקסיומת האינסוף", והיא אומרת שיש קבוצה אינסופית; מי שלא מאמין שזה נכון, אין לו שום סיבה לקבל את ההוכחה הזו של עקביות PA. סתם, דוגמה, שנזכור מה זה "הוכחה".

__

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

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

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

בכל מקרה, אני חושב שזה חשוב מאוד. הוא בהחלט מהווה צד פורה בדיאלקטיקה שהנושא הזה נבנה דרכה.

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

אני לא חושב שאתה צריך לנסות לבחון אם הביקורת שלו על AIT היא מוצדקת או לא, אלא להיפך: לנסות לראות אם אתה מסוגל לגזור איזו מסקנה מרחיקת-לכת מ-AIT, ואז להעמיד את טיעונך למבחן. אני סבור שזה dead end, אבל בהצלחה.
בקיצור 316278
אני אשמח לנצל את ההזדמנות הזו כדי להגיד גם לך וגם לד.ק. שזה ללא ספק הדיון המהנה, המעשיר והמעניין ביותר שקראתי ב-''האייל הקורא'' עד עכשיו.
הייתי גם מחמיא מאוד על רמת ואופן הדיון אבל אני ארגיש כמו מורה...
בקיצור 316308
תודה על המחמאה, אני קצת המום מכך שעוד מישהו עקב. כל מה שאני יכול לומר הוא שזה ללא ספק הדיון בעל הכותרת הנגררת הכי מגוחכת שקראתי ב''האייל הקורא'' עד עכשיו (וקראתי הרבה).
בקיצור 316313
אתה מתכוון, הכי אוקסימורונית, לא?
בקיצור 316589
מגניב, תודה.

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

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