בתשובה לאלון עמית, 17/07/05 21:27
יופי 317486
אולי אני לא מבין למה אתה מתכוון בייצוג של האדם כמ"ט. אם האדם יכול לדעת את PA, ללמוד אותה בקורס לוגיקה או להמציא אותה, אז אני לא רואה איך רדוקציה של אותו אדם לכדי מ"ט תהיה שלמה אם היא לא מכילה בתוכה את PA, אם לא ניתן לבטא כל משפט ב-PA במ"ט הזאת.
יופי 317565
"לבטא כל משפט"? איזו בעייה יש לבטא כל משפט של PA במ"ט? אולי אתה לא ממש מסביר למה אתה מתכוון בייצוג. אני למדתי את PA, כן; ואת מה שאני יכול לעשות עם PA, יכולה גם תכנית מחשב שיקח לי חצי-יום לכתוב.

בפעם השלישית: מה יש לאדם שאין ל-PA? אתה מבין, או לא מבין, ש"לדעת את PA" או "ללמוד אותה בקורס בלוגיקה" או "להמציא אותה" זה לא מספיק?
יופי 317569
מה עם היכולת להוכיח בעזרת ZFC את משפט גודסטיין? (סתם שליפה, אל תירה בי)
יופי 317575
שלח את המ"ט לקורס המתקדם (זה שבו לומדים את ZFC); היא תוכיח לך בחדווה גם את גודסטין. אתה רוצה שהיא *תמציא* את ZFC? תן לה קצת לשחק, וגם זה יקרה (למה לא?)
יופי 317577
שאלת "מה יש לאדם שאין ל-PA". לי אישית ברור שמכונת הטיורינג (האוניברסלית) הממוצעת הרבה יותר חכמה ממני, רק שבגלל נסיבות טכניות עוד לא בנו אותה.
יופי 317587
בהקשר של הדיון ביני לבין ד.ק., אין הבדל בין PA למערכת אחרת (אלא אם כן ד.ק. יפתיע).
יופי 318417
PA היא "חשופה למשפט גדל", ולכן היא או לא עקבית, או לא שלמה, נכון?
יש לי כמה שאלות.
א. ב-ZFC אני יכול לבנות מודל ל-PA וכך להוכיח את עקביותה ב-ZFC?
ב. האם אני יכול לעשות גם ההיפך?
ג. אם לא, האם זה אומר ש-ZFC יותר חזקה מ-PA?
ד. אם כן, האם זה אומר ש-ZFC בהכרח חשופה גם היא למשפט גדל?
יופי 318429
א. כן, ZFC מוכיחה עקביות PA (מה זה עקביות *ב*-ZFC?). ראה תשובה מפורטת יותר לעוזי מתישהו מאוחר יותר.
ב. לא.
ג.במובן מסוים כן.
ד. ZFC חשופה למשפט גדל ללא קשר מכיון שהיא תורה אריתמטית ואפקטיבית.
יופי 318443
א. מאחר ואנחנו לא יודעים אם ZFC בעצמה היא עקבית, אנחנו גם לא בטוחים שההוכחה שלה את עקביות PA היא נכונה. כלומר, PA מוכחת כעקבית רק בתוך ZFC, לא?
יופי 318433
ג. אני רק רוצה להזכיר, שוב, שיש תורות המוכיחות את עקביות PA, ו-PA לא מוכיחה את עקביותן, אבל הן לא "יותר חזקות" מ-PA כי יש משפטים ש-PA מוכיחה והן לא.

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

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

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

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

אם אתה טוען שאדם יודע מתמטיקה ושימפנזה לא וZFC לא, עליך להסביר באיזה מובן אדם יודע משהו על מספרים משהו ש-ZFC לא יודעת.
יופי 318474
אני לא מבין מה המשמעות של לתאר את PA ואת ZFC באמצעות מערכת פורמאלית. אולי מטא-מערכת מתארת מערכת-בת. מטא-שפה כנראה מתארת שפה-אובייקט. אבל אני לא יודע, זה מוזר להתייחס אליהן בצורה הזו.

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

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

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

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

(תשובה עם "אלוהים אדירים" תתקבל בהכנעה. ברור לי שאני טועה, רק לא ברור לי איפה)
פינת השאלה הקטנה 318547
אלוהים אדירים!

(סתם, אני סקרן לראות אותך כנוע).

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

