 |
|
 |
||
|
||||
 |
השאלות המעניינות אותי אינן האם אלגוריתם יכול לייצר הוכחה למשפט מתמטי ספציפי. ברור שהוא יכול, באופן טריוויאלי, כפי שכתבת בעצמך. מה שפחות מובן הוא: 1) האם קיים אלגוריתם שיכול לייצר את כ_ל ההוכחות שמתמטיקאים מסוגלים להפיק אי פעם (בהנתן זמן בלתי מוגבל)? 2) האם אלגוריתם המפיק הוכחה מתמטית מבין שהוא הפיק הוכחה מתמטית? לדעתי התשובות לשתי השאלות האלו הן שליליות. אלגוריתם יכול אולי לשפוט נכונות של כל הוכחה מתמטית המיוצגת באמצעות שפה פורמלית מסויימת, אולם אין שום שפה פורמלית המייצגת את כל החשיבה המתמטית האפשרית. זה נובע, כך נדמה לי, ממשפט אי השלמות של גדל. בכלל, העובדה שלא ניתן לבצע פורמליזציה של השפה, אפילו לא של השפה המצומצמת המשמשת לחשיבה מתמטית, מוכיחה את הטיעון שלי. אלגוריתמים מוגבלים לשפות פורמליות בלבד. |
 |
 |
 |
|
|
|
||
|
||||
|
לדעתי התשובה לשאלה הראשונה היא טריוואילת כן. שאלה מעט יותר מעניינת וקשה היא האם האלגוריתם ידע למיין את ההוכחות לנכונות ולא נכונות. התשובה לשאלה השנייה היא בעיתית כי לא נתת דרך עבור המתבונן לדעת מתי משהו אחר מבין. | |
|
|
|
|
|
||
|
||||
|
כמובן שהתכוונתי לאלגוריתם שיציג רק הוכחות נכונות. הוכחה שגויה כלל איננה הוכחה. האם קיים "מתמטיקאי אבסולוטי" אלגוריתמי, כזה שמסוגל לגלות את כל ההוכחות (התקפות!) שמתמטיקאים אנושיים עשויים לגלות, ולא להציג טיעונים שמכילים כשלים לוגיים או טעויות? קשה לתת הגדרה ביהוויוריסטית להבנה, משום שהבנה איננה התנהגות, אם כי היא עשויה להתבטא גם באופן התנהגותי. יש מורים, למשל, שמפתחים מיומנות בכתיבת שאלות למבחן הבוחנות עד כמה התלמידים הבינו את החומר ולא סתם שיננו אותו. לדעתי תמיד ניתן למצוא מבחן כזה, אבל אני לא בטוח עד כמה זה פשוט למצוא אותו. |
|
|
|
|
|
|
||
|
||||
|
האם לא נראה לך סביר שברגע שהוכחה קיימת, מכונה תוכל לבדוק את תקפותה? יש שיגידו שזאת *ההגדרה* של הוכחה. אם מכונה כזאת קיימת, כל מה שנותר לנו לעשות זה להזין אותה בגיבריש ולדלות מהגיבריש את ההוכחות התקפות. | |
|
|
|
|
|
||
|
||||
|
מכונה יכולה, תיאורטית, לבדוק תקפותן של הוכחות הכתובות בשפה פורמלית איתה היא יודעת לעבוד. אבל אין שום שפה פורמלית המאפשרת לקודד כל טיעון מתמטי אפשרי. הוכחות מתמטיות כתובות בעברית (או שפה טבעית אחרת), שהיא שפה יותר חזקה מכל שפה פורמלית אפשרית (למשל, היא מכילה את המטא-שפה של עצמה). | |
|
|
|
|
|
||
|
||||
|
אני חשבתי שעד שלא מעבירים הוכחה משפה טבעית לשפה פורמלית אי אפשר בעצם להוכיח כלום. | |
|
|
|
|
|
||
|
||||
|
למעשה יש מעט מאוד הוכחות מתמטיות שמנוסחות בשפה פורמלית. הסימנים המשונים של המתמטיקאים הם קצרנות, לא פורמליזציה. שפה פורמלית זה משהו מאוד ספציפי שמבוסס על הגדרת מחרוזות תווים מסויימות כאקסיומות ושורת פעולות מותרות עליהן ליצירת משפטים. הופשטטר תיאר את העניין מצויין בגא"ב. בכל אופן, גם אם צריך ואפשר להעביר כל הוכחה מתמטית תקפה לשפה פורמלית, מה שאי אפשר לעשות זה להעביר את כל ההוכחות האפשריות ל_א_ו_ת_ה שפה פורמלית. |
|
|
|
|
|
|
||
|
||||
|
אם אי אפשר, אז מחשב, שיכולת העיבוד המתמטית מוגדרת על ידי שפה פורמלית ספציפית (התלויה באלגוריתם שלו) לא יוכל להבין את ההוכחות המתמטיות שאינן ניתנות לקידוד באותה שפה. אבל לבני אדם אין מגבלה כזו. | |
|
|
|
|
|
||
|
||||
|
איך אנחנו יודעים אילו מגבלות יש לבני אדם? | |
|
|
| חזרה לעמוד הראשי |  |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |