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

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

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

עמדתי היא פשוטה: אין כל פער. כל סוגי הידיעה, וכל רמות הביטחון, שיש לבני-אדם בקשר לטענות מתמטיות ואחרות, ניתנים להשגה באותה רמה של הצלחה ע"י מכונות מספיק משוכללות.
317051
"*שתי* שגיאות נפוצות נוספות הן הטענות "יש משפטים שבני־אדם *רואים שהם אמיתיים*, אבל תורות פורמליות לא יכולות להוכיח" ו"יש משפטים שבני־אדם רואים שהם אמיתיים, ומחשבים לא יוכלו לראות זאת לעולם"... האם יש באמת משפטים שאנחנו רואים שהם אמיתיים, אבל *אי־אפשר להוכיח אותם פורמלית*? כותב שורות אלה, אישית, משוכנע שאין;"
מלכתחילה שאלתי על הטענה האחרונה שלך, שלמיטב הבנתי התייחסה ל"שגיאה" הראשונה שאתה מזכיר כאן, ואיננה מתייחסת למכונות כלל. האם לא די לי בלוקאס ובפנרוז, שעליי לסבול גם מכונות לא רצויות? או שכוונתך במשפט האחרון בציטוט היא ש"להוכיח פורמלית" פירושו "להוכיח בעזרת מכונות"? לא ברור העניין הזה.
317100
מה שאפשר להוכיח פורמלית, אפשר להוכיח ע"י מכונה, כן. איזה עניין לא ברור? (לא להתרגז, אני שואל בכנות, לא בכעס).
317113
(האלמונית מורטת כעת את שערה שלה בייאוש).
האייל האלמוני (יום שישי, 15/07/2005 שעה 14:05)
במאמרך מופיעה בפסקה הבאה:
"שתי* שגיאות נפוצות נוספות הן הטענות "יש משפטים שבני־אדם *רואים שהם אמיתיים, אבל תורות פורמליות לא יכולות להוכיח" ו"יש משפטים שבני־אדם רואים שהם אמיתיים, ומחשבים לא יוכלו לראות זאת לעולם"... האם יש באמת משפטים שאנחנו רואים שהם אמיתיים, אבל אי־אפשר להוכיח אותם פורמלית? כותב שורות אלה, אישית, משוכנע שאין;".
למיטב הבנתי, פירושה של הפסקה הוא:
יש (בין היתר) *שתי* טענות שגויות ביחס למשפט גדל:
1. "יש משפטים שבני־אדם *רואים שהם אמיתיים, אבל תורות פורמליות לא יכולות להוכיח".
2. "יש משפטים שבני־אדם רואים שהם אמיתיים, ומחשבים לא יוכלו לראות זאת לעולם".
אם הבנתי נכון, מדובר בשתי טענות *שונות*. אני מתייחסת לטענה מס' 1.
כעת, בהמשך אתה אומר (טענה 3, לא שגויה כנראה): "האם יש באמת משפטים שאנחנו רואים שהם אמיתיים, אבל אי־אפשר להוכיח אותם פורמלית? כותב שורות אלה, אישית, משוכנע שאין;".
כיוון שבטענה מס' 1 ובטענה מס' 3 אין מלה המרמזת על מכונות, למיטב הבנתי לא מדובר בהן על מכונות (האם אני טועה?). ומאותה סיבה, נדמה היה לי שטענה מס' 3 באה להפריך את טענה מס' 1. דהיינו (טענה שתכונה להלן טענה 4): "כל משפט שאנשים רואים שהוא אמיתי, ניתן להוכחה בתורות פורמליות."
אם עד כאן טעיתי, אנא האר את עיניי. אם לא - אני מנסה להבין את טענה מס' 4, ושואלת:
האם ברור לך שכל משפט שאנשים רואים שהוא אמתי הוא אכן אמתי?
האם כל משפט אמתי יכיח בתורות פורמליות?
טענות 317114
אם ניתן להוכיח טענה פורמלית, אז גם מכונה יכולה להוכיח אותה, ולהפך. טענות 1,2,4 שקולות (וטענה 3, כמובן, הפוכה להן).
טענות 317115
לא התייחסתי כלל לטענה 2.
וטענה 4 הפוכה מטענה 1.
317119
לי לא ברור שכל משפט שאנשים רואים שהוא אמיתי הוא אכן אמיתי. אפשר להיכנס כאן לדיון על מה זה "רואים" ומה זה "אמיתי", אבל הטענה המקורית שלי היא הרבה יותר פשוטה: אחרים - לוקאס, סרל, לא אני - טוענים שיש משפט פורמלי בתורת המספרים שאנו רואים שהוא נכון ומערכות פורמליות לא יכולות להוכיח. אילו היה זה נכון, זה היה טיעון מסקרן לגבי שאלת המוח האנושי, אבל זה לא.

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

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

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