(אגב, זה לא הכל; מה שהראינו בינתיים זה שאם PA עקבית אז G לא יכיח ב-PA. זה לא אומר ש-PA לא שלמה: צריך גם להראות ש*שלילת* G לא יכיחה ב-PA. את זה *אי-אפשר* לעשות בלי להניח עוד משהו, סוג של נאותות, על PA; מי שהצליח להיפטר מהדרישה הנוספת הזו היה רוסר, אבל הוא לא השתמש במשפט האריתמטי שהזכרת אלא במשפט אחר, יותר מתוחכם ונבזי).

זה פותר את הבעייה? אם לא, אנא, תן לי את הצ'אנס לראות אותך שוב מקבל בהכנעה.
פינת השאלה הקטנה 318591
קראת לי?

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

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

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

3. אם כך, PA אינה סתם "או לא עקבית או לא שלמה" אלא "לא עקבית" ממש, בניגוד גמור לסעיף 1 לעיל.

4. כידוע, זאת לא המסקנה האמיתית ממשפט גדל שטוען טענה חלשה יותר.
פינת השאלה הקטנה 318669
למה? אם PA אכן לא מוכיחה את G, G דובר אמת, נכון. אבל זה לא אומר שיש הוכחה פורמלית ב-PA של G; מסתמא אין כזו, דווקא.

1. לא לגמרי הבנתי איך זה קשור לטיעון. נכון שזה סביר יותר, אבל איך זה מקנה תוקף להמשך?

2. "את אמיתות הטענה *הוכחנו* ב PA" - את אמיתות איזו טענה? שוב אתה מנסה להדחיק את "הנחת העקביות שלה": קודם הגלית אותה מחוץ לכוכביות, עכשיו שמת אותה בסוגריים. מה ש-PA מראה הוא את הגרירה PA עקבית -> G; זה פסוק פורמלי שיש לו הוכחה פורמלית ב-PA: אקסיומה, אקסיומה, מסקנה, אקסיומה, מסקנה, מסקנה, מסקנה, בום, מש"ל. הוכחה פורמלית כזו ל-G עצמה, סובר הציבור הרחב, דווקא אין!

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

וזה, כזכור, בדיוק מה שגם PA יודעת להראות, פורמלית לגמרי. אני מציין זאת כדי להדגיש שוב שאין פה איזו מערכת חיצונית ל-PA, איזה הגיון-ברזל משולב בחכמת-חיים, שמצליח להראות משהו ש-PA לא. את C->G מראה גם הגיוננו וגם PA, כש-C זה הפסוק "PA עקבית"; את G עצמה לא אנחנו ולא PA יודעים להראות.

3. כדי להסיק ש-PA לא עקבית, יש לעשות דבר פשוט: להוכיח פורמלית דבר והיפוכו, או לפחות להוכיח פורמלית שיש הוכחה פורמלית של דבר והיפוכו. כפי שאתה רואה, לא עשינו את זה ולא עשינו את זה - נכון? את איזה פסוק-והיפוכו הוכחנו?

נדמה לי שקודם הרגשת בנוח עם משפט גדל והוכחתו, ומה שמבלבל אותך עכשיו הוא הטענה שלי שלא רק שהמשפט נכון, אלא שהוכחתו ניתנת לפירמול ב-PA. שוב, כל מה שזה אומר הוא שהפסוק C->G יכיח ב-PA - והפסוק הזה איננו G עצמו.
פינת השאלה הקטנה 318843
זהו נסיון נוסף שלי לעשות סדר, לפני שנחליט להעביר את המשך הפתיל ל דיון 1571. שוב אמספר את הטענות שלי כדי שתוכל לשלות במלקחיים את הטענה השגויה ולהסביר לי את הטעות. אני גם משמיט, בשלב הראשון, כל מיני פסאודו-טענות מעורפלות ואמירות כלליות ומנסה לגעת בלב העניין.

1. G הוא משפט ב PA.

2. G אומר "אני לא יכיח ב PA".

3. אם G אינו נכון, הרי שהטענה שהוא טוען שגויה, דהיינו הוא כן יכיח ב PA. מכאן: ב PA אפשר להוכיח משפטים לא נכונים (שהרי זאת ההנחה על G בסעיף זה), ומכאן שהיא לא עקבית. אם אתה מתעקש על הוכחה של משפט וגם של המשפט המנוגד לו, אפשר בקלות לנסח את המצב גם באופן הזה.

4. אם G נכון, הרי הטענה שהוא טוען מתקיימת, ומצאנו משפט נכון שאינו יכיח, ומכאן ש PA אינה שלמה.

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

5. האם ייתכן ש PA עקבית אך לא שלמה? הרי הראינו בסעיף 3 שאם היא עקבית אזי G חייב להיות נכון (אינו יכול להיות לא נכון).

