|
||||
|
||||
<הערת אגב> "עתידה שעשוי להיות מוחלף על ידי מחשבים" יש בדיון הזה פתיל ארוך בנושא, החל מתגובה 211565. הפרקטיקה של ההוכחות הממוחשבות לא רלוונטית לנושא. אני כמובן דיברתי על מערכת אקסיומות אפקטיבית, שמוגדרת באמצעות מכונת טיורינג. ההגדרה קיימת כבר משנות ה-20 או ה-30. אני בכל זאת אציין את דעתי: אני אינני יודע איך מחשב יחליט האם משפט כלשהו הוא "מעניין", הוכחה כלשהי היא "אלגנטית", וגם אינני יודע איך הוא יתרגם הוכחה פורמלית לשפת בני אדם. עד שהוא לא יעשה את זה, הוא יהיה חסר תועלת בתור מתמטיקאי. אם הוא יעשה את זה, הוא בוודאי יוכל לכתוב גם שיר קצר (כפי שאמר אלון באחת התגובות). מחשב שרק יפלוט את הנוסח הפורמלי של כל המשפטים האפשריים לא יהיה שונה מאלף הקופים על מכונות הכתיבה. במצב כזה, לפרנסתם של המתמטיקאים לא נשקפת סכנה מיוחדת. <\הערת אגב> "המוח שלנו חושב ומפרש את המציאות בצורה מדהימה פי כמה ממכונת טיורינג" אינני יודע למה אתה קורא "מציאות", אבל בהקשר המתמטי כדאי לדבר על מערכות אקסיומות. אם קראת את דיון 2396 אתה יודע שמערכת אקסיומות מוגדרת כפונקציה שמקבלת סדרה סופית של טענות בשפה כלשהי, ומחזירה "היקש תקף" או "היקש לא תקף" 1. כלומר, כדי שמוח האדם יעסוק במערכת אקסיומות שמחשב לא יכול לעסוק בה ("לא אפקטיבית"), הוא צריך לחשב פונקציה שאינה ניתנת לחישוב (במשמעות הפורמלית של המושג). אני לא מכיר אף פונקציה כזו שאדם מסוגל לחשב, ואני אשמח אם תראה לי אחת. "הסכמה הלינארית של אוקלידיס היא השטחה של פוטנציאל התודעה" אולי דורון ואתה מנסים להפעיל עלינו את מבחן טיורינג? אתם מנהלים איתנו דיון בכתב, מראים לנו מערכת אקסיומות שמחשב לא יכול להבין, והפלא ופלא: גם אנחנו לא מבינים. :-) "אגב לא חדשה כלל אלא בעצם בת אלפי שנים" מה הכוונה שלך כשאתה אומר שהיא "בת אלפי שנים"? אני מבין את זה כאילו היא מוכרת אלפי שנים, אבל אתה טוען שהיא נחשפת רק בימינו. אני אשמח אם תסביר את עצמך. |
|
||||
|
||||
1 הפונקציה מחזירה "צעד היקש תקף" רק בשני מקרים: (1) הסדרה היא באורך אחת, והטענה היא אקסיומה. (2) הסדרה היא באורך גדול מאחת, וקיים צעד היקש שבאמצעותו ניתן להסיק את הטענה האחרונה מהטענות הקודמות. ע"פ הגדרות אלה, "הוכחה" היא סדרה סופית של סדרות סופיות של טענות ("היקשים"), שעבור כל היקש הפונקציה מחזירה "צעד היקש תקף", וכל הנחה של היקש התקבלה כמסקנה של היקש קודם. |
|
||||
|
||||
''אני אינני יודע איך מחשב יחליט האם משפט כלשהו הוא ''מעניין'', הוכחה כלשהי היא ''אלגנטית'', וגם אינני יודע איך הוא יתרגם הוכחה פורמלית לשפת בני אדם. עד שהוא לא יעשה את זה, הוא יהיה חסר תועלת בתור מתמטיקאי.'' אייל צעיר, מחשב אינו אלא שלוחה או סוכן שלנו, ואין הוא עושה דבר שלא במסגרת שהוקצבה לו על ידנו, לכן אין טעם לדון בפתרונות כלשהם ע''י מחשב, כי כל פיתרון איננו אלא פתרון שלנו, ואין זולתנו. זה כולל כמובן את השיטה הדדוקטיבית וחוקי המשחק הפורמליים, וכל הד שנשמע מקורו בקולנו אנו ורק אנו אלה ששומעים אותו ומעניקים לשמיעה משמעות בתודעתנו. |
|
||||
|
||||
אין ספק שמחשב לא יוכל להוכיח שום דבר שאדם לא יכול להוכיח. השאלה פה היא שאלה של יעילות. גם אני יכול לחשב את המספר 45384^38276, וגם המחשב שלי יכול. משום-מה, אני אעדיף שהמחשב שלי יעשה את זה. ואם אתה עוד תכריז שזה הפתרון שלי, זה בכלל נהדר. |
|
||||
|
||||
אין ספק? |
|
||||
|
||||
תיאורטית, כל הוכחה שמחשב יכול למצוא, גם האדם היה יכול למצוא עם מספיק זמן ומספיק זיכרון. אין יתרון מהותי למחשב - רק יתרון כמותי. לכן אין שום משמעות לטענה של דורון לפיה ''המחשב הוא רק שלוחה של האדם''. אני בהחלט מסכים שההוכחה שהמחשב ימצא היא ''הוכחה אנושית'' שנמצאה בעזרת מכונה. |
|
||||
|
||||
"אין ספק שמחשב לא יוכל להוכיח שום דבר שאדם לא יכול להוכיח." אתה מתעלם לחלוטין מתגובתי, שהיא: "אין דבר כזה מחשב, כישות המנותקת ממקורה, כאשר המקור הוא תודעתנו, ותודעתנו יכולה למנף עצמה ע"י רתימת חומרי הגלם שבסביביתה לצרכיה היא. האם אתה מבין את מה שאני אומר, או שאתה מתכונן לחזור שוב על המחול חסר התובנה של אי-זיהוי עצמך ביציר כפיך? |
|
||||
|
||||
אתה זה שמתעלם מהתגובה שלי. אתה לוקח פתיל שעוסק בשימוש *פרקטי* במחשב לצורך הוכחה 1 וקושר אותו לשאלת ה"אובייקטיביות" של המחשב, שלא שייכת בכלל. האם יש לך ספק שההוכחות שהמחשב מספק הן הוכחות תקפות *ע"פ הגישה הדדוקטיבית*? 1 בניגוד לפתילים אחרים, שעסקו בהגדרה של מערכות אקסיומות באמצעות מכונות טיורינג, שבהם הרעיון שלך היה רלוונטי. |
חזרה לעמוד הראשי | המאמר המלא |
מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
RSS מאמרים | כתבו למערכת | אודות האתר | טרם התעדכנת | ארכיון | חיפוש | עזרה | תנאי שימוש | © כל הזכויות שמורות |