האם ניתן להוכיח שאלגוריתם שקול למכונת טיורינג
- פותח הנושא לפטופ3
- פורסם בתאריך
גדי אלכסנדרוביץ'? זה אתה?
"זה לא מוכיח שמחר לא יהיה מודל שחזק יותר ממכונת טיורינג, אבל זו הסיבה שבגללה ניסוח פורמלי של טענות חישוביות מתייחס תמיד למכונת טיורינג ולא ל"חישובים" באופן כללי."
ניסחת בדיוק את מה הבעיה שלי! אולי מחר ימצאו מודל חישובי חזק יותר??
מתוך ויקיפדיה:
"כאמור, תזת צ'רץ' טיורינג היא סברה ולא משפט דבר העשוי להקשות על קבלתה. למעשה, התזה טוענת כי המושג "חישוב" הוא בעל משמעות אוניברסלית. למעשה, מאחר שהמתמטיקה מתעסקת בהגדרות פורמליות, ואין לנו הגדרה פורמלית אחרת לחישוב, תזת צ'רץ'-טיורינג היא ההגדרה הפורמלית של חישוב. ניתן להשתכנע בנכונות התזה עקב הנימוקים הבאים......."
http://he.wikipedia.org/wiki/תזת_צ'רץ'-טיורינג
"מודלים "קלאסיים" כמו פונקציות רקורסיביות, תחשיב למבדא ומכונות רגיסטרים הם שקולים למכונת טיורינג"
המרצה שלי אכן הזכיר זאת
"זה לא מוכיח שמחר לא יהיה מודל שחזק יותר ממכונת טיורינג, אבל זו הסיבה שבגללה ניסוח פורמלי של טענות חישוביות מתייחס תמיד למכונת טיורינג ולא ל"חישובים" באופן כללי."
ניסחת בדיוק את מה הבעיה שלי! אולי מחר ימצאו מודל חישובי חזק יותר??
מתוך ויקיפדיה:
"כאמור, תזת צ'רץ' טיורינג היא סברה ולא משפט דבר העשוי להקשות על קבלתה. למעשה, התזה טוענת כי המושג "חישוב" הוא בעל משמעות אוניברסלית. למעשה, מאחר שהמתמטיקה מתעסקת בהגדרות פורמליות, ואין לנו הגדרה פורמלית אחרת לחישוב, תזת צ'רץ'-טיורינג היא ההגדרה הפורמלית של חישוב. ניתן להשתכנע בנכונות התזה עקב הנימוקים הבאים......."
http://he.wikipedia.org/wiki/תזת_צ'רץ'-טיורינג
"מודלים "קלאסיים" כמו פונקציות רקורסיביות, תחשיב למבדא ומכונות רגיסטרים הם שקולים למכונת טיורינג"
כשאתה עובר לסמנטיקה דברים נעשים מעורפלים קצת
גם כשמדובר במתמטיקה.
אני מאוד מצטער אם לא התנסחתי באופן שמסביר את זה, אבל לי נראה שהבעיה שלך היא לא עם ההוכחות של צ'רץ' או של טיורינג אלא עם המושג הבסיסי הנקרא "אלגוריתם".
קיימים כל מיני מודלים חישוביים שהוכחו כולם כשקולים (ע"ע למבדא-קלקולוס ומכונות טיורינג).
אם אני מבין אותך נכון אתה לא באמת מאמין (כן, מאמין) כי הסמנטיקה של המושג "אלגוריתם" אכן מוצגת כראוי בעולם המתמטי על ידי למבדא קלקולוס או מכונות טיורינג - תקן אותי אם אני טועה בהבנתי את השאלה.
אם אתה כן מוכן לקבל את ההנחות שמאפשרות מעבר ממושג האלגוריתם למכונות טיורינג למשל, אני לא מבין מה בדיוק הבעיה.
אם אתה לא מוכן לקבל את ההנחות הללו, אני מציב בפניך אתגר - הראה דוגמה של אלגוריתם שלא ניתן לייצגו על ידי מכונת טיורינג או מודל חישובי שקול אחר (זה יותר קשה ממה שאתה חושב מכיוון שמודל ה RAM של מחשב שקול למכונת טיורינג).
אתה מוזמן גם להציע מודל חישובי אחר אשר מייצג את המושג "אלגוריתם" יותר טוב להבנתך ולנסות להוכיח כי אינו שקול למכונת טיורינג.
בהצלחה
גם כשמדובר במתמטיקה.
אני מאוד מצטער אם לא התנסחתי באופן שמסביר את זה, אבל לי נראה שהבעיה שלך היא לא עם ההוכחות של צ'רץ' או של טיורינג אלא עם המושג הבסיסי הנקרא "אלגוריתם".
קיימים כל מיני מודלים חישוביים שהוכחו כולם כשקולים (ע"ע למבדא-קלקולוס ומכונות טיורינג).
אם אני מבין אותך נכון אתה לא באמת מאמין (כן, מאמין) כי הסמנטיקה של המושג "אלגוריתם" אכן מוצגת כראוי בעולם המתמטי על ידי למבדא קלקולוס או מכונות טיורינג - תקן אותי אם אני טועה בהבנתי את השאלה.
אם אתה כן מוכן לקבל את ההנחות שמאפשרות מעבר ממושג האלגוריתם למכונות טיורינג למשל, אני לא מבין מה בדיוק הבעיה.
אם אתה לא מוכן לקבל את ההנחות הללו, אני מציב בפניך אתגר - הראה דוגמה של אלגוריתם שלא ניתן לייצגו על ידי מכונת טיורינג או מודל חישובי שקול אחר (זה יותר קשה ממה שאתה חושב מכיוון שמודל ה RAM של מחשב שקול למכונת טיורינג).
אתה מוזמן גם להציע מודל חישובי אחר אשר מייצג את המושג "אלגוריתם" יותר טוב להבנתך ולנסות להוכיח כי אינו שקול למכונת טיורינג.
בהצלחה
נכון , אתה צדק
"אם אני מבין אותך נכון אתה לא באמת מאמין (כן, מאמין) כי הסמנטיקה של המושג "אלגוריתם" אכן מוצגת כראוי בעולם המתמטי על ידי למבדא קלקולוס או מכונות טיורינג "
נכון. בדיוק כמו ששאלתי בכותרת הראשית של השאלה הראשית שלי: "האם ניתן להוכיח שאלגוריתם שקול למכונת טיורינג?"
"אם אתה לא מוכן לקבל את ההנחות הללו, אני מציב בפניך אתגר - הראה דוגמה של אלגוריתם שלא ניתן לייצגו על ידי מכונת טיורינג או מודל חישובי שקול אחר".
חחח לא נראה שיהיה לי זמן
אגב , אני ממש לא טענתי שהתזה לא נכונה (המתמטיקאים מאמינים שהיא נכונה), אני רק חושב שאסור לנו להסתמך עליה ללא הוכחה.
"אם אני מבין אותך נכון אתה לא באמת מאמין (כן, מאמין) כי הסמנטיקה של המושג "אלגוריתם" אכן מוצגת כראוי בעולם המתמטי על ידי למבדא קלקולוס או מכונות טיורינג "
נכון. בדיוק כמו ששאלתי בכותרת הראשית של השאלה הראשית שלי: "האם ניתן להוכיח שאלגוריתם שקול למכונת טיורינג?"
"אם אתה לא מוכן לקבל את ההנחות הללו, אני מציב בפניך אתגר - הראה דוגמה של אלגוריתם שלא ניתן לייצגו על ידי מכונת טיורינג או מודל חישובי שקול אחר".
חחח לא נראה שיהיה לי זמן
אגב , אני ממש לא טענתי שהתזה לא נכונה (המתמטיקאים מאמינים שהיא נכונה), אני רק חושב שאסור לנו להסתמך עליה ללא הוכחה.
טרול המתכנן
New member
"הוכחה" זה מושג במתמטיקה
המתאר הליך בו מגיעים מאוסף הנחות והנחות נתון למסקנה, בעזרת צעדים לוגיים.
השאלה האם ההנחות, או "הצעדים הלוגיים", תקפים או ברי-השלכה על המציאות בפועל - אינה שאלה במתמטיקה.
המתאר הליך בו מגיעים מאוסף הנחות והנחות נתון למסקנה, בעזרת צעדים לוגיים.
השאלה האם ההנחות, או "הצעדים הלוגיים", תקפים או ברי-השלכה על המציאות בפועל - אינה שאלה במתמטיקה.
נראה לי שהבנתי את לב הבעיה שלך
חשוב להבין שבמתמטיקה *אף אחד* לא "מסתמך" על התזה של צ'רץ' וטיורינג. היא לא משמשת כהנחה בשום הוכחה שהיא. הוכחות בתורת החישוביות הן תמיד של טענות מהצורה "לא קיימת מכונת טיורינג שעושה כך וכך" - כלומר, עוסקות במודל החישוב הקונקרטי שלנו.
התזה של צ'רץ' וטיורינג משמשת בדיוק למטרה אחת - להצדיק *אינטואיטיבית* את העובדה שבתורת החישוביות עוסקים במכונת טיורינג ולא במודלי חישוב אחרים. אנחנו עושים את זה כי אנחנו מאמינים שכל מה שאנחנו מבינים בתור חישוב יכול להיות מתואר בידי מכונת טיורינג. אם ההנחה הזו תיפול, אז התחום שעוסק בשאלה "מה מכונת טיורינג יכולה לעשות?" יהפוך לתת-תחום של השאלה "מה אפשר לחשב", אבל שום משפט מתמטי לא יקרוס.
חשוב להבין שבמתמטיקה *אף אחד* לא "מסתמך" על התזה של צ'רץ' וטיורינג. היא לא משמשת כהנחה בשום הוכחה שהיא. הוכחות בתורת החישוביות הן תמיד של טענות מהצורה "לא קיימת מכונת טיורינג שעושה כך וכך" - כלומר, עוסקות במודל החישוב הקונקרטי שלנו.
התזה של צ'רץ' וטיורינג משמשת בדיוק למטרה אחת - להצדיק *אינטואיטיבית* את העובדה שבתורת החישוביות עוסקים במכונת טיורינג ולא במודלי חישוב אחרים. אנחנו עושים את זה כי אנחנו מאמינים שכל מה שאנחנו מבינים בתור חישוב יכול להיות מתואר בידי מכונת טיורינג. אם ההנחה הזו תיפול, אז התחום שעוסק בשאלה "מה מכונת טיורינג יכולה לעשות?" יהפוך לתת-תחום של השאלה "מה אפשר לחשב", אבל שום משפט מתמטי לא יקרוס.
לא בדיוק הבנת את הבעיה
"הוכחות בתורת החישוביות הן תמיד של טענות מהצורה "לא קיימת מכונת טיורינג שעושה כך וכך" - כלומר, עוסקות במודל החישוב הקונקרטי שלנו"
כן , אני יודע שכל הוכחה מתייחסת למודל של מכונת טיורינג. השאלה שלי היא האם משליכים הוכחות שמתייחסות למכונת טיורינג על טענות שמתייחסת למושג חישוב או אלגוריתם?
אם נחזור לשנת 1900 , בשנה בה הילבט הציג את הבעיה העשירית שלו , או לשנת 1928 בה הציג את האתגר שלו שזכה לשם Entscheidungsproblem , (והיה הבעיה הבאה:
למצוא אלגוריתם אשר בהינתן טענה כלשהי שמנוסחת בשפה הפורמלית של הלוגיקה (לוגיקה מסדר ראשון), לקבוע האם היא נכונה או לא (כאשר "נכונה" כאן פירושו "נכונה בכל עולם שמקיים את האקסיומות של הטענה") הרי שהילברט מבקש בשפה של ימינו אנו למצוא "מודל של מכונת חישוב כלשהו" שתפתור את הבעיות הנ"ל.
למעשה , ופה בדיוק אני רוצה לשמוע את דעתכם , כדי לטעון למשל שהאתגר של 1928 (ה-Entscheidungsproblem) בלתי אפשרי , צריך להוכיח שלא קיים אף מודל חישובי שיכול לחשב זאת.
האם על המשפט האחרון אתם מסכימים איתי?
האם בעצם , המתמטיקאים טוענים שבעיית ה-"Entscheidungsproblem בלתי פתירה , או שהם רק טוענים שבעיית ה-"Entscheidungsproblem לא פתירה במסגרת המודל של מכונת טיורינג?
*בתגובה זו נעזרתי וציטטתי מתך הבלוג "לא מדויק".
"הוכחות בתורת החישוביות הן תמיד של טענות מהצורה "לא קיימת מכונת טיורינג שעושה כך וכך" - כלומר, עוסקות במודל החישוב הקונקרטי שלנו"
כן , אני יודע שכל הוכחה מתייחסת למודל של מכונת טיורינג. השאלה שלי היא האם משליכים הוכחות שמתייחסות למכונת טיורינג על טענות שמתייחסת למושג חישוב או אלגוריתם?
אם נחזור לשנת 1900 , בשנה בה הילבט הציג את הבעיה העשירית שלו , או לשנת 1928 בה הציג את האתגר שלו שזכה לשם Entscheidungsproblem , (והיה הבעיה הבאה:
למצוא אלגוריתם אשר בהינתן טענה כלשהי שמנוסחת בשפה הפורמלית של הלוגיקה (לוגיקה מסדר ראשון), לקבוע האם היא נכונה או לא (כאשר "נכונה" כאן פירושו "נכונה בכל עולם שמקיים את האקסיומות של הטענה") הרי שהילברט מבקש בשפה של ימינו אנו למצוא "מודל של מכונת חישוב כלשהו" שתפתור את הבעיות הנ"ל.
למעשה , ופה בדיוק אני רוצה לשמוע את דעתכם , כדי לטעון למשל שהאתגר של 1928 (ה-Entscheidungsproblem) בלתי אפשרי , צריך להוכיח שלא קיים אף מודל חישובי שיכול לחשב זאת.
האם על המשפט האחרון אתם מסכימים איתי?
האם בעצם , המתמטיקאים טוענים שבעיית ה-"Entscheidungsproblem בלתי פתירה , או שהם רק טוענים שבעיית ה-"Entscheidungsproblem לא פתירה במסגרת המודל של מכונת טיורינג?
*בתגובה זו נעזרתי וציטטתי מתך הבלוג "לא מדויק".
השני מביניהם
המתמטיקאים טוענים שבעיית ה-Entscheidungsproblem (אגב, זה כפל; המשמעות המילולית של "Entscheidungsproblem" היא "בעיית הכרעה", כך שלהגיד "בעיית ה-Entscheidungsproblem" זה כמו לומר "בעיית בעיית ההכרעה") לא פתירה במסגרת המודל של מכונת טיורינג.
הטענה הלא מתמטית היא שההוכחה שה-Entscheidungsproblem אינה פתירה במסגרת המודל של מכונת טיורינג היא דבר מספיק כדי "להפיס את דעתנו" ולהפסיק להתעסק עם ה-Entscheidungsproblem. אולי יום אחד יומצא מודל חישובי שבמסגרתו יהיה פתרון ל-Entscheidungsproblem ואותו מודל יהיה סביר מבחינה יישומית, אבל לעת עתה אין כזה ולא סביר שיימצא אי פעם. ה"לא סביר" כאן אינו טענה מתמטית פורמלית, דהיינו לא ניתן להוכיח אותו מתמטית; זה דומה לעובדה שמרבית מדעני המחשב יגידו לך שלא סביר ש-P=NP למרות שאין כיום שום הוכחה לכך. למרות שאין הוכחה מתמטית פורמלית, יש לא מעט סיבות לא פורמליות או פורמלית למחצה לחשוב כך.
המתמטיקאים טוענים שבעיית ה-Entscheidungsproblem (אגב, זה כפל; המשמעות המילולית של "Entscheidungsproblem" היא "בעיית הכרעה", כך שלהגיד "בעיית ה-Entscheidungsproblem" זה כמו לומר "בעיית בעיית ההכרעה") לא פתירה במסגרת המודל של מכונת טיורינג.
הטענה הלא מתמטית היא שההוכחה שה-Entscheidungsproblem אינה פתירה במסגרת המודל של מכונת טיורינג היא דבר מספיק כדי "להפיס את דעתנו" ולהפסיק להתעסק עם ה-Entscheidungsproblem. אולי יום אחד יומצא מודל חישובי שבמסגרתו יהיה פתרון ל-Entscheidungsproblem ואותו מודל יהיה סביר מבחינה יישומית, אבל לעת עתה אין כזה ולא סביר שיימצא אי פעם. ה"לא סביר" כאן אינו טענה מתמטית פורמלית, דהיינו לא ניתן להוכיח אותו מתמטית; זה דומה לעובדה שמרבית מדעני המחשב יגידו לך שלא סביר ש-P=NP למרות שאין כיום שום הוכחה לכך. למרות שאין הוכחה מתמטית פורמלית, יש לא מעט סיבות לא פורמליות או פורמלית למחצה לחשוב כך.
אפשר להוכיח בתנאים מסויימים
תחת כמה תנאים בסיסיים ההשערה הזו ניתנת להוכחה.
חלקם מאוד טבעיים (הקוד של המכונה הוא בגודל סופי, המכונה עובדת עם ביטים דיסקרטיים ולא עם משתנה רציף) וחלקם שנויים במחלוקת (המכונה לא מטילה מטבע - מצד אחד זה פוסל את כל האפשרות של אלגוריתמים רנדומיים, מצד שני מחשב אמיתי לא באמת יכול להטיל מטבע אלא רק מחקה רנדומיזציה)
בלינק הזה יש הפניות להוכחה המקורית ולהוכחת המשך עוד יותר שנויה במחלוקת:
http://nanoexplanations.wordpress.c...h-proof-of-the-extended-church-turing-thesis/
תחת כמה תנאים בסיסיים ההשערה הזו ניתנת להוכחה.
חלקם מאוד טבעיים (הקוד של המכונה הוא בגודל סופי, המכונה עובדת עם ביטים דיסקרטיים ולא עם משתנה רציף) וחלקם שנויים במחלוקת (המכונה לא מטילה מטבע - מצד אחד זה פוסל את כל האפשרות של אלגוריתמים רנדומיים, מצד שני מחשב אמיתי לא באמת יכול להטיל מטבע אלא רק מחקה רנדומיזציה)
בלינק הזה יש הפניות להוכחה המקורית ולהוכחת המשך עוד יותר שנויה במחלוקת:
http://nanoexplanations.wordpress.c...h-proof-of-the-extended-church-turing-thesis/
נראה לי שאתה הכי קלעת למהששאלתי
לא חלילה שאני לא נהניתי לקרוא את שאר התשובות המפורטות , המעניינות והיפות שלכם (שעסקו במה ששאלתי אבל טיפה פיספסו את הנקודה הקריטית של השאלה. אבל דווקא משום כך התשובות שלכם הןעשירות ומעניינות ויכולות לגלוש לנושאים רלוונטיים יפים , ואני מודה לכם באמת מכל הלב. תענוג לקרוא את כל התשובות שלכם!).
"אילן לאלא" - הגבת בדיוק למה ששאלתי. לא הבנתי לגמרי את הכול עד הסוף - אבל אתה התייחסת ישירות לנקודה שלי.
במה התכוונת ב"וחלקם שנויים במחלוקת"?
רשמת: "בלינק הזה יש הפניות להוכחה המקורית ולהוכחת המשך עוד יותר שנויה במחלוקת:" מה בדיוק שנוי במחלוקת?
מה שאתה אומר בגדול שכן ניתן להוכיח את התזה תחת הנחות מסויימות , ושחלק מההוכחה/הוכחות שנויות במחלוקת?
אלה מכם שמשתעממים כרגע בעבודה , הנה משהו קצת יותר מעניין להתעסק בו
. אתם מוזמנים להגיב
לא חלילה שאני לא נהניתי לקרוא את שאר התשובות המפורטות , המעניינות והיפות שלכם (שעסקו במה ששאלתי אבל טיפה פיספסו את הנקודה הקריטית של השאלה. אבל דווקא משום כך התשובות שלכם הןעשירות ומעניינות ויכולות לגלוש לנושאים רלוונטיים יפים , ואני מודה לכם באמת מכל הלב. תענוג לקרוא את כל התשובות שלכם!).
"אילן לאלא" - הגבת בדיוק למה ששאלתי. לא הבנתי לגמרי את הכול עד הסוף - אבל אתה התייחסת ישירות לנקודה שלי.
במה התכוונת ב"וחלקם שנויים במחלוקת"?
רשמת: "בלינק הזה יש הפניות להוכחה המקורית ולהוכחת המשך עוד יותר שנויה במחלוקת:" מה בדיוק שנוי במחלוקת?
מה שאתה אומר בגדול שכן ניתן להוכיח את התזה תחת הנחות מסויימות , ושחלק מההוכחה/הוכחות שנויות במחלוקת?
אלה מכם שמשתעממים כרגע בעבודה , הנה משהו קצת יותר מעניין להתעסק בו
זה כתוב בפסקה הראשונה
זה שנוי במחלוקת כי זה מניח הנחות שבכלל לא בטוח שהן תקפות.
It is safe to say that the proof is controversial — not because it is technically inaccurate, but because it relies on an axiomatization of computation that excludes randomness, parallelism and quantum computing.
וזאת בדיוק הנקודה: אתה לא יכול להוכיח טענה בלי להתבסס על הנחות יסוד/עובדות כלשהן.
תעקוב אחרי המאמר - הם עושים בדיוק את מה שטיורינג עשה. הם מגדירים את המושג "אלגוריתם", ואז מגדירים את המושג "חישוב", ומזה מסיקים אם אלגוריתם מסוים ניתן לחישוב לפי הגדרתם.
אבל כדי להגיע להגדרות הם מגיעים להנחות מסוימות, שאנשים טוענים שעלולות להיות לא נכונות (אני מתרגם את הכתוב במאמר, אתה יכול ללכת ולקרוא את הרפרנסים). למשל, הם מניחים שלא יכול להיות מודל חישובי בו יהיו תוצאות אקראיות, הכל חייב להיות דטרמיניסטי. בעולם חישובי של ימינו זה נכון, אבל האם זה אכן כך במציאות באמת?
יחד עם זאת, אם אנחנו מניחים שהמגבלות שהם הציבו סבירות - אז גם ההוכחה סבירה. אבל אנחנו שוב חוזרים לשאלה שלך - "מי אמר? למה להאמין? תוכיחו לי שההנחות אכן מתקיימות".
זה שנוי במחלוקת כי זה מניח הנחות שבכלל לא בטוח שהן תקפות.
It is safe to say that the proof is controversial — not because it is technically inaccurate, but because it relies on an axiomatization of computation that excludes randomness, parallelism and quantum computing.
וזאת בדיוק הנקודה: אתה לא יכול להוכיח טענה בלי להתבסס על הנחות יסוד/עובדות כלשהן.
תעקוב אחרי המאמר - הם עושים בדיוק את מה שטיורינג עשה. הם מגדירים את המושג "אלגוריתם", ואז מגדירים את המושג "חישוב", ומזה מסיקים אם אלגוריתם מסוים ניתן לחישוב לפי הגדרתם.
אבל כדי להגיע להגדרות הם מגיעים להנחות מסוימות, שאנשים טוענים שעלולות להיות לא נכונות (אני מתרגם את הכתוב במאמר, אתה יכול ללכת ולקרוא את הרפרנסים). למשל, הם מניחים שלא יכול להיות מודל חישובי בו יהיו תוצאות אקראיות, הכל חייב להיות דטרמיניסטי. בעולם חישובי של ימינו זה נכון, אבל האם זה אכן כך במציאות באמת?
יחד עם זאת, אם אנחנו מניחים שהמגבלות שהם הציבו סבירות - אז גם ההוכחה סבירה. אבל אנחנו שוב חוזרים לשאלה שלך - "מי אמר? למה להאמין? תוכיחו לי שההנחות אכן מתקיימות".
כן
דרשוביץ וגורביץ הגדירו הנחות מסויימות שתחתן אפשר להוכיח את התיזה כמשפט. אף אחד לא מפקפק בכך שאם מקבלים את ההנחות שלהן אזי הם הוכיחו את תיזת צ'רץ-טיורינג.
מה שלא כזה ברור, הוא האם ההנחות שלהם (וההגדרות שנובעות מהן) תופסות באמת את מה שאינטואיטיבי לקרוא לו "חישוב". למשל, בתיאוריה של מדעי המחשב מקובל לחשוב על אלגוריתמים שיש להם סיכוי לטעות (ואפשר להראות שאם יש לך אלגוריתם כזה אפשר להריץ אותו מספיק פעמים כדי שהסיכוי לטעות יהיה קטן כרצונך). לפי האקסיומות שלהם פרוצדורה כזו אינה נחשבת ל"חישוב". אז האם אתה מקבל את ההנחות שלהם? זו כבר שאלה פילוסופית ולא שאלה מתמטית. מבחינה מתמטית - התיזה היא משפט שנובע מהאקסיומות שלהם.
אני דרך אגב לא שותף לדעת הרוב בשרשור הזה. אני חושב שהשואל המקורי שם את האצבע על נקודה מאוד מעניינת. עובדה שהמאמר של דרשוביץ וגורביץ פורסם רק ב - 2008 (!). אני לפחות לא מכיר הוכחות קודמות שהצליחו להגדיר מערכת פורמלית של הנחות שבתוכה אפשר להוכיח את התיזה.
נ.ב.
דרשוביץ היה המרצה שלי בקורס לחישוביות לפני כמה וכמה שנים. אדם ממש נחמד אבל מעופף ברמות אחרות
דרשוביץ וגורביץ הגדירו הנחות מסויימות שתחתן אפשר להוכיח את התיזה כמשפט. אף אחד לא מפקפק בכך שאם מקבלים את ההנחות שלהן אזי הם הוכיחו את תיזת צ'רץ-טיורינג.
מה שלא כזה ברור, הוא האם ההנחות שלהם (וההגדרות שנובעות מהן) תופסות באמת את מה שאינטואיטיבי לקרוא לו "חישוב". למשל, בתיאוריה של מדעי המחשב מקובל לחשוב על אלגוריתמים שיש להם סיכוי לטעות (ואפשר להראות שאם יש לך אלגוריתם כזה אפשר להריץ אותו מספיק פעמים כדי שהסיכוי לטעות יהיה קטן כרצונך). לפי האקסיומות שלהם פרוצדורה כזו אינה נחשבת ל"חישוב". אז האם אתה מקבל את ההנחות שלהם? זו כבר שאלה פילוסופית ולא שאלה מתמטית. מבחינה מתמטית - התיזה היא משפט שנובע מהאקסיומות שלהם.
אני דרך אגב לא שותף לדעת הרוב בשרשור הזה. אני חושב שהשואל המקורי שם את האצבע על נקודה מאוד מעניינת. עובדה שהמאמר של דרשוביץ וגורביץ פורסם רק ב - 2008 (!). אני לפחות לא מכיר הוכחות קודמות שהצליחו להגדיר מערכת פורמלית של הנחות שבתוכה אפשר להוכיח את התיזה.
נ.ב.
דרשוביץ היה המרצה שלי בקורס לחישוביות לפני כמה וכמה שנים. אדם ממש נחמד אבל מעופף ברמות אחרות
התשובה לשאלה הזאת נוגעת ביסודות המתמטיקה
הבעיה פה היא שאתה משתמש במונח "הוכחה" בשני משמעויות דומות אבל שונות.
יש את המשמעות שכולנו מכירים מחיי היום יום "להדגים בסבירות גבוהה מאוד שמשהו נכון" ("proven beyond resonable doubt").
ויש את המשמעות מהלוגיקה המתמטית, הגדרת מערכת אקסיומות והפעלת כללי הסקה בשביל בשביל להגיע לזה שטענה (כלומר, ביטויי בלוגיקה פורמלית, רצף של סימבולים) היא נכונה או לא נכונה. הוכחה פורמלית היא בסך הכול משחק עם סימבולים, מערכת האקסיומות לא צריכה להיות קשורה לעולם האמיתי, היא רק לא צריכה להוביל לסתירות. אתה בסך הכול מספר סיפור עם המשחק הזה עם סימבולים שייכול להוביל למסקנות אבסורדיות ביותר (לדוגמה שאפשר לפרק תפוח, ולהרכיב מחדש ממנו כדור בגודל של השמש - הפרדוקס של בנך-טרסקי).
חשוב להבין שכאשר מוכיחים לך משהו בכיתה, במובן הפורמלי לא מדובר בהוכחה אמיתית, אלא בתוכנית high level לבניית ההוכחה.
אם אתה מבין את המשמעות של הוכחה פורמלית, אתה מבין מיידית שזה בלתי אפשרי להוכיח משהו לגבי מונח שאין לו הגדרה במונחים של המערכת הפורמלית שבה אמורה להתבצע ההוכחה (אם אתה לא מסוגל לתאר את המונח "אלגוריתם" בשפה הפורמלית של מערכת האקסיומות, בטח שאתה לא ייכול להוכיח משהו לגביו).
הבעיה פה היא שאתה משתמש במונח "הוכחה" בשני משמעויות דומות אבל שונות.
יש את המשמעות שכולנו מכירים מחיי היום יום "להדגים בסבירות גבוהה מאוד שמשהו נכון" ("proven beyond resonable doubt").
ויש את המשמעות מהלוגיקה המתמטית, הגדרת מערכת אקסיומות והפעלת כללי הסקה בשביל בשביל להגיע לזה שטענה (כלומר, ביטויי בלוגיקה פורמלית, רצף של סימבולים) היא נכונה או לא נכונה. הוכחה פורמלית היא בסך הכול משחק עם סימבולים, מערכת האקסיומות לא צריכה להיות קשורה לעולם האמיתי, היא רק לא צריכה להוביל לסתירות. אתה בסך הכול מספר סיפור עם המשחק הזה עם סימבולים שייכול להוביל למסקנות אבסורדיות ביותר (לדוגמה שאפשר לפרק תפוח, ולהרכיב מחדש ממנו כדור בגודל של השמש - הפרדוקס של בנך-טרסקי).
חשוב להבין שכאשר מוכיחים לך משהו בכיתה, במובן הפורמלי לא מדובר בהוכחה אמיתית, אלא בתוכנית high level לבניית ההוכחה.
אם אתה מבין את המשמעות של הוכחה פורמלית, אתה מבין מיידית שזה בלתי אפשרי להוכיח משהו לגבי מונח שאין לו הגדרה במונחים של המערכת הפורמלית שבה אמורה להתבצע ההוכחה (אם אתה לא מסוגל לתאר את המונח "אלגוריתם" בשפה הפורמלית של מערכת האקסיומות, בטח שאתה לא ייכול להוכיח משהו לגביו).
Copyright©1996-2021,Tapuz Media Ltd. Forum software by XenForo® © 2010-2020 XenForo Ltd.