6. מה זה "הראינו בסעיף 3"? הוכחנו. אם לא השתמשנו שם בשום דבר שחורג מתחומי PA הרי שהוכחנו זאת ב PA.

7. אם כך הוכחנו את מה שכביכול אינו יכיח והגענו שוב לסתירה.

8. אם כך PA אינה עקבית.

והערה לסיום: כידוע אני לא נמנה עם מחנה "מותר האדם ממכונות טיורינג" כך שאין צורך לחשוד בי שאני מנסה להשתמש במשפט גדל כדי לשרת איזו אג'נדה אנתרופוצנטרית. אתה צודק בכך שהרבה זמן חייתי בשלום עם G מתוך שהינחתי שסעיף 6 לא נכון, דהיינו שבסעיפים 3 ו 4 נעשה שימוש בטיעונים שחורגים מ PA (אין לי מושג אילו מחוקי הלוגיקה הם חלק ממנה ומה בדיוק מותר לטעון במסגרתה). רק כשהערת באחת ההודעות שהכל כולל הכל נעשה בתוך PA התחלתי להרגיש את תחושת חוסר הנוחות ממה שהולך כאן. אני מכיר היטב את התחושה הזאת: היא מהסוג שמתחלף מהר בהרגשה "איזה אידיוט אני", אבל אליה כבר התרגלתי מזמן.
פינת השאלה הקטנה 318927
לא הבנתי את 7. איזו סתירה? מה שהוכחנו הוא, כדבריך (ואני מצטט את סעיף 5): "הראינו בסעיף 3 שאם היא עקבית אזי G חייב להיות נכון". זהו, זה כל מה שהראינו: ש*אם* PA עקבית *אז* G חייב להיות נכון. זה (כמו שציינת ב-‏6) כל מה שאנחנו יודעים להוכיח ב-PA. איפה הסתירה?
פינת השאלה הקטנה 318942
אבוי. הראינו (תחת הנחת העקביות) ש G חייב להיות נכון, אבל G עצמו הרי אומר שאנחנו לא יכולים להראות דבר כזה ("א... אי.. אינ... אינני יכיח" הוא חוזר ואומר), כלומר הוא לא נכון. סתירה.

אולי העניינים יתבררו לי ביתר קלות אם תשיב על שאלה אחרת: האם ניתן לבנות בדומה ל G את המספר R שהטענה שהוא מייצג היא "אינני נכון ב PA"?
פינת השאלה הקטנה 318945
אבל אתה מבלבל בין "תחת הנחת העקביות, G נכון" ל-"G נכון".
שים לב:

"הראינו (תחת הנחת העקביות) ש G חייב להיות נכון"

נכון...

"אבל G עצמו הרי אומר שאנחנו לא יכולים להראות דבר כזה"

לא נכון. הוא אומר "אינני יכיח מהאקסיומות של PA ותו לא; אני לא מתחייב על מה יקרה איתי אם תצרף הנחות נוספות (למשל ההנחה ש-PA עקבית)".

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

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

מה היית עונה לאותה הרגשה טורדנית?
פינת השאלה הקטנה 319027
"הוכחנו (בדרך השלילה) את המשפט שאומר על עצמו שאינו יכיח".

וביתר פירוט:

"הוכחנו (ב-SA) את המשפט שאומר על עצמו שאינו יכיח-ב-PA"

לכן SA לא עקבית? למה?
פינת השאלה הקטנה 319124
אהה! תודה.
פינת השאלה הקטנה 320295
אם טרם מיציתי את הסבלנות שלך, ואם יש לך זמן וחשק: מה עם המספר R?

(אם התשובה על הרישא שלילית זה בסדר, הכי גרוע אשוב אל GEB הישן והטוב, נדמה לי שהוא מזכיר אותו).
R מה הוא אומר? 320384
אין בעייה :-) אבל לא הבנתי מה ברצונך שהמספר R "יגיד". מה זה "נכון ב-PA"? נובע מהאקסיומות? נכון במודל הסטנדרטי של הטבעיים? אם זה הראשון, אז זה בדיוק "יכיח", כמו G. אם השני, אין לזה קשר ל-PA, ואין פרדיקט ב-PA האומר "x נכון בטבעיים". להגיד ש-x נכון זה פשוט להגיד "x"; להגיד שהוא לא נכון זה פשוט להגיד "לא x". אתה רוצה ש-R יהיה "לא R"? אי-אפשר...
יופי 318459
ג. אנסה להתחכם עוד יותר מהמתטיקאי שמעלי (תוך הסתכנות באמירת שטויות): התורה שיש בה אקסיומה אחת: "PA עקבית".
יופי 318461
אי אפשר להגיד סתם-כך ''עקבית''. שפה מסדר ראשון מרשה לך להשתמש רק בקשרים הלוגיים הרגילים, ובפונקציות, יחסים וקבועים שמותרים בשפה. צריך מספיק ''יכולת אריתמטית'' במסגרת השפה כדי לתרגם ''עקביות'' למשפט תקני בשפה (העובדה שזה בכלל אפשרי היא ההישג הגדול של גדל).
יופי 318469
בדיוק כפי שציינת, את האקסיומה "PA עקבית" אפשר לרשום באותו אופן גם ב-PA וגם בתורה שיש לה את אותה השפה של PA ואף לא אקסיומה אחת. ה"יכולת האריתמטית" קיימת ב*שפה* ברגע שיש בה את הסימנים המתאימים ("0", "+" וכו'). לכאורה, אפשר לקחת את הנוסחה (Con(PA כפי שהיא מופיעה ב-PA, ולהשאיר אותה לבד בלי אף אקסיומה אחרת, ולקבל את התורה שירדן דיבר עליה.

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

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

1 בעצם לקחנו את כל המופעים של סכמת האינדוקציה שמופיעים בהוכחת משפט גדל.
יופי 318506
סילוק חלק מאקסיומות האינדוקציה היה המהלך הבא שלי - חשפת אותי!

פרסבורגר הוא כנראה באמת חלש מדי.
יופי 318471
עוד פעם אתה עושה את הבלבול הזה בין *תיאור* שלם של מערכת פורמלית לבין שלמות התורה. זה לא אותו דבר בשום מובן שאני יכול להעלות על הדעת. כדי לסבר את האוזן, אתן דוגמא:
האם מי שמתכנן מחשב (או iMac, בשביל אלון) צריך לדעת מה יעשה המחשב עבור כל קלט נתון? כן, הוא יכול להריץ סימולציה של המחשב המתוכנן. האם זה אומר שהוא יודע, עבור כל פלט אפשרי, האם יש קלט שיגרום למחשב לתת את הפלט הזה? התשובה במהופך:

cl

סתם, התשובה היא לא, אבל כן אפשר לכתוב במהופך.
יופי 318481
האם הפיזיקה אינה מערכת פורמאלית שמתארת את העולם? כדי שהיא תהיה שלמה, כל משפט בשפה שלה שנכון לגבי העולם צריך להיות יכיח בה על סמך האקסיומות וכללי ההיסק. אני משער שיש כל מיני דרכים להבנות את כל הידע הפיזיקלי לכדי מערכת. אולי חוקי הפיזיקה הם הפונקציות והאקסיומות, וגם יש איזשהו קבוע - המפץ הגדול בנקודת זמן 0. אנחנו יכולים לחשב איך בדיוק היקום נראה בכל נקודת זמן על סמך המערכת הזאת (אם היא שלמה), כלומר להוכיח בה כל משפט שנכון לגבי היקום.
אבל איך לעזאזל ניתן להוכיח שהיא עקבית? הרי אי אפשר לבנות לה מודל בתורה חיצונית מכיוון שלא יכולה להיות לה תורה חיצונית.
יופי 318494
לי אישית לא ברור למה מערכת פורמלית שמתארת את העולם/פיזיקה+תנאי התחלה צריכה להיות:
א. אפקטיבית
ב. שלמה

א. מניח שיש תורה של הכל עם תיאור סופי, ענין שכלל לא ברור בעיני.
ב. עוד פחות ברור. אם יורשה לי לצטט סתם איזה מישהו: האם השאלה האם יש אינסוף ספרות 7 בפיתוח העשרוני של פאי היא שאלה פיזיקלית?
יופי 318497
אני גם לא חושב שהמערכת שמתארת את היקום היא אפקטיבית ושלמה. אבל זאת המשמעות של המשפט ''היקום הוא מ''ט''.
יופי 318538
אני חושש שהתבלבת כאן: ברור שלכל פלט אפשרי X קיים קלט שגורם למחשב לתת אותו. למשל הקלט:

printf("%s", X);‎
יופי 318550
אתה חושב על מחשב שמריץ תוכניות בשפת C ואילו אני מדבר על מחשב כללי. גם בדוגמא שלך אין לך תיאור שלם במובן ש-ד.ק. השתמש בו: אם תריץ תוכנה למצוא מספר זוגי שאינו סכום של שני ראשוניים האם היא תדפיס משהו?

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